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.
Cite
@article{arxiv.1806.06683,
title = {New Approaches for Almost-Sure Termination of Probabilistic Programs},
author = {Mingzhang Huang and Hongfei Fu and Krishnendu Chatterjee},
journal= {arXiv preprint arXiv:1806.06683},
year = {2018}
}