Reference:

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Madhusudan Parathasarathy and Sanjit A. Seshia, editors, Proceedings of the 24th International Conference on Computer Aided Verification (CAV), volume 7358 of LNCS, pages 123–138, Berkeley, California, USA, 2012. Springer.

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:

@inproceedings{12EGK:CAV,
    address = {Berkeley, California, USA},
    author = {Javier Esparza and Andreas Gaiser and Stefan Kiefer},
    booktitle = {Proceedings of the 24th International Conference on Computer Aided Verification (CAV)},
    editor = {Madhusudan Parathasarathy and Sanjit A. Seshia},
    pages = {123--138},
    publisher = {Springer},
    series = {LNCS},
    title = {Proving Termination of Probabilistic Programs Using Patterns},
    volume = {7358},
    year = {2012}
}