Sound and Complete Proof Rules for Probabilistic Termination

TL;DR

The paper tackles termination analysis for probabilistic programs with discrete probabilistic choice and bounded nondeterminism by introducing sound and relatively complete proof rules for both qualitative ${\mathsf{AST}}$ and quantitative termination, all formulated in an arithmetic assertion language. It leverages supermartingales and distance-variant certificates to provide certificate-based proof systems whose completeness is relative to the completeness of ${\mathsf{Th}(\mathbb{Q})}$; a key contribution is a constructive completeness framework that can express and manipulate certificates within arithmetic, enabling a unifying approach that subsumes many existing rules. The authors develop an explicit ${\mathsf{AST}}$ proof for the 2D random walker as a nontrivial application, and show how their rules can simulate and extend prior methods (e.g., McIver–Morgan, McIver–MKK18) while maintaining practical interpretability of certificates. Overall, the work provides a foundational, machine-checkable framework for certifying termination properties in infinite-state probabilistic programs, with implications for verification tooling and automatic certificate synthesis.

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.

Figures (5)

• Figure 1: The 2D symmetric random walker. The symbol $\oplus$ is a probabilistic choice operator.
• Figure 1: An element $n_i$ in the diagonal sequence. The states are ordered from left to right according to the enumeration $\mathsf{Enum}$; accordingly, $\sigma_0$, highlighted in green, is the terminal state. The arrows indicate probabilistic/nondeterministic/assignment transitions between the states. The yellow state space contains states indexed $\leq i$, and the red space contains states indexed $\geq n_i$. The probability of a run beginning from inside the yellow state space reaching the red space is $\leq 1/2^i$. Importantly, $n_i$ is the smallest such state index; meaning that if the red region included $\sigma_{n_i - 1}$, the aforementioned probability inequality will not hold.
• Figure 2: The long tail end, an $\mathsf{AST}$ program for which synthesizing a supermartingale variant is difficult. We refer to the second loop at Line \ref{['line:tel-loop-2']}, which corresponds to the right-half of the transition system, as the tail end loop of the program. The final/terminal state is shown in red.
• Figure 3: If shortest runs of $\Sigma_{good}$ were too long. This is a representation of the collection of executions beginning at a good state $\sigma \in \Sigma_{good}$, according to the partitioning system suggested in the proof of \ref{['lem:SI-lower-bounds-partial-completeness']}. The black nodes are the terminal states; they all lead to the single terminal state. The blue states are identical to each other; the same holds for the blue green states. The pathological scheduler $\mathfrak{s}'$ always takes the red back edges, rendering no terminal runs from $\sigma$.
• Figure 4: Counterexample to the SI-rule for lower bounds. With an initial state of $(l_1, (1, 2, 1/4))$, the termination probability of this program is $1/2$. However, there is no SI that shows this.

Theorems & Definitions (24)

• definition 1: Control Flow Graphs
• Remark 1
• theorem 2: doobBook
• definition 2: Termination Probability
• lemma 1: Unrolling Lemma MS24arxiv
• corollary 1
• theorem 3: Robinson49
• lemma 2
• lemma 3: McIverMorganBook
• lemma 4: Soundness