Source-linked AI summary
Stochastic Invariants for Probabilistic Termination
Krishnendu Chatterjee, Petr Novotný, Đorđe Žikelić
TL;DR
The paper takes up the quantitative question of bounding termination probability, beyond asking whether termination occurs almost surely. It combines stochastic invariants with repulsing supermartingales, showing applications to termination bounds, almost-sure termination refutation, and persistence.
Problem
Almost-sure termination asks whether a program terminates with probability 1, whereas probabilistic termination asks for a lower bound on its termination probability.
Source: §1 · p. 1Method
The paper pairs locationwise constraints with probability thresholds as stochastic invariants and introduces RepSMs to bound their violation probabilities.
Source: §1 · pp. 2–3Results
Combining RSMs and RepSMs yields lower termination-probability bounds, while RepSMs witness refutations of almost-sure termination and infinite expected termination time.
Source: §1 · p. 3Takeaways & Limitations
Combining RSMs and RepSMs also establishes persistence properties of probabilistic programs.
Source: §1 · p. 3The termination-probability bound is sound but not necessarily tight, and its magnitude depends on the RepSM and the initial variable valuation.
Source: §5 · p. 10
Abstract
from arXiv · showhide
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. 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. In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We define the notion of {\em stochastic invariants}, which are constraints along with a probability bound that the constraints hold. We introduce a concept of {\em 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. We also present results on related computational problems and an experimental evaluation of our approach on academic examples.
1. Introduction
The paper addresses probabilistic termination, where the goal is to bound termination probability, and the limitation that existing RSM-based methods use invariants that ignore probabilistic behavior. It introduces stochastic invariants and repulsing supermartingales (RepSMs), then develops their applications and computational methods.
Motivation
- Existing RSM approaches use invariants that hold along all executions and ignore probability, limiting their ability to address probabilistic termination.An invariant over-approximates reachable configurations; the quantitative problem instead seeks termination-probability bounds.Source: §1 · p. 2
Contributions
- A stochastic invariant pairs a constraint at each program location with a bound on its violation probability; the example uses x ≤100 with a threshold below 10^-5.In the random walk example, x can exceed 100, but the paper says this happens with very low probability due to asymmetry.Source: §1 · p. 2
- A RepSM is non-negative inside a configuration set and decreases on average outside it, capturing how executions starting outside tend to avoid and move away from that set.The paper describes RepSMs as dual in some sense to ranking supermartingales.Source: §1 · p. 3
- Combining RSMs and RepSMs yields lower bounds on termination probability and establishes persistence, while RepSMs witness refutations of almost-sure termination and infinite expected termination time.The termination bounds apply to programs that may not terminate almost-surely but terminate with high probability.Source: §1 · p. 3
Computational and Experimental Results
- Given strict invariants and polyhedral stochastic constraints, existence of a linear RepSM is decidable in polynomial time via LP; stochastic-invariant synthesis reduces to the existential theory of reals.The paper also reports academic-example experiments as validation of its new concepts.Source: §1 · p. 3
2. Preliminaries
The preliminaries define the mathematical notation and affine probabilistic programs used in the paper, give their probabilistic-control-flow semantics, and formalize almost-sure and probabilistic termination.
2.1 Basic Notions, Linear Predicates, Valuations
- The preliminaries define affine expressions, linear constraints and assertions, and propositionally linear predicates as finite disjunctions of linear assertions.Vectors are compared componentwise, and affine expressions evaluate by substituting vector components for variables.Source: §2.1 · p. 3
2.2 Syntax of Affine Probabilistic Programs (APPs)
- APPs use real-valued variables, affine tests and assignments, probabilistic choices and sampling, and nondeterministic branching or assignment.Programs are preceded by an initialization that assigns each variable a concrete number.Source: §2.2 · pp. 3–4
2.3 Semantics of Affine Probabilistic Programs
- A pCFG represents finite control locations, program variables, transitions, probability distributions, and guards, defining program behavior over real-valued configurations.The semantics treat programs as uncountable-state-space MDPs and associate a stochastic process with each program.Source: §2.3 · p. 4
- Schedulers resolve nondeterministic choices, while probabilistic locations use their specified distributions; together they induce a probability measure over runs.A scheduler also specifies distributions for assignments from sets at deterministic locations.Source: §2.3 · pp. 4–5
2.4 Almost-Sure and Probabilistic Termination
- Almost-sure termination requires termination with probability 1 under every scheduler; probabilistic termination seeks a lower bound on termination probability under every scheduler.The same probability questions are also defined for reaching a set of configurations.Source: §2.4 · p. 5
3. Invariants and Ranking Supermartingales
The section recalls pure invariants and ranking supermartingales as tools for proving qualitative termination, then shows why they cannot establish high-probability termination when termination is not almost sure. Its example motivates extending invariants with probabilistic bounds.
3.1 Pure Invariants
- Pure invariants assign each program location a predicate that holds whenever that location is reached along a finite execution path.The paper distinguishes these from the stochastic invariants introduced later.Source: §3.1 · p. 6
3.2 Supermartingales
- A ranking supermartingale decreases by at least ε in expectation until its stopping condition, while remaining nonnegative before that condition is reached.The paper also treats reachability times, not only termination, as stopping conditions.Source: §3.2 · p. 6
- An ε-linear ranking supermartingale supported by a pure invariant proves almost-sure termination and bounds expected termination time by its initial value divided by ε.The theorem applies under each scheduler.Source: §3.2 · p. 7
- In Figure 3, termination is high-probability but not almost sure, so no positive-ε ranking supermartingale supported by a pure invariant can prove that high-probability termination.The example's probabilistic trend is that x increases on average while y decreases; a rare sequence can instead trap execution in the inner loop.Source: §3.2 · p. 7, Figure 3 · p. 7
4. Stochastic Invariants and Probabilistic Termination
Stochastic invariants attach a probability bound to constraints on program variables, addressing the limits of pure invariants for probabilistic termination. Combined with a ranking supermartingale, they yield lower bounds on reaching a target, including a worked bound of 0.99999.
Stochastic invariants
- A stochastic invariant pairs location-wise linear constraints with a bound p on the probability that any execution under any scheduler violates them.The paper defines the probability over runs that reach a configuration violating the constraint.Source: §4 · p. 7
Probabilistic reachability
- If a target has an ε-ranking supermartingale supported by constraints entailed by stochastic invariants with bounds p1 through pn, its reachability probability is at least 1 − Σpj.The theorem holds under each scheduler.Source: §4 · p. 8
- A worked example combines a pure invariant with a stochastic invariant bounded by 10^-5 to prove termination probability of at least 0.99999.The ranking supermartingale is supported by the conjunction of the two invariants.Source: §4 · p. 8
Repulsing supermartingales
- Pure linear invariant methods do not reason about assertion probabilities, so the paper proposes repulsing supermartingales to establish stochastic invariants.The stochastic-invariant and ranking-supermartingale result makes finding such invariants a key step in proving probabilistic termination.Source: §4 · p. 8
5. Proving Stochastic Invariance with Repulsing Supermartingales
The section develops repulsing supermartingales (RepSMs) to bound stochastic-invariant violations. Combined with ranking supermartingales, these bounds support probabilistic termination analysis.
Applying stochastic invariants to termination
- The section’s construction combines a ranking supermartingale for termination time with an upper bound on the probability that the stochastic predicate map is violated.The authors identify obtaining a probabilistic bound on predicate-map failure as the more difficult task.Source: §5 · p. 8
Repulsing supermartingales
- A RepSM decreases on average until a target set is reached and must be non-negative upon reaching it, rather than throughout the run.For an ǫ-LRepSM, the conditions also require a supported predicate map and an expected decrease of at least ǫ outside the target set.Source: §5 · p. 8
From linear to stochastic RepSMs
- An LRepSM can be converted into a stochastic process that is an ǫ-RepSM until the target set is reached, or until the supporting invariant fails.When the supporting predicate map is a pure invariant, the process is an ǫ-RepSM for the target set itself.Source: §5 · p. 9
Bounding reachability
- Azuma’s inequality gives an exponentially decreasing bound on reaching the target set in exactly n steps when the RepSM has bounded differences and starts below zero.Summing the stepwise bounds gives a geometric-series upper bound on the probability of reaching the set.Source: §5 · p. 9
Illustration
- 5.06 · 10^-6 bounds the probability of violating PI in the illustrated program example.The example applies Azuma’s inequality and Theorem 4 using a per-step change bound of 12 and initial value −3429.Source: §5 · p. 10
Stochastic-invariant probability bounds
- RepSM bounds yield a stochastic invariant with probability at least 1−γ when an LRepSM for violations of PI meets the stated bounded-differences and initial-value conditions.The bound is sound but not necessarily tight, and depends on the RepSM and initial valuation.Source: §5 · p. 10
6. Effectiveness of Repulsing Supermartingales
The section applies RepSMs to probabilistic termination, termination refutation, and persistence. Its results combine RepSMs with ranking supermartingales where needed, and also use optional stopping for refutation.
6.1 Probabilistic Termination
- Combining stochastic invariants with ranking supermartingales provides bounds for probabilistic termination.The section presents this combination as an answer to the probabilistic termination problem.Source: §6.1 · p. 10
6.2 Refuting Almost-Sure and Finite Termination
- RepSMs can refute almost-sure termination even when the bound from Theorem 4 is at least 1, while 0-RepSMs can refute finite termination.Finite termination means the expected termination time is finite; the section notes that almost-sure termination need not imply finite termination.Source: §6.2 · p. 10
6.3 Proving Almost-Sure Persistence
- A set C is almost-surely persistent when ranking and repulsing supermartingales satisfy the stated conditions for C and a related set D.The proof idea gives each entry into D a positive, configuration-independent chance of never returning to the complement of C.Source: §6.3 · p. 11
7. Computational Results
The section develops algorithms for computing stochastic invariants and synthesizing ranking and repulsing supermartingales. It reduces fixed-input synthesis to linear constraints and joint invariant synthesis to quadratic systems.
7. Computational Results
- For stochastic-invariant computation, the method can use a pure invariant and a linear predicate map, or seek a predicate map supporting an LRSM for a chosen configuration set.The latter setup assumes the configuration set is represented by a linear predicate map; terminal configurations can be represented this way.Source: §7 · pp. 11–12
- For polyhedral predicates, computing a probability bound for a stochastic invariant reduces to synthesizing a bounded-difference LRepSM for its complement.The method searches over several difference bounds and selects the resulting probability bound that is smallest.Source: §7 · pp. 11–12
- The LRSM synthesis system is solvable exactly when the corresponding bounded-difference LRSM exists, and can be constructed in polynomial time when the configuration set is polyhedral.A system solution yields an LRSM; an unsolvable system rules one out.Source: §7 · pp. 11–12
- LRepSM synthesis for the complement of a polyhedral predicate uses linear constraints and is complete for bounded-difference LRepSM existence.The constraints differ from LRSM synthesis in requiring non-negativity inside, rather than outside, the target set.Source: §7 · p. 12
- Jointly synthesizing an invariant and supporting LRSM and LRepSM yields quadratic systems reducible to existential theory of the reals, decidable in PSPACE.The shared unknown invariant coefficients parameterize both systems; the LRSM system encodes the target set and the LRepSM system its complement.Source: §7 · p. 12
- The computational section identifies Table 1 as reporting experimental results, without specifying its values in the supplied text.The algorithms described use linear programming for fixed polyhedral inputs and a heuristic search over difference bounds for tighter probability bounds.Source: §7 · p. 12, Table 1 · p. 13
8. Experimental Results
The experiments apply the approach to three academic probabilistic-program examples and compute probability thresholds for selected initial configurations. The authors describe the experiments as basic validation of the concepts.
8. Experimental Results
- The experiments are presented as basic validation of the new concepts, rather than as the paper’s main contribution.The authors identify the conceptual and algorithmic contributions as primary.Source: §8 · p. 13
- The three examples cover a one-dimensional walk that loses almost-sure termination above a threshold, a two-dimensional walk with a low-probability trapping event, and a three-dimensional process with non-proportional updates.The third program terminates almost-surely, but computing the probability bound for its predicate map remains nontrivial.Source: §8 · p. 13
- For various initial configurations, the method computes probability thresholds for given linear predicate maps, reported in Table 1.The text says the resulting linear programs can be solved with standard solvers, including lpsolve and CPlex.Source: §8 · p. 13
9. Related Work
The related work spans probabilistic logics, termination analysis, martingale methods, and probability-of-assertion analysis. The paper distinguishes its approach by addressing quantitative termination with stochastic invariants for infinite-state probabilistic programs.
9. Related Work
- Earlier probabilistic logics include PROB-DL for restricted loop structures and PrDl for first-order reasoning about assertions and their probabilities.Decidable propositional fragments were studied in.Source: §9 · p. 13
- Prior probabilistic termination work includes discrete-choice methods and studies of almost-sure termination; the paper contrasts these with its quantitative focus and stochastic invariants.The paper states that earlier infinite-state work with nondeterminism addressed the qualitative problem, while its results target probabilistic termination for infinite-state programs.Source: §9 · pp. 13–14
- Martingales have also been used to bound expected termination time and to define expectation invariants, whereas stochastic invariants reason about the probability that an assertion holds.Source: §9 · p. 14
- Other assertion-probability approaches use optimized simulation, symbolic execution, or finite Markov-chain and MDP abstractions.The paper says RepSMs need neither abstraction nor simulation, while suggesting they could be combined with abstraction methods.Source: §9 · p. 14
- Ranking supermartingales generalize ranking functions from non-probabilistic termination analysis, but probabilistic termination requires additional concepts and methods.The cited non-probabilistic approaches include.Source: §9 · p. 14
10. Conclusion and Future Work
The paper presents stochastic invariants and repulsing supermartingales as tools for quantitative probabilistic termination. It identifies nonlinear repulsing supermartingales and practical stochastic-invariant synthesis as directions for future work.
10. Conclusion and Future Work
- The paper addresses probabilistic termination by introducing stochastic invariants and repulsing supermartingales.Source: §10 · p. 14
- One future direction is to study polynomial repulsing supermartingales and whether efficient algorithms can be developed for them.Source: §10 · p. 14
- Another future direction is practical synthesis of stochastic invariants, since the theoretical results use existential first-order theory of the reals.Source: §10 · p. 14
Supplementary Material
The supplementary material details the affine probabilistic program model, its probabilistic control-flow representation, and examples illustrating the Section 3 definitions.
A. Details of Section 2
- For unary PLPs, the valuation set can be identified with the corresponding set of numbers satisfying the constraint.Finite-valued random variables can likewise be represented by identifying their values with distinct real numbers.Source: A. Details of Section 2 · p. 17, §A.2 · p. 17
A.1 Details of Section 2.2
- APPs allow affine expressions and propositionally linear predicates, with assignments that may be nondeterministic and branches that may be demonic, probabilistic, or deterministic.Programs start from concrete initialized variables; distributions are characterized for analysis by their expectation and a linear constraint containing their support.Source: §A.1 · p. 17
A.2 Details of Section 2.3
- Each program is translated inductively into a pCFG whose locations represent program-counter values and whose transitions capture program behavior.The construction handles assignments, sequential composition, loops, and conditionals; conditional branching gives locations at most two successors.Source: §A.2 · pp. 17–18
B. Details of Section 3
- The examples illustrate a pure linear invariant and a supermartingale for an asymmetric one-dimensional random walk.The examples also show a ranking supermartingale construction and how whether it qualifies can depend on the supporting invariant.Source: B. Details of Section 3 · p. 18
- The examples use pre-expectations to evaluate expected values and illustrate linear ranking supermartingales for terminal configurations supported by invariants.The text contrasts an invariant-supported terminal set with an invariant that assigns true at every location.Source: B. Details of Section 3 · p. 18
C.1 Proof of Lemma 1 and Lemma 2
The proof establishes that the constructed process preserves the ranking-supermartingale property up to the target or invariant violation, while retaining bounded differences when present.
C.1 Proof of Lemma 1 and Lemma 2
- Replacing the process after the stopping time with a fixed negative value preserves its ranking-supermartingale property for the target-or-invariant-violation stopping time.If the invariant is pure, violation never occurs, so this stopping time reduces to the target hitting time.Source: §C.1 · pp. 18–19
- The constructed process remains adapted and integrable because each state variable has finite expectation at every step.The induction uses affine updates, finite distribution expectations, and integrable distributions for nondeterministic assignments.Source: §C.1 · pp. 18–19
- Before the stopping time, conditional expected updates are bounded by the ranking function's pre-expectation, which decreases by ε; after stopping, the process is held at its prior value.This establishes the required conditional decrease for the stopped process.Source: §C.1 · p. 19
C.2 Proof of Theorem 2
The proof derives the hitting-time guarantee for ranking supermartingales by modifying the process after the target is reached. This removes an additional bounded-below assumption used in earlier work.
C.2 Proof of Theorem 2
- An ε-ranking supermartingale for a target set implies that the set is reached almost surely and has expected hitting time less than Eσ[X0]/ε.The theorem applies to a general set of configurations and does not require the additional lower-bound condition described for the earlier result.Source: §C.2 · pp. 19–20
- The proof removes the earlier requirement that the ranking supermartingale be almost surely bounded below by stopping and modifying the process.The earlier theorem also concerned terminal configurations and used a different decrease-until condition; both differences are addressed in adapting the result.Source: §C.2 · pp. 19–20
- After the target is reached, the modified process takes value −ε, preserving the ranking-supermartingale decrease condition and the needed boundedness.The proof checks the cases before, at, and after the hitting time to establish the conditional-expectation requirement.Source: §C.2 · pp. 19–20
C.3 Proof of Theorem 6
The proof uses a repulsing supermartingale with bounded differences to establish a positive-probability escape from the target under any scheduler.
C.3 Proof of Theorem 6
- From an initial configuration with η < 0, the proof establishes that every scheduler has positive probability of reaching a configuration with η ≤ −z·c.It reduces the claim to reaching that level before the target, using a ranking supermartingale for the combined stopping set.Source: §C.3 · p. 20
- The proof applies optional stopping to the shifted ranking supermartingale at the combined target-or-low-η stopping time.The shift preserves c-bounded differences, and the stopping time is finite almost surely under the derived ranking-supermartingale argument.Source: §C.3 · p. 20
- The probability of reaching a sufficiently high η-value is bounded away from zero by a quantity depending on c, z, and the initial η-value.This follows from the stated expectation comparison involving the probability of reaching C and the c-bounded-difference condition.Source: §C.3 · p. 20