Stochastic invariants for probabilistic termination
From MaRDI portal
Abstract: 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.
Recommendations
- scientific article; zbMATH DE number 1927425
- Termination of nondeterministic probabilistic programs
- Probabilistic semantics of terminating programs
- scientific article; zbMATH DE number 4076588
- Termination analysis of probabilistic programs through Positivstellensatz's
- Probabilistic termination: soundness, completeness, and compositionality
- scientific article; zbMATH DE number 1832220
- New approaches for almost-sure termination of probabilistic programs
Cited in
(30)- On termination and invariance for faulty channel machines
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- A denotational semantics for low-level probabilistic programs with nondeterminism
- Automated termination analysis of polynomial probabilistic programs
- Termination of nondeterministic probabilistic programs
- Computing expected runtimes for constant probability programs
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
- Termination analysis of probabilistic programs through Positivstellensatz's
- Synthesizing Probabilistic Invariants via Doob’s Decomposition
- scientific article; zbMATH DE number 7376040 (Why is no real title available?)
- On the termination problem for probabilistic higher-order recursive programs
- Of cores: a partial-exploration framework for Markov decision processes
- Tail probabilities for randomized program runtimes via martingales for higher moments
- Moment-based invariants for probabilistic loops with non-polynomial assignments
- Ranking and repulsing supermartingales for reachability in probabilistic programs
- The probabilistic termination tool amber
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
- On Lexicographic Proof Rules for Probabilistic Termination
- A learner-verifier framework for neural network controllers and certificates of stochastic systems
- Automated tail bound analysis for probabilistic recurrence relations
- MDPs as distribution transformers: affine invariant synthesis for safety objectives
- Probabilistic program verification via inductive synthesis of inductive invariants
- On lexicographic proof rules for probabilistic termination
- From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
- Finite-time safety and reach-avoid verification of stochastic discrete-time systems
- Quantitative verification with neural networks
- Quantitative verification with neural networks
- Omega-regular verification and control for distributional specifications in MDPs
- Sum-of-squares certificates for almost-sure reachability of stochastic polynomial systems
- Learning probabilistic termination proofs
This page was built for publication: Stochastic invariants for probabilistic termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370852)
