Proving termination of probabilistic programs using patterns

Javier Esparza; Andreas Gaiser; Stefan Kiefer

doi:10.1007/978-3-642-31424-7_14

Proving termination of probabilistic programs using patterns

Javier Esparza, Andreas Gaiser, Stefan Kiefer

Informatics 7 - Chair of Theoretical Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

45 Scopus citations

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.

Original language	English
Title of host publication	Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings
Pages	123-138
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-31424-7_14
State	Published - 2012
Event	24th International Conference on Computer Aided Verification, CAV 2012 - Berkeley, CA, United States Duration: 7 Jul 2012 → 13 Jul 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7358 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th International Conference on Computer Aided Verification, CAV 2012
Country/Territory	United States
City	Berkeley, CA
Period	7/07/12 → 13/07/12

Access to Document

10.1007/978-3-642-31424-7_14

Cite this

Esparza, J., Gaiser, A., & Kiefer, S. (2012). Proving termination of probabilistic programs using patterns. In Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings (pp. 123-138). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7358 LNCS). https://doi.org/10.1007/978-3-642-31424-7_14

@inproceedings{5fc90c154e41413289ac2cb9d0de41c7,

title = "Proving termination of probabilistic programs using patterns",

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.",

author = "Javier Esparza and Andreas Gaiser and Stefan Kiefer",

year = "2012",

doi = "10.1007/978-3-642-31424-7_14",

language = "English",

isbn = "9783642314230",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "123--138",

booktitle = "Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings",

note = "24th International Conference on Computer Aided Verification, CAV 2012 ; Conference date: 07-07-2012 Through 13-07-2012",

}

Esparza, J, Gaiser, A & Kiefer, S 2012, Proving termination of probabilistic programs using patterns. in Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7358 LNCS, pp. 123-138, 24th International Conference on Computer Aided Verification, CAV 2012, Berkeley, CA, United States, 7/07/12. https://doi.org/10.1007/978-3-642-31424-7_14

Proving termination of probabilistic programs using patterns. / Esparza, Javier; Gaiser, Andreas; Kiefer, Stefan.
Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings. 2012. p. 123-138 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7358 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Proving termination of probabilistic programs using patterns

AU - Esparza, Javier

AU - Gaiser, Andreas

AU - Kiefer, Stefan

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84864049038&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-31424-7_14

DO - 10.1007/978-3-642-31424-7_14

M3 - Conference contribution

AN - SCOPUS:84864049038

SN - 9783642314230

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 123

EP - 138

BT - Computer Aided Verification - 24th International Conference, CAV 2012, Proceedings

T2 - 24th International Conference on Computer Aided Verification, CAV 2012

Y2 - 7 July 2012 through 13 July 2012

ER -

Proving termination of probabilistic programs using patterns

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this