# Transformation Rules for Probabilistic Progams: An Algebraic Approach

Meinicke, Larissa A. (2008). Transformation Rules for Probabilistic Progams: An Algebraic Approach PhD Thesis, School of Information Technology and Electrical Engineering, The University of Queensland.

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
n33709114_phd_abstract.pdf n33709114_phd_abstract.pdf application/pdf 1.00MB 33
n33709114_phd_content.pdf n33709114_phd_content.pdf application/pdf 1003.01KB 3
n33709114_phd_front.pdf n33709114_phd_front.pdf application/pdf 87.21KB 51
n33709114_phd_totalthesis.pdf n33709114_phd_totalthesis.pdf application/pdf 1.00MB 8
Author Meinicke, Larissa A. Transformation Rules for Probabilistic Progams: An Algebraic Approach School of Information Technology and Electrical Engineering The University of Queensland 2008-05 PhD Thesis Hayes, Ian J. 290000 Engineering and Technology280000 Information, Computing and Communication Sciences Program transformation rules describe the conditions under which it is possible to transform one program into another one which preserves the behaviour of the ﬁrst. They may be used to reason about such things as compiler optimisations, distributed algorithms or data reﬁnement. Such program transformations have traditionally been used to reason about standard (i.e., non-probabilistic) programs which may possibly include a nondeterministic choice operator. In this thesis we aim to identify and verify transformation theorems for probabilistic programs. In particular we examine probabilistic programs which may contain a discrete proba¬bilistic choice operator in addition to one or two nondeterministic choice operators. Such probabilistic programs may be used for reasoning about distributed proba¬bilistic algorithms, reliable systems modelling, or probabilistic games. The probabilistic transformation theorems are investigated and veriﬁed using an algebraic approach since this method has been successfully applied to this task for standard programs. We only consider probabilistic program models in which choices are resolved – intuitively speaking – according to the execution order of the program. Such probabilistic program models, even those which only include one form of nondeterministic choice, do not satisfy all of the algebraic properties of standard programs which may only include one form of choice. This means that many well known program transformation theorems do not hold for these programs. We algebraically investigate transformation theorems for a non-reactive proba¬bilistic program model in detail. This model, an expectation-transformer model, is suitable for reasoning about total program correctness, and can be used to express guards, assertions, recursively deﬁned statements, in addition to probabilistic, de¬monic and angelic choice. As part of this work, transformation theorems for weak and strong iteration statements, as well as non-reactive probabilistic action systems and while loops are developed. Abstract algebras that are suitable for expressing and verifying many of the transformation theorems we had investigated in the total-correctness model are then identiﬁed, discussed, and used to specify commonalities between diﬀerent pro¬gram models. In particular we use the algebras to show that standard programs which may include two forms of choice share many algebraic similarities with the probabilistic programs we have considered, and that most of our transformation theorems are equally valid for these kinds of programs. We also develop a sim¬ple reactive program language which is capable of modelling reactive probabilistic action systems, and we show that this model also satisﬁes many of the same alge¬braic properties as the non-reactive model. This work demonstrates how it may be possible to reason about transformations of reactive probabilistic programs in the same way it is possible to reason about non-reactive ones.

 Document type: Thesis UQ Theses (RHD) - UQ staff and students only UQ Theses (RHD) - Official

Citation counts: Search Google Scholar 376 Abstract Views, 95 File Downloads  -  Detailed Statistics Fri, 13 Jun 2008, 11:09:15 EST by Noela Stallard on behalf of Library - Information Access Service