Expectation Invariants for Probabilistic Program Loops as Fixed Points

Abstract. We present static analyses for probabilistic loops using expectation in-variants. Probabilistic loops are imperative while-loops augmented with calls to random variable generators. Whereas, traditional program analysis uses Floyd-Hoare style invariants to over-approximate the set of reachable states, our ap-proach synthesizes invariant inequalities involving the expected values of pro-gram expressions at the loop head. We first define the notion of expectation invari-ants, and demonstrate their usefulness in analyzing probabilistic program loops. Next, we present the set of expectation invariants for a loop as a fixed point of the pre-expectation operator over sets of program expressions. Finally, we use exist-ing concepts from abstract interpretation theory to present an iterative analysis that synthesizes expectation invariants for probabilistic program loops. We show how the standard polyhedral abstract domain can be used to synthesize expecta-tion invariants for probabilistic programs, and demonstrate the usefulness of our approach on some examples of probabilistic program loops.