Reference:

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. Technical report, arXiv.org, April 2012. Available at http://arxiv.org/abs/1204.2932.

Abstract:

Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analog for probabilistic programs, namely termination with probability one (``almost-sure termination''), is an equally important property for randomized algorithms and probabilistic protocols. We suggest a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs: it calls such tools within a refinement loop and thereby iteratively constructs a ``terminating pattern'', which is a set of terminating runs with probability one. We report on various case studies illustrating the effectiveness of our algorithm. As a further application, our algorithm can improve lower bounds on reachability probabilities.

Suggested BibTeX entry:

@techreport{12EGK:CAV-TR,
    author = {Javier Esparza and Andreas Gaiser and Stefan Kiefer},
    institution = {arXiv.org},
    month = {April},
    note = {Available at http://arxiv.org/abs/1204.2932},
    title = {Proving Termination of Probabilistic Programs Using Patterns},
    year = {2012}
}