Automated termination analysis of polynomial probabilistic programs

DOI10.1007/978-3-030-72019-3_18zbMATH Open1473.68053arXiv2010.03444OpenAlexW3144365821WikidataQ124212480 ScholiaQ124212480MaRDI QIDQ2233477FDOQ2233477

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

Publication date: 18 October 2021

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.

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

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

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)

Cites Work

• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Nagoya Termination Tool
• An axiomatic basis for computer programming
• A probabilistic PDL
• Abstraction, Refinement and Proof for Probabilistic Systems
• Semantics of probabilistic programs
• Transition invariants and transition predicate abstraction for program termination
• Verification, Model Checking, and Abstract Interpretation
• The concrete tetrahedron. Symbolic sums, recurrence equations, generating functions, asymptotic estimates
• Probabilistic termination: soundness, completeness, and compositionality
• Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
• Fair Termination for Parameterized Probabilistic Concurrent Systems
• Automated termination analysis of polynomial probabilistic programs
• Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
• Termination Analysis of Probabilistic Programs Through Positivstellensatz’s
• Stochastic invariants for probabilistic termination
• Term Rewriting and Applications
• Title not available (Why is that?)
• On probabilistic term rewriting
• On the Hardness of Almost–Sure Termination
• Probabilistic Termination by Monadic Affine Sized Typing
• Analysis of Bayesian networks via prob-solvable loops
• Computing expected runtimes for constant probability programs
• New approaches for almost-sure termination of probabilistic programs
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Ranking and repulsing supermartingales for reachability in probabilistic programs

Cited In (14)

• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Learning probabilistic termination proofs
• Title not available (Why is that?)
• The probabilistic termination tool amber
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• On Lexicographic Proof Rules for Probabilistic Termination
• Automated termination analysis of polynomial probabilistic programs
• 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
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
• Moment-based analysis of Bayesian network properties
• Probabilistic program verification via inductive synthesis of inductive invariants

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)