PaperlayerView exact revision on arXiv

Source-linked AI summary

Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support

Anne Schreuder, Lorenz Winkler, Laura Kovács, C. -H. Luke Ong

arXiv:2609.02446v1cs.LO

TL;DR

The paper addresses polynomial-invariant synthesis for probabilistic transition systems when termination occurs at a random stopping time and sampled distributions may have unbounded support. It introduces the dui precondition for applying the Optional Stopping Theorem, simplifies verification for linear loops to runtime-moment bounds, and uses the resulting invariants to derive post-termination moment bounds. The method applies to examples beyond existing bounded-support approaches, but requires prior finiteness proofs and is not complete.

  • Problem

    Polynomial expressions need not preserve expected value at random termination because stopping times and updates can have problematic tails or behavior.

  • Method

    The paper applies the Optional Stopping Theorem through dui, an integrable-dominating-function precondition, and derives tractable polynomial-invariant conditions for linear loops.

  • Results

    The approach automatically synthesises OST-valid polynomial invariants and derives bounds for higher- and mixed-moments of variables and runtime after termination, including unbounded-support examples.

  • Takeaways & Limitations

    Finite sample moments plus a suitable runtime-moment bound enable polynomial invariant synthesis for linear loops with unbounded-support sampling.

  • Takeaways & Limitations

    The method makes no completeness claim and requires potentially manual proofs of stopping-time finiteness; its bound generation also uses restricted subsumption checks.

Abstract

from arXiv · show

We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. We do this by applying the Optional Stopping Theorem (OST) in the form of a specific precondition. This precondition requires the existence of an integrable dominating function for the martingale expression, which implies uniform integrability; we refer to this condition as dui. For linear PTS we simplify the dui property to proving finiteness of the expected value of an expression depending on the update matrix, the degree of the martingale expression, and the stopping time. Specifically, if all random samples have finite moments and we can verify a moment bound on the runtime of a linear loop, then we can automatically synthesise polynomial loop invariants that satisfy the OST. Notably, dui allows for the sampled distributions to have unbounded support, which is a novel contribution to the field.

1 Introduction

The paper develops martingale-based polynomial invariants for probabilistic programs with unbounded-support sampling, using a flexible OST precondition and applying it to linear loops. The approach synthesises invariants and derives termination-time and variable-moment bounds, while requiring prior finiteness proofs for stopping times.

  • Problem setting: Probabilistic programs are modeled as PTSs that may sample from continuous distributions with unbounded support.The framework covers standard imperative programs with random samples and nested loops.
  • OST precondition: The dui precondition requires an integrable dominating function, implying uniform integrability without imposing a priori restrictions on runtime, variables, or updates.It is presented as a flexible OST precondition for martingale expressions.
  • Linear-loop synthesis: For polynomial martingales of simple linear loops, checking dui reduces to proving finiteness of stopping-time moments.The sufficient condition requires identically distributed samples with all moments finite and a runtime bound depending on polynomial degree and update-matrix structure.
  • Bound generation: The method constructs OST-valid martingale expressions from the number of finite stopping-time moments and derives upper and lower bounds for terminated variable moments.It includes variables with negative, state-dependent, unbounded increments.
  • Scope and evaluation: The implementation handles examples with unbounded-support distributions, but does not claim completeness and requires potentially manual proofs that stopping-time moments are finite.The implementation is built on the Polar analyser and evaluated on programs with unbounded support.

2 Probabilistic Transition Systems and Invariants

The paper models probabilistic programs as probabilistic transition systems and defines polynomial invariants through step-wise expectation preservation. Because random runtimes can invalidate this property at termination, soundness requires an Optional Stopping Theorem precondition.

  • Probabilistic Transition Systems: PTS represent imperative programs with deterministic variables, random samples, locations, guards, and polynomial updates.Samples are assumed independent, identically distributed over time, known, and finite-moment.
  • Probabilistic Transition Systems: A PTS computation repeatedly enables a unique guarded transition, draws fresh random samples, applies its update, and stops upon reaching the final location.The runtime is the first step at which the final location is reached.
  • Probabilistic Invariants: Probabilistic invariants are location-independent polynomials whose expected value is preserved from one computation step to the next.Their step-wise condition is expressed using the pre-expectation operator.
  • Probabilistic Invariants: Unlike deterministic programs, a step-wise invariant need not preserve its expectation at a random termination time.The martingale betting example has E(M0) = 0 but E(MT ) = 1, so it is not a loop invariant.
  • Probabilistic Invariants: The Optional Stopping Theorem provides the precondition needed to make step-wise martingale invariants sound at program termination.This supplies the probabilistic justification for equating initial and terminal expectations.

3 Martingales and the Optional Stopping Theorem

The paper treats martingales as probabilistic invariants and uses the Optional Stopping Theorem to justify their values at random termination. It introduces dui, an integrable-dominance condition, and derives tractable polynomial-invariant conditions for linear loops.

  • Martingales: A martingale represents an expression whose conditional expected value remains unchanged across computation steps.The paper identifies such martingales with probabilistic invariants.
  • Optional Stopping Theorem: Random stopping can break equality between initial and terminal expectations, so martingale invariants require suitable Optional Stopping Theorem conditions.The OST restores E(MT ) = E(M0) under appropriate boundedness or integrability assumptions.
  • dui: Unlike almost-sure deterministic bounds, dui permits a random-variable bound and imposes no constant a priori bound on runtime, variables, or updates.This generality accommodates martingales whose differences depend on unbounded-support distributions.
  • Optional Stopping Theorem: The dui precondition requires an integrable dominating function for the stopped martingale, thereby implying uniform integrability and the OST conclusion.For martingales, the theorem gives terminal integrability and equality of terminal and initial expectations.
  • Linear PTS: For linear single-loop programs, the paper derives tractable sufficient conditions under which polynomial martingale expressions satisfy the OST.These conditions form the basis of the implementation and support automatic synthesis and moment-bound derivation.

4 Polynomial Invariants of Linear Programs

This section gives sufficient conditions for polynomial martingales in single-loop linear PTS to satisfy the OST, including programs with unbounded-support sampling. It then uses these martingales to derive symbolic moment bounds.

  • Polynomial invariants: Theorem 3 provides a sufficient condition for polynomial martingale expressions in single-loop linear PTS to satisfy the OST.The condition depends on update-matrix structure, polynomial degree, and stopping-time moments.
  • Polynomial invariants: The analysis assumes update matrices have eigenvalues of absolute value at most 1, while sampled distributions have finite moments and independent fresh draws.These are the stated restrictions for the linear-program model.
  • Polynomial invariants: For each variable, dependence submatrices and Jordan-block sizes determine almost-sure bounds used to dominate stopped variable values.The construction reduces attention to variables and distributions on which the target variable depends.
  • Polynomial invariants: Uniform integrability of each monomial implies uniform integrability of a polynomial, allowing the dui precondition to establish the OST for polynomial martingales.Theorem 3 requires a suitable stopping-time moment; if the runtime depends on unbounded-support distributions, an additional moment is required.
  • Deriving bounds: The method synthesises martingales by solving coefficient equations, then uses symbolic propagation rules to derive bounds for terminated moments.Mixed-integer linear programming selects sparse solutions because the equation system is usually under-determined.
  • Deriving bounds: Automatic bound generation restricts square-root expressions and compares only highest-degree monomials to control computational cost.The implementation also selects a number of sparsest equation-system solutions rather than enumerating all rules.

5 Examples of Bound Derivation

The examples implement the approach on two linear PTS and derive symbolic bounds for moments after termination. The reported bounds are often asymptotically sharp, including cases with unbounded and state-dependent updates.

  • Examples: The implementation analyses Figures 1 and 2 because existing tools cannot compute tight symbolic termination-moment bounds for these examples.The authors implement automatic bound derivation in Polar.
  • Examples: E(T^2) < ∞ is required for Figure 1, while E(T^3) < ∞ is required for Figure 2 because its stopping time depends on unbounded-support variables.These runtime-moment conditions must currently be verified externally.
  • Figure 2: The Figure 2 bound for E(x_T) uses the final update and a truncated Normal(−1, 1) comparison, yielding a lower bound of −1.3.A corresponding truncated-variable argument gives E(x_T^2) ≤ 2.3.
  • Examples: Many Table 1 bounds are asymptotically sharp because their upper and lower bounds have equal leading terms.This includes E(z_T) in Figure 1 despite state-dependent increments unbounded below.
  • Examples: The runtime can itself be represented by a variable that increments by one each step, enabling bounds on runtime moments.This is the variable k in Figures 1 and 2.

6 Related Work

The related-work discussion positions the approach among methods for probabilistic invariants, runtime reasoning, and higher-order moment inference. It distinguishes the paper’s treatment of unbounded distributions and sign-unconstrained martingales.

  • OST preconditions: Prior OST-based analyses use preconditions such as bounded runtime, bounded step differences, or iteration-dependent bounds.The paper develops an alternative precondition for settings where constant bounds are unavailable.
  • Probabilistic invariants: Unlike approaches requiring non-negative martingales, Theorem 3 handles unbounded distributions and martingale invariants without a sign constraint for restricted PTS.The comparison concerns applicability to unbounded-support sampling.
  • Runtime bounds: Related work connects OST satisfaction with lower and upper bounds on probabilistic-program runtimes.The cited approaches use probabilistic invariants or supermartingales for runtime analysis.
  • Moment inference: Other studies infer higher-order moments and lower bounds for expected program quantities, including programs that are not almost surely terminating.The paper places its polynomial-invariant OST conditions within this broader line of work.

7 Conclusion

The paper presents dui as a general OST precondition and uses it to synthesise polynomial invariants and moment bounds for a class of linear loops. Its scope includes unbounded-support distributions, while nonlinear and nested loops remain future directions.

  • Conclusion: The paper introduces dui as a sufficient OST precondition for polynomial invariants of probabilistic transition systems.The precondition is based on an integrable dominating function.
  • Conclusion: For a restricted class of linear loops, the approach automatically derives polynomial invariants and bounds higher- and mixed-moments of variables and runtime after termination.These bounds are obtained using the synthesised invariants.
  • Conclusion: The approach handles distributions with unbounded support that other techniques cannot handle.The conclusion identifies this as a central scope of the contribution.
  • Conclusion: Future work includes adapting dui to nonlinear and nested loops, where unbounded updates may be necessary.The conclusion presents these as directions for improving automatic moment-bound derivation.

A A crash course in martingale theory

This section introduces filtrations, conditional expectations, and martingales through dyadic-interval examples. It explains why martingales serve as probabilistic invariants by preserving expected values as information grows.

  • Filtrations: A filtration is an increasing sequence of σ-algebras that records progressively finer information about a probability space.The dyadic construction satisfies F0 ⊆ Fn ⊆ Fn+1 ⊆ F.
  • Conditional expectation: Conditional expectation E[X | G] is the best approximation of X using only information represented by the sub-σ-algebra G.With the trivial σ-algebra, this approximation is the constant E[X].
  • Conditional expectation: For the uniform dyadic example, the conditional expectation Zn = E[Z | Fn] is constant on every dyadic interval at level n.The construction establishes these interval-wise constants and identifies the base case Z0(ω) = 1/2.
  • Martingales: A martingale is an adapted integrable sequence satisfying E[Mn+1 | Fn] = Mn almost surely.Consequently, E[Mn] = E[M0] for every n.
  • Martingales: Martingales are natural candidates for probabilistic invariants because they preserve information and expected value under the filtration.Supermartingales and submartingales respectively overapproximate and underapproximate later values.

B Known versions of the Optional Stopping Theorem

The section reviews sufficient conditions under which the Optional Stopping Theorem preserves martingale expectations at stopping times. These conditions use boundedness, uniform integrability, runtime tails, or growth controls.

  • Boundedness and supermartingales: The theorem applies when either the stopping time or the martingale is bounded.The reviewed conditions are P(T ≤ N) = 1 for some N or P(|Mn| ≤ K) = 1 for all n.
  • Boundedness and supermartingales: Non-negative supermartingales automatically satisfy the Optional Stopping Theorem with E[MT] ≤ E[M0].This provides an inequality rather than equality for stopped supermartingales.
  • Uniform integrability: Uniformly integrable martingales satisfy E[MT] = E[M0] for every stopping time T.Uniform integrability is defined through uniform control of tail expectations across all martingale indices.
  • Growth and runtime conditions: Polynomial growth of the martingale combined with a finite runtime moment can ensure uniform integrability of the stopped process.One version assumes E[p(T)] < ∞ and |Mn| ≤ p(n) on {T ≥ n}; another uses |Mn| ≤ C · (n + 1)^l.
  • Growth and runtime conditions: Exponential stopping-time tails paired with polynomially bounded increments are sufficient for integrability and optional-stopping conclusions.The reviewed result requires P(T > n) ≤ c1 · e^(-c2·n) and |Mn+1 − Mn| ≤ K · n^d almost surely.

C Proof of the dui-precondition

The dui precondition supplies an integrable dominating random variable for the stopped martingale process. This yields uniform integrability and therefore the expected-value conclusion of optional stopping.

  • dui precondition: The dui condition is a precondition for a stopped (super)martingale involving an integrable nonnegative dominating random variable.The paper names dui as “dominating function for uniform integrability.”
  • Conclusion: For a martingale, dui gives E(MT) = E(M0); for a supermartingale, it gives E(MT) ≤ E(M0).The proof obtains the result by L1 convergence of the stopped process to MT.
  • Proof: Under dui, the stopped process is uniformly integrable because it is dominated by an integrable random variable.The proof applies uniform-integrability closure results to the family {Mn∧T}n∈N.

D Operational Semantics and the proofs of Section 2

The operational semantics records program locations and states as random variables driven by initial values and successive random samples. Polynomial pre-expectations then connect one-step updates to martingale reasoning.

  • Operational semantics: A PTS operational semantics is a sequence of random variables {L[k], X[k]}k∈N representing locations and program states.The state variables take values in R^n and evolve through transitions and random samples.
  • Filtration: The natural filtration Fk = σ(X[0], R[1], · · ·, R[k]) contains the initial state and the first k random samples.It therefore stores the information available through the kth computation step.
  • Measurability: Operational semantics are measurable with respect to the product σ-algebra on locations and states and the filtration Fk.The proof establishes measurability inductively for the initial configuration and successive transitions.
  • Pre-expectations: For a polynomial h, the conditional expectation of its next-step value equals the pre-expectation evaluated at the current configuration.Independence of fresh samples from Fk permits treating the current state as fixed during the expectation.
  • Pre-expectations: If preE(h)(l, x, k + 1) ≤ h(l, x, k), then h(L[k], X[k], k) forms a supermartingale adapted to the standard filtration.The inequality follows directly from the conditional-expectation identity.

E Proofs of Section 4

The proofs establish norm and matrix-growth bounds used to show uniform integrability of polynomial martingales under finite stopping-time moments and the stated linear-system assumptions.

  • Matrix bounds: Matrix powers are bounded by analyzing Jordan blocks and comparing Euclidean and Frobenius norms.The proof uses an upper-triangular comparison matrix and block-diagonal structure to obtain the required norm bounds.
  • Theorem 3: Theorem 3 uses update matrices, largest Jordan-block sizes, and matrix norms to characterize growth relevant to polynomial martingales.The theorem fixes matrices A_i and B_i, block sizes m_i, and β_i = ∥B_i∥2 for a multi-index α.
  • Uniform integrability: Uniform integrability follows when the relevant stopping-time moment is finite and the random samples have the required finite moments.The proof applies Theorem 1 to stopped monomials and combines stopping-time and sample-moment conditions.
  • Uniform integrability: The proof handles variables with unbounded increments by bounding monomial growth through the update matrices and sample terms.The resulting bounds combine matrix norms, Jordan-block parameters, and moments of the random samples.
  • Soundness of derivation rules: The derivation rules are proved sound using expectation inequalities, Hölder’s inequality, Jensen’s inequality, Minkowski’s inequality, and sign information.Separate lemmas establish soundness for multiplication, conditional-sign bounds, Jensen-based bounds, and moment rules.

F.1 Limitations of Bound Derivation

The bound-derivation implementation faces scaling and synthesis challenges, especially when many bounds or non-polynomial terms are involved.

  • Bound derivation: Multiple bounds for one monomial cause very poor scaling because martingale rules are applied across all bound combinations.The problem becomes more severe when additional rules introduce terms outside the polynomial fragment.
  • Martingale synthesis: Martingale-expression synthesis is challenging because the defining equation system is usually under-determined and its solutions differ in usefulness.The implementation uses mixed-integer linear programming with CBC to iteratively search for sparse solutions.
  • Sign information: Multiplication rules require strict sign knowledge, which becomes more involved for generalized loop guards such as x > b.Such guards require considering expressions involving x − b and E(x − b).

G Termination Proofs of Examples

The examples establish finite moments for their stopping times using concentration bounds, supporting the runtime assumptions needed by the invariant analysis.

  • Uniform-decrement example: The first example models a loop with i.i.d. Uniform(−1, 0) decrements and defines termination as the first time X_n becomes negative.The process is represented as X_n = x0 + ΣU_i while the loop runs.
  • Uniform-decrement example: The uniform-decrement example uses the martingale M_n = X_n + n/2 and Azuma’s inequality to bound the termination tail.The argument uses the implication T ≥ n ⇒ X_n ≥ 0.
  • Termination moments: The resulting tail exponent is exp(O(−N√n)), so every fixed stopping-time moment is finite.This convergence conclusion is stated for the example’s stopping-time analysis.
  • Gaussian example: For the Gaussian and biased-step example, X_n − E(X_n) is shown to be sub-Gaussian with variance proxy 2n, yielding the same exp(O(−N√n)) tail behavior.The proof derives the concentration estimate from the moment-generating function, Gaussian additivity, Hoeffding’s lemma, and a Chernoff bound.
Loading 2609.02446v1…