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

(20)

• Stochastic invariants for probabilistic termination
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 1832220 (Why is no real title available?)
• The probabilistic termination tool amber
• On the hardness of almost-sure termination
• Probabilistic termination by monadic affine sized typing
• Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
• 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
• Probabilistic termination: soundness, completeness, and compositionality
• Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
• Proving Positive Almost Sure Termination Under Strategies
• On lexicographic proof rules for probabilistic termination
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• scientific article; zbMATH DE number 4076588 (Why is no real title available?)
• Automated tail bound analysis for probabilistic recurrence relations
• Ranking and repulsing supermartingales for reachability in probabilistic programs

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)