POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 15:10 - 15:35 at Amphitheater 44 - Probabilistic Programming Chair(s): Marco Gaboardi

Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability 1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability, and this problem has not been addressed yet. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider the probabilistic behavior of the programs, the invariants are obtained completely ignoring the probabilistic aspect (i.e., the invariants are obtained considering all behaviors with no information about the probability).

In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We formally define the notion of stochastic invariants, which are constraints along with a probability bound that the constraints hold, for the probabilistic termination problem. We introduce a new concept of repulsing supermartingales. First, we show that repulsing supermartingales can be used to obtain bounds on the probability of the stochastic invariants. Second, we show the effectiveness of repulsing supermartingales in the following three ways: (1) With a combination of ranking and repulsing supermartingales we can compute lower bounds on the probability of termination; (2) repulsing supermartingales provide witnesses for refutation of almost-sure termination; and (3) with a combination of ranking and repulsing supermartingales we can establish persistence properties of probabilistic programs.

Along with our conceptual contributions, we establish the following computational results: First, the synthesis of a stochastic invariant which supports some ranking supermartingale and at the same time admits a repulsing supermartingale can be achieved via reduction to the existential first-order theory of reals, which generalizes existing results from the non-probabilistic setting. Second, given a program with ``strict" invariants'' (e.g., obtained via abstract interpretation) and a stochastic invariant, we can check in polynomial time whether there exists a linear repulsing supermartingale wrt the stochastic invariant (via reduction to LP). We also present experimental results on academic examples of our approach.

Wed 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Probabilistic ProgrammingPOPL at Amphitheater 44
Chair(s): Marco Gaboardi SUNY Buffalo, USA
14:20
25m
Talk
Beginner's Luck: A Language for Property-Based Generators
POPL
Leonidas Lampropoulos University of Pennsylvania, Diane Gallois-Wong Inria Paris, ENS Paris, Cătălin Hriţcu Inria Paris, John Hughes Chalmers University of Technology, Benjamin C. Pierce University of Pennsylvania, Li-yao Xia ENS Paris
Pre-print
14:45
25m
Talk
Exact Bayesian Inference by Symbolic Disintegration
POPL
Chung-chieh Shan Indiana University, USA, Norman Ramsey
Pre-print
15:10
25m
Talk
Stochastic Invariants for Probabilistic Termination
POPL
Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge
15:35
25m
Talk
Coupling proofs are probabilistic product programs
POPL
Gilles Barthe IMDEA, Benjamin Gregoire INRIA, Justin Hsu , Pierre-Yves Strub École Polytechnique