Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Proving Termination of Probabilistic Programs Using Patterns

Reference:

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In Proceedings of CAV 2012, Berkeley, USA, 2012.

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{EGK12Cav,
    address = {Berkeley, USA},
    author = {Javier Esparza and Andreas Gaiser and Stefan Kiefer},
    booktitle = {Proceedings of CAV 2012},
    title = {Proving Termination of Probabilistic Programs Using Patterns},
    year = {2012}
}

See archive.model.in.tum.de ...
Tech report version