New Approaches for Almost-Sure Termination of Probabilistic Programs

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.

References in corpus (5)

• Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
• A New Proof Rule for Almost-Sure Termination
• Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
• Reasoning about Recursive Probabilistic Programs
• A new rule for almost-certain termination of probabilistic- and demonic programs