New approaches for almost-sure termination of probabilistic programs

DOI10.1007/978-3-030-02768-1_11zbMATH Open1519.68052arXiv1806.06683OpenAlexW2808151598MaRDI QIDQ6166145FDOQ6166145

Authors: Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee 

Publication date: 2 August 2023

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

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.

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

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

Mathematics Subject Classification ID

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

Cited In (15)

• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Title not available (Why is that?)
• 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
• Probabilistic termination: soundness, completeness, and compositionality
• On lexicographic proof rules for probabilistic termination
• Proving Positive Almost Sure Termination Under Strategies
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• Automated tail bound analysis for probabilistic recurrence relations
• Title not available (Why is that?)
• Ranking and repulsing supermartingales for reachability in probabilistic programs
• Stochastic invariants for probabilistic termination

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)