Automated termination analysis of polynomial probabilistic programs

DOI10.1007/978-3-030-72019-3_18MaRDI QIDQ2233477zbMATH OpenOpenAlexWikidataFDO

Authors Marcel Moosbrugger, Ezio Bartocci, Laura Kovács, Joost-Pieter Katoen

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2010.03444

zbMATH Keywords

martingaleslinear recurrencesasymptotic boundsprobabilistic programmingalmost sure termination

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

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

• scientific article; zbMATH DE number 1832220 (Why is no real title available?)
• 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
• 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

(14)

• On lexicographic proof rules for probabilistic termination
• Learning probabilistic termination proofs
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
• The probabilistic termination tool amber
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Probabilistic program verification via inductive synthesis of inductive invariants
• Moment-based analysis of Bayesian network properties
• Exact and approximate moment derivation for probabilistic loops with non-polynomial assignments
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• From innermost to full almost-sure termination of probabilistic term rewriting
• scientific article; zbMATH DE number 1832220 (Why is no real title available?)
• On Lexicographic Proof Rules for Probabilistic Termination
• Automated termination analysis of polynomial probabilistic programs

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)