Automated termination analysis of polynomial probabilistic programs
From MaRDI portal
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Abstract: The termination behavior of probabilistic programs depends on the outcomes of random assignments. Almost sure termination (AST) is concerned with the question whether a program terminates with probability one on all possible inputs. Positive almost sure termination (PAST) focuses on termination in a finite expected number of steps. This paper presents a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions. As proving (positive) AST is undecidable in general, existing proof rules typically provide sufficient conditions. These conditions mostly involve constraints on supermartingales. We consider four proof rules from the literature and extend these with generalizations of existing proof rules for (P)AST. We automate the resulting set of proof rules by effectively computing asymptotic bounds on polynomials over the program variables. These bounds are used to decide the sufficient conditions - including the constraints on supermartingales - of a proof rule. Our software tool Amber can thus check AST, PAST, as well as their negations for a large class of polynomial probabilistic programs, while carrying out the termination reasoning fully with polynomial witnesses. Experimental results show the merits of our generalized proof rules and demonstrate that Amber can handle probabilistic programs that are out of reach for other state-of-the-art tools.
Recommendations
- New approaches for almost-sure termination of probabilistic programs
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
- Termination analysis of probabilistic programs through Positivstellensatz's
- On Lexicographic Proof Rules for Probabilistic Termination
- On the hardness of almost-sure termination
Cites work
- A probabilistic PDL
- Abstraction, Refinement and Proof for Probabilistic Systems
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
- An axiomatic basis for computer programming
- Analysis of Bayesian networks via prob-solvable loops
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automated termination analysis of polynomial probabilistic programs
- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
- Computing expected runtimes for constant probability programs
- Fair termination for parameterized probabilistic concurrent systems
- scientific article; zbMATH DE number 1832220 (Why is no real title available?)
- Nagoya termination tool
- New approaches for almost-sure termination of probabilistic programs
- On probabilistic term rewriting
- On the hardness of almost-sure termination
- Probabilistic termination by monadic affine sized typing
- Probabilistic termination: soundness, completeness, and compositionality
- Ranking and repulsing supermartingales for reachability in probabilistic programs
- Semantics of probabilistic programs
- Stochastic invariants for probabilistic termination
- Term Rewriting and Applications
- Termination analysis of probabilistic programs through Positivstellensatz's
- The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
- Transition invariants and transition predicate abstraction for program termination
- Verification, Model Checking, and Abstract Interpretation
- Weakest precondition reasoning for expected runtimes of randomized algorithms
Cited in
(16)- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Moment-based analysis of Bayesian network properties
- Automated termination analysis of polynomial probabilistic programs
- scientific article; zbMATH DE number 1832220 (Why is no real title available?)
- The probabilistic termination tool amber
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
- Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
- On Lexicographic Proof Rules for Probabilistic Termination
- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
- Probabilistic program verification via inductive synthesis of inductive invariants
- On lexicographic proof rules for probabilistic termination
- From innermost to full almost-sure termination of probabilistic term rewriting
- Exact and approximate moment derivation for probabilistic loops with non-polynomial assignments
- 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
- Learning probabilistic termination proofs
This page was built for publication: Automated termination analysis of polynomial probabilistic programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233477)
