A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations

TL;DR

This paper introduces a new semantics for reasoning about the expected values of mixed-sign, unbounded random variables in probabilistic programs, ensuring well-definedness even when expectations do not exist.

Contribution

It develops a weakest-precondition calculus for mixed-sign expectations with a well-defined semantics for loops, extending traditional fixed-point methods.

Findings

Semantics is always well-defined, even if expectations do not exist.

The calculus is sound and supports compositional reasoning.

An invariant-based approach for loop pre-expectations is presented.

Abstract

We present a weakest-precondition-style calculus for reasoning about the expected values (pre-expectations) of \emph{mixed-sign unbounded} random variables after execution of a probabilistic program. The semantics of a while-loop is well-defined as the limit of iteratively applying a functional to a zero-element just as in the traditional weakest pre-expectation calculus, even though a standard least fixed point argument is not applicable in this context. A striking feature of our semantics is that it is always well-defined, even if the expected values do not exist. We show that the calculus is sound, allows for compositional reasoning, and present an invariant-based approach for reasoning about pre-expectations of loops.