Sound and Complete Proof Rules for Probabilistic Termination
This program is tentative and subject to change.
Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete probabilistic choice and demonic bounded nondeterminism. The qualitative question asks if the program terminates almost-surely, no matter how nondeterminism is resolved. The quantitative question asks for a bound on the probability of termination. Despite a long and rich literature on the topic, no sound and relatively complete proof systems were known for these problems. In this paper, we provide sound and relatively complete proof rules for proving qualitative and quantitative termination in the assertion language of arithmetic. Our rules use variant functions as measures of distances to termination as well as supermartingales that restrain the growth of these variants almost surely. Our completeness result shows how to construct suitable supermartingale and variant functions from an almost-surely terminating program. We also show that proofs of termination in many existing proof systems can be transformed to proofs in our system, pointing to its applicability in practice. As an application of our proof rule, we show an explicit proof of almost-sure termination for the two-dimensional random walker.
This program is tentative and subject to change.
Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change
15:00 - 16:20 | |||
15:00 20mTalk | A quantitative probabilistic relational Hoare logic POPL Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Benjamin Gregoire INRIA, Davide Davoli Université Côte d’Azur, Inria | ||
15:20 20mTalk | Approximate Relational Reasoning for Higher-Order Probabilistic Programs POPL Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University Pre-print | ||
15:40 20mTalk | Compositional imprecise probability: a solution from graded monads and Markov categories POPL | ||
16:00 20mTalk | Sound and Complete Proof Rules for Probabilistic Termination POPL |