01whole.pdf (2.2 MB)
Download file

Semantics and loop invariant synthesis for probabilistic programs

Download (2.2 MB)
thesis
posted on 28.03.2022, 12:10 by Friedrich Gretz
In this thesis we consider sequential probabilistic programs. Such programs are a means to model randomised algorithms in computer science. They facilitate the formal analysis of performance and correctness of algorithms or security aspects of protocols. We develop an operational semantics for probabilistic programs and show it to be equivalent to the expectation transformer semantics due to McIver and Morgan. This connection between the two kinds of semantics provides a deeper understanding of the behaviour of probabilistic programs and is instrumental to transfer results between communities that use transition systems such as Markov decision processes to reason about probabilistic behaviour and communities that focus on deductive verification techniques based on expectation transformers. As a next step, we add the concept of observations and extend both semantics to facilitate the calculation of expectations which are conditioned on the fact that no observation is violated during the program's execution. Our main contribution here is to explore issues that arise with non-terminating, non-deterministic or infeasible programs and provide semantics that are generally applicable. Additionally, we discuss several program transformation to facilitate the understanding of conditioning in probabilistic programming. In the last part of the thesis we turn our attention to the automated verification of probabilistic programs. We are interested in automating inductive verification techniques. As usual the main obstacle in program analysis are loops which require either the calculation of fixed points or the generation of inductive invariants for their analysis. This task, which is already hard for standard, i.e. non-probabilistic, programs, becomes even more challenging as our reasoning becomes quantitative. We focus on a technique to generate quantitative loop invariants from user defined templates. This approach is implemented in a software tool called Prinsys and evaluated on several examples.

History

Table of Contents

1. Introduction -- 2. Linking operational and denotational semantics -- 3. Conditional probabilities and expectations -- 4. Automated analysis -- Chapter 5. Conclusion and future work -- Appendices.

Notes

"A thesis submitted in fulfilment of the requirements for the degree of Doctor of Philosophy in the Department of Computing, Faculty of Science and Engineering, Macquarie University". "2014". Bibliography: pages 75-82

Awarding Institution

Macquarie University

Degree Type

Thesis PhD

Degree

PhD, Macquarie University, Faculty of Science and Engineering, Department of Computing

Department, Centre or School

Department of Computing

Year of Award

2015

Principal Supervisor

Annabelle. McIver

Rights

Copyright Friedrich Gretz 2015. Copyright disclaimer: http://www.copyright.mq.edu.au/ Copyright disclaimer: http://www.copyright.mq.edu.au

Language

English

Extent

1 online resource (x, 85 pages) illustrations (some coloured)

Former Identifiers

mq:42261 http://hdl.handle.net/1959.14/1051765