Probabilistic Program Analysis using Martingale Theory

Probabilistic programs are standard imperative programs enriched with constructs to generate random values according to a pre-specified distribution. Such programs are common in a variety of application domains, including risk assessment, biological systems, sensor fusion algorithms and randomized algorithms. We present deductive techniques for the analysis of infinite state probabilistic programs to synthesize probabilistic “invariants” and prove almost-sure termination. Our analysis is based on the notion of martingales and super martingales from probability theory.
First, we define the concept of (super) martingales for loops in probabilistic programs, and present analogies between super martingales and inductive invariants. We then use concentration of measure inequalities to bound the values of martingales with high probability. This directly allows us to infer probabilistic bounds on assertions involving the program variables. Using the notion of a super martingale ranking function (SMRF), we prove almost sure termination of probabilistic programs. We extend constraint-based approaches for synthesizing inductive invariants to also synthesize martingales and super-martingale ranking functions for probabilistic programs. We present some applications of our approach to reason about invariance and termination of some probabilistic program benchmarks.
Joint work with Aleksandar Chakarov, University of Colorado Boulder.