New approaches for almost-sure termination of probabilistic programs

DOI10.1007/978-3-030-02768-1_11MaRDI QIDQ6166145zbMATH OpenOpenAlexFDO

Authors Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for the almost-sure termination problem. Moreover, using this approach we can obtain explicit optimal bounds on tail probabilities of non-termination within a given number of steps. Second, we present a new approach based on Central Limit Theorem for the almost-sure termination problem, and show that this approach can establish almost-sure termination of programs which none of the existing approaches can handle. Finally, we discuss algorithmic approaches for the two above methods that lead to automated analysis techniques for almost-sure termination of probabilistic programs.

Recommendations

• scientific article; zbMATH DE number 1927425
• Termination analysis of probabilistic programs through Positivstellensatz's
• Probabilistic semantics of terminating programs
• scientific article; zbMATH DE number 4076588
• Termination of nondeterministic probabilistic programs
• scientific article; zbMATH DE number 1832220
• On the termination problem for probabilistic higher-order recursive programs
• Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
• Termination Analysis of Probabilistic Programs with Martingales

Cited in

(19)

• Ranking and repulsing supermartingales for reachability in probabilistic programs
• Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
• Stochastic invariants for probabilistic termination
• Probabilistic termination by monadic affine sized typing
• On lexicographic proof rules for probabilistic termination
• The probabilistic termination tool amber
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Proving Positive Almost Sure Termination Under Strategies
• Automated tail bound analysis for probabilistic recurrence relations
• Probabilistic termination: soundness, completeness, and compositionality
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• scientific article; zbMATH DE number 1832220 (Why is no real title available?)
• On Lexicographic Proof Rules for Probabilistic Termination
• On the hardness of almost-sure termination
• Automated termination analysis of polynomial probabilistic programs
• scientific article; zbMATH DE number 4076588 (Why is no real title available?)

This page was built for publication: New approaches for almost-sure termination of probabilistic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166145)