Invariance and Almost-Sure Termination Analysis for Probabilistic Programs
University of Colorado Boulder, USA.
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
Joint work with Aleksandar Chakarov, University of Colorado Boulder.