Sound and Complete Proof Rules for Probabilistic Termination

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.