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

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 𝐶, if a function 𝑓 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 𝐶 on 𝜎 (also called the weakest preexpectation wp 𝐶 (𝑓 )) 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 𝑓 , 𝑔, and 𝐶, we can check whether 𝑔 ⪯ wp 𝐶 (𝑓 ). February 1, 2022: This is a revised version, correcting technical issues in the proofs of Theorem 8.4 and 9.4. * Batz and Katoen are supported by the ERC AdG 787914 FRAPPANT.