Termination Analysis of Probabilistic Programs through Positivstellensatz's

• Algorithmic synthesis of nonlinear ranking supermartingales was unavailable even for probabilistic programs without nondeterminism, while prior approaches were limited to linear forms.Source: §1 · p. 3
• Polynomial ranking supermartingales extend linear ranking supermartingales and imply both almost-sure and finite termination.Source: §1 · p. 3
• Positivstellensatz-based synthesis avoids quantifier elimination and uses linear or semidefinite programming, yielding an efficient but incomplete method.Source: §1 · p. 3
• Experiments show synthesis on classical examples such as Gambler’s Ruin and Random Walk, where linear ranking supermartingales do not exist.Source: §1 · p. 3
• The paper uses Schmüdgen’s Positivstellensatz and Handelman’s Theorem to synthesize polynomial ranking functions for nonprobabilistic programs.Source: §1 · p. 4

2.1 Basic Notations and Concepts

• Polynomial predicates describe constraints over real-valued variables, while probability spaces, random variables, expectations, and filtrations provide the probabilistic notation.Source: §2.1 · pp. 4–5

2.2 Probabilistic Programs

• Programs include assignments, loops, conditional and probabilistic branches, demonic nondeterminism, and bounded random sampling over real-valued variables.Source: §2.2 · p. 5
• A control-flow graph represents program locations and transitions, with guards, probabilistic choices, nondeterministic choices, or update functions determining transition behavior.Source: §2.2 · p. 6
• Runs are sequences of configurations; schedulers resolve demonic choices and, together with random sampling, induce a probability measure over runs.Source: §2.2 · p. 7
• Bounded sampling ensures program-variable values remain bounded random variables, and polynomial invariants characterize reachable configurations.Source: §2.2 · p. 8

• Almost-sure termination requires termination with probability 1 under every scheduler, whereas finite termination requires finite expected termination time under every scheduler.Source: §3 · p. 8
• Finite termination implies almost-sure termination, but not conversely; the supremum of expected termination times across schedulers is denoted ET(P).Source: §3 · pp. 8–9
• A concentration bound M gives an exponential upper bound on the probability that termination time exceeds N for all N ≥ M.Source: §3 · p. 9
• The analysis takes a program, polynomial invariant, and initial configuration as input, and seeks termination judgments or a concentration bound.Source: §3 · p. 9

4 Polynomial Ranking-Supermartingale

• The pre-expectation uses probability-weighted successors for probabilistic transitions, a maximum for nondeterministic choices, and expected post-assignment values for sampling assignments.For conditional transitions it follows the uniquely enabled branch.Source: §4 · p. 10
• A d-pRSM is polynomial of degree at most d, nonnegative on invariant states, negative at the terminal location, and has an expected decrease of at least ε on continuing states.These conditions yield sound termination guarantees.Source: §4 · p. 11
• A d-pRSM proves almost-sure termination and bounds expected termination time by η(ℓ0,x0)−K.The theorem therefore supplies both termination conclusions from the same certificate.Source: §4 · pp. 11–12
• For the running example, a 2-pRSM with ε=0.2 and K=−0.2 gives almost-sure termination under any scheduler and an expected-time bound of 5·(x0−1)·(10−x0)+51 for the stated initial values.The initial valuation is assumed to satisfy 1≤x0≤10.Source: §4 · p. 11
• The running example does not admit a linear (1-) pRSM because ER(r) = 0 at label 3, indicating that linear pRSMs may not exist even for simple affine programs.Source: §4 · p. 11
• For a difference-bounded pRSM, bounded increments support a concentration bound on termination time.The section derives this result using Hoeffding’s inequality.Source: §4 · p. 12
• For any fixed degree d, existence of a d-pRSM or difference-bounded d-pRSM is decidable, although the stated procedure involves costly quantifier elimination.The section next develops more efficient synthesis algorithms.Source: §4 · p. 13

5 The Synthesis Algorithm

• The synthesis framework replaces quantifier elimination with Positivstellensatz reasoning, giving a sound but incomplete approach to termination and concentration analysis.Feasibility produces a pRSM, which certifies termination; a difference-bounded certificate also supports concentration analysis.Source: §5 · p. 13, §5.2 · p. 17
• The framework converts universally quantified pRSM conditions into polynomial-positivity implications over semialgebraic constraints.It over-approximates strict premise inequalities by non-strict ones; the section states that this does not affect the pRSM conditions.Source: §5 · p. 13

5.1 Positivstellensatz’s

• Schmüdgen and Putinar certificates yield linear equalities with positive-semidefinite matrix variables, while Handelman certificates yield linear equalities without semidefinite constraints.The Handelman construction bounds the number of multiplicands in monoid elements.Source: §5.1 · pp. 15–16

5.2 The Algorithm for pRSM Synthesis

• PRSMSynth sets a bounded-degree polynomial template, computes pre-expectations, extracts certificate constraints, and solves them by semidefinite or linear programming.The search can also optimize the expected-termination upper bound.Source: §5.2 · p. 17
• Every function synthesized by PRSMSynth is a valid pRSM, and linear predicates permit polynomial-time feasibility checking through Handelman’s theorem.The stated polynomial-time result applies when each propositional polynomial predicate involves only linear polynomials.Source: §5.2 · pp. 17–18
• For compact guards in the specified while-loop form, the procedure is semi-complete as certificate bounds increase, and the approach also introduces Schmüdgen and Handelman methods for nonprobabilistic programs.The program form uses a demonic branch between two single assignments, with DNF invariants containing no strict inequalities.Source: §5.2 · p. 18

Experimental results

• Across the examples, translations to optimization problems are linear, and the experiments report solver runtimes and synthesized pRSMs.The setup uses SOSTOOLS with SeDuMi and CPLEX; it checks numerical error for SOSTOOLS equalities.Source: §6 · pp. 18–19

Experimental examples and setup

• The six examples include Logistic Map, Decay, Random Walk, Gambler’s Ruin and its variant, and Nested Loop; the approach is semi-complete for all but the last two named exceptions.Source: §6 · pp. 18–19

• For every example except Logistic Map, prior approaches could not answer almost-sure termination; Logistic Map reduces to linear programming rather than semidefinite programming.Source: §6 · p. 20

7 Conclusion and Future Work

• Polynomial ranking supermartingales extend LRSMs to nondeterministic probabilistic programs and are sound for almost-sure and finite termination and concentration bounds.The synthesis algorithm is sound and semi-complete over an important class of programs; future work includes numerical methods for semidefinite programming and other RSM forms.Source: §7 · p. 20

A Propositional Polynomial Predicates

• Propositional polynomial predicates are built from polynomial constraints and true or false using negation, conjunction, and disjunction, with satisfaction defined over real vectors.Source: A Propositional Polynomial Predicates · p. 24

B Probabilistic Programs: Detailed Syntax

• Program syntax permits polynomial expressions and predicates, simultaneous assignments, sequencing, conditionals, and loops; sampling variables are used only on assignment right-hand sides.Sampling variables have associated distributions with bounded support and sampled values remain in that support with probability 1.Source: B Probabilistic Programs: Detailed… · pp. 24–25, Figure 3 · p. 25

C Transformation from Programs to CFGs

• Each probabilistic program is translated inductively into a control-flow graph with initial and terminal labels, representing assignments, sequences, loops, and conditional branches.Source: C Transformation from Programs to CFGs · p. 26

D The Semantics: Detailed Description

• Under a scheduler, execution samples variables independently of prior configurations, then follows demonic, probabilistic, deterministic-guard, or assignment transitions according to the current label.Source: D The Semantics: Detailed Description · pp. 26–27

• The conditional-expectation argument relies on polynomial assignments making the relevant expectations well-defined; the proof extends to other RSMs when that condition holds.Source: E Proof of Lemma 1 and Theorem 1 · pp. 27–28
• The proof invokes the RSM property that the process falls below zero almost surely, with an expected bound on the first time it does so.Source: E Proof of Lemma 1 and Theorem 1 · p. 29
• A difference-bounded pRSM implies almost-sure termination and bounds expected termination time by η(ℓ0,x0)−K.The proof uses the ranking-supermartingale conditions to obtain this guarantee.Source: E Proof of Lemma 1 and Theorem 1 · p. 29

• The shifted process Y_n is a supermartingale with bounded increments in [a + ǫ, b + ǫ], so it meets the stated requirements for Hoeffding’s inequality.Source: F Proof of Theorem 2 · p. 29
• On the event T_P > n, the shift parameters coincide, letting the proof bound P(T_P > n) by dropping that event from a probability involving X_n.Source: F Proof of Theorem 2 · p. 30
• The resulting tail bound applies to general difference-bounded ranking supermartingales, not only polynomial ones.Source: F Proof of Theorem 2 · p. 30

• The difference-bounded conditions can likewise be encoded in first-order real arithmetic, so existence is decidable.Source: G Proof for Theorem 3 · p. 31
• A d-pRSM is represented by a template over all monomials of degree at most d, with scalar coefficients to solve for.Source: G Proof for Theorem 3 · p. 31
• The pRSM conditions are encoded by existentially quantifying the template coefficients, K, and ǫ, then universally quantifying over the state vector.Source: G Proof for Theorem 3 · p. 31

• Every function synthesized by PRSMSynth is a valid pRSM.Source: H Proof of Theorem 7 · p. 31
• The algorithm instantiates a polynomial template, computes pre-expectations, and uses Positivstellensatz conditions to establish the required inequalities.Source: H Proof of Theorem 7 · p. 31
• The soundness argument applies regardless of whether the invariant-defined state set is compact.Source: H Proof of Theorem 7 · p. 31

• The examples use bracketed invariants attached to program labels, which the text says are straightforward to obtain directly from each program.Source: I Experimental Details · p. 31
• The Logistic Map example uses a bounded logistic update, while Decay is a discretized randomized version of an ODE describing exponential convergence to the origin.Source: I Experimental Details · pp. 31–32
• The Random Walk example uses a bounded region defined by nonlinear parabolas rather than linear constraints.Source: I Experimental Details · p. 32
• The Gambler’s Ruin Variant is an affine program without a linear ranking supermartingale; Nested Loop has two independent loop-control variables.Source: I Experimental Details · p. 33