Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning

Proceedings of the ACM on Programming Languages, vol. 5, pp. 1–30

Abstract

We study a syntax for specifying quantitative assertions —functions mapping program states to numbers—for probabilistic program verification. We prove that our syntax is expressive in the following sense: Given any probabilistic program C , if a function f is expressible in our syntax, then the function mapping each initial state σ to the expected value of evaluated in the final states reached after termination of C on σ (also called the weakest preexpectation wp[ C ]( f )) is also expressible in our syntax. As a consequence, we obtain a relatively complete verification system for reasoning about expected values and probabilities in the sense of Cook: Apart from proving a single inequality between two functions given by syntactic expressions in our language, given f , g , and C , we can check whether g ≼ wp[ C ]( f ).

Authors 4

1. Kevin Batz Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

2. Benjamin Lucien Kaminski

   University College London

   Affiliation as printed

   University College London, UK

3. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Germany

4. Christoph Matheja

   ETH Zurich

   Affiliation as printed

   ETH Zurich, Switzerland