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 31
n33709114_phd_content.pdf n33709114_phd_content.pdf application/pdf 1003.01KB 1
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 2
Author Meinicke, Larissa A.
Thesis Title Transformation Rules for Probabilistic Progams: An Algebraic Approach
School, Centre or Institute School of Information Technology and Electrical Engineering
Institution The University of Queensland
Publication date 2008-05
Thesis type PhD Thesis
Supervisor Hayes, Ian J.
Subjects 290000 Engineering and Technology
280000 Information, Computing and Communication Sciences
Formatted abstract Program transformation rules describe the conditions under which it is possible to transform one program into another one which preserves the behaviour of the first. They may be used to reason about such things as compiler optimisations, distributed algorithms or data refinement. 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 verified 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 defined 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 identified, discussed, and used to specify commonalities between different 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 satisfies 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.

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