salle A. Turing CE4
11 juillet 2013 - 14h00
Invariance and Termination for Probabilistic Programs using Martingales.
par Sriram Sankaranarayanan de University of Colorado at Boulder
Abstract: 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. We then turn our attention to almost sure termination of probabilistic programs. 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.
Note: The talk will try to be self-contained. No prior knowledge of martingale theory is assumed.
