Relatively Complete Verification of Probabilistic Programs

arXiv (Cornell University)

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 $f$ evaluated in the final states reached after termination of $C$ on $σ$ (also called the weakest preexpectation $\textit{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 \preceq \textit{wp} [C] (f)$.

Authors 4

1. Kevin Batz Aachen

   Christophorus Kliniken · RWTH Aachen University

   Affiliation as printed

   CHRISTOPH MATHEJA ,

   RWTH Aachen University

2. Benjamin Lucien Kaminski Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University (Germany)

3. Joost-Pieter Katoen Aachen

   Christophorus Kliniken · RWTH Aachen University

   Affiliation as printed

   CHRISTOPH MATHEJA ,

   RWTH Aachen University

4. Christoph Matheja

   ETH Zurich

   Affiliation as printed

   ETH Zürich