A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations

Benjamin Kaminski (RWTH Aachen)

When: Wednesday, October 19, 2pm

Where: room C417 (at the very end of the corridor)

Abstract

This paper presents a weakest-precondition-style calculus for reasoning about the expected values (pre-expectations) of 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 and present an invariant-based approach for reasoning about pre-expectations of loops. Finally, we give an insight on how our calculus could be applied in amortized analysis of randomized algorithms, where the expected change of a potential can possibly be positive or negative.