Sound and Complete Proof Rules for Probabilistic Termination

TL;DR

This paper introduces sound and relatively complete proof rules for probabilistic termination, using supermartingales and variants, applicable to programs with nondeterminism and probabilistic choices, advancing the theoretical foundation of program analysis.

Contribution

It provides the first sound and relatively complete proof systems for qualitative and quantitative probabilistic termination using supermartingales, with practical applicability demonstrated.

Findings

Constructed supermartingales from almost-surely terminating programs

Proved soundness and relative completeness of the proof rules

Applied rules to prove termination of a two-dimensional random walker

Abstract

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 such sound and relatively complete proof rules for proving qualitative and quantitative termination in the assertion language of arithmetic. Our rules use supermartingales as estimates of the likelihood of a program's evolution and variants as measures of distances to termination. Our key insight is our completeness result, which shows how to construct a suitable supermartingales 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.