Relatively Complete Verification of Probabilistic Programs

TL;DR

This paper introduces a syntax for specifying and verifying quantitative assertions in probabilistic programs, demonstrating its expressiveness and providing a relatively complete verification system for expected values and probabilities.

Contribution

The paper presents a new expressive syntax for probabilistic assertions and proves its relative completeness for verifying expected values in probabilistic programs.

Findings

The syntax can express the weakest preexpectation functions for any probabilistic program.

The verification system can determine inequalities between expected values using syntactic expressions.

The approach achieves relative completeness in probabilistic program verification.

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 $\sigma$ to the expected value of $f$ evaluated in the final states reached after termination of $C$ on $\sigma$ (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)$.