research-article

Open access

A new proof rule for almost-sure termination

Authors:

Annabelle McIver,

Carroll Morgan,

Benjamin Lucien Kaminski,

Joost-Pieter KatoenAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 33, Pages 1 - 28

https://doi.org/10.1145/3158121

Published: 27 December 2017 Publication History

Abstract

We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism.

An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice.

Like others, we use variant functions (a.k.a. "super-martingales") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.

Supplementary Material

WEBM File (almostsuretermination.webm)

Download
122.02 MB

References

[1]

Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. 2018. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. In Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). ACM, New York, NY, USA.

Digital Library

[2]

David Blackwell. 1955. On Transient Markov Processes with a Countable Number of States and Stationary Transition Probabilities. Ann. Math. Statist. 26 (1955), 654–658.

[3]

Orieta Celiku and Annabelle McIver. 2005. Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs. In FM (Lecture Notes in Computer Science), Vol. 3582. Springer, 107–122.

Digital Library

[4]

Aleksandar Chakarov. 2016. Deductive Verification of Infinite-State Stochastic Systems using Martingales. Ph.D. Dissertation. University of Colorado at Boulder.

[5]

Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV (Lecture Notes in Computer Science), Vol. 8044. Springer, 511–526.

Digital Library

[6]

Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs/1701.02944 (2017).

[7]

Krishnendu Chatterjee, Petr Novotný, and Dorde Žikelić. 2017. Stochastic Invariants for Probabilistic Termination. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA, 145–160.

Digital Library

[8]

Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall.

Digital Library

[9]

Javier Esparza, Andreas Gaiser, and Stefan Kiefer. 2012. Proving Termination of Probabilistic Programs Using Patterns. In CAV (Lecture Notes in Computer Science), Vol. 7358. Springer, 123–138.

Digital Library

[10]

Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic Termination: Soundness, Completeness, and Compositionality. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015). ACM, New York, NY, USA, 489–501.

Digital Library

[11]

F. G. Foster. 1951. Markoff chains with an enumerable number of states and a class of cascade processes. Cambridge Philosophical Society 1, 47 (1951), 77–85.

[12]

F. G. Foster. 1952. On Markov Chains with an Enumerable Infinity of States. Mathematical Proceedings of the Cambridge Philosophical Society 4 (Oct 1952), 587–591.

[13]

Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. 2014. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73 (2014), 110–132.

Digital Library

[14]

G.R. Grimmett and D. Welsh. 1986. Probability: an Introduction. Oxford Science Publications.

[15]

Sergiu Hart, Micha Sharir, and Amir Pnueli. 1983. Termination of Probabilistic Concurrent Programs. ACM Trans. Program. Lang. Syst. 5, 3 (July 1983), 356–380.

Digital Library

[16]

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580.

Digital Library

[17]

Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In ESOP (Lecture Notes in Computer Science), Vol. 9632. Springer, 364–389.

Digital Library

[18]

David G. Kendall. 1951. On non-dissipative Markoff chains with an enumerable infinity of states. Mathematical Proceedings of the Cambridge Philosophical Society 47, 3 (001 007 1951), 633–634.

[19]

Konrad Knopp. 1928. Theory and Application of Infinite Series. London.

[20]

Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci. 30, 2 (1985), 162–178.

[21]

Ugo Dal Lago and Charles Grellois. 2017. Probabilistic Termination by Monadic Affine Sized Typing. In ESOP (Lecture Notes in Computer Science), Vol. 10201. Springer, 393–419.

[22]

Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer.

Digital Library

[23]

Annabelle McIver and Carroll Morgan. 2016. A New Rule for Almost-Certain Termination of Probabilistic and Demonic Programs. CoRR abs/1612.01091 (2016).

[24]

C.C. Morgan. 1996. Proof Rules for Probabilistic Loops. In Proc BCS-FACS 7th Refinement Workshop (Workshops in Computing), He Jifeng, John Cooke, and Peter Wallis (Eds.). Springer. http://www.bcs.org/upload/pdf/ewic rw96 paper10.pdf.

[25]

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst. 18, 3 (May 1996), 325–353.

Digital Library

[26]

Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning About Recursive Probabilistic Programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16). ACM, New York, NY, USA, 672–681.

Digital Library

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Dal Lago UPadovani L(2024)On the Almost-Sure Termination of Binary SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678239(1-12)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678239
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Show More Cited By

Index Terms

A new proof rule for almost-sure termination
1. Theory of computation
  1. Models of computation
    1. Probabilistic computation
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification
    2. Program semantics
      1. Axiomatic semantics

Recommendations

Modular verification for almost-sure termination of probabilistic programs

In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical ...
Positive Almost-Sure Termination: Complexity and Proof Rules

We study the recursion-theoretic complexity of Positive Almost-Sure Termination (PAST) in an imperative programming language with rational variables, bounded nondeterministic choice, and discrete probabilistic choice. A program terminates positive almost-...
Almost-Sure Termination by Guarded Refinement

Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logics have mostly been developed for first-order programs written in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Australian Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

69
Total Citations
View Citations
1,125
Total Downloads

Downloads (Last 12 months)210
Downloads (Last 6 weeks)41

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Dal Lago UPadovani L(2024)On the Almost-Sure Termination of Binary SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678239(1-12)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678239
Aguirre AHaselwarter Pde Medeiros MLi KGregersen STassarotti JBirkedal L(2024)Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36746358:ICFP(284-316)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674635
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Almost-Sure Termination by Guarded RefinementProceedings of the ACM on Programming Languages10.1145/36746328:ICFP(203-233)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674632
Chatterjee KGoharshady ENovotný PŽikelić Đ(2024)Equivalence and Similarity Refutation for Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36564628:PLDI(2098-2122)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656462
Chatterjee KGoharshady AMeggendorfer TŽikelić Đ(2024)Quantitative Bounds on Resource Usage of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498248:OOPSLA1(362-391)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649824
Majumdar RSathiyanarayana V(2024)Positive Almost-Sure Termination: Complexity and Proof RulesProceedings of the ACM on Programming Languages10.1145/36328798:POPL(1089-1117)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632879
Ye KWoodcock JFoster S(2024)Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: Semantics and automated reasoning with theorem provingTheoretical Computer Science10.1016/j.tcs.2024.1148761021(114876)Online publication date: Dec-2024
https://doi.org/10.1016/j.tcs.2024.114876
Kassing JDollase SGiesl J(2024)A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term RewritingFunctional and Logic Programming10.1007/978-981-97-2300-3_4(62-80)Online publication date: 15-May-2024
https://dl.acm.org/doi/10.1007/978-981-97-2300-3_4
Majumdar RSathiyanarayana V(2024)Sound and Complete Techniques for Reasoning About TerminationPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75783-9_2(41-72)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75783-9_2
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents