Annabelle McIver
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.
Supplemental Material
- 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.Google Scholar
Digital Library
- David Blackwell. 1955. On Transient Markov Processes with a Countable Number of States and Stationary Transition Probabilities. Ann. Math. Statist. 26 (1955), 654–658. Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Aleksandar Chakarov. 2016. Deductive Verification of Infinite-State Stochastic Systems using Martingales. Ph.D. Dissertation. University of Colorado at Boulder.Google Scholar
- Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV (Lecture Notes in Computer Science), Vol. 8044. Springer, 511–526. Google ScholarDigital Library
- Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs/1701.02944 (2017).Google Scholar
- 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. Google ScholarDigital Library
- Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall.Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarCross Ref
- 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. Google ScholarCross Ref
- 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. Google ScholarDigital Library
- G.R. Grimmett and D. Welsh. 1986. Probability: an Introduction. Oxford Science Publications.Google Scholar
- Sergiu Hart, Micha Sharir, and Amir Pnueli. 1983. Termination of Probabilistic Concurrent Programs. ACM Trans. Program. Lang. Syst. 5, 3 (July 1983), 356–380. Google ScholarDigital Library
- C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarCross Ref
- Konrad Knopp. 1928. Theory and Application of Infinite Series. London.Google Scholar
- Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci. 30, 2 (1985), 162–178. Google ScholarCross Ref
- 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. Google ScholarCross Ref
- Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer.Google ScholarDigital Library
- Annabelle McIver and Carroll Morgan. 2016. A New Rule for Almost-Certain Termination of Probabilistic and Demonic Programs. CoRR abs/1612.01091 (2016).Google Scholar
- 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.Google ScholarCross Ref
- Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Trans. Program. Lang. Syst. 18, 3 (May 1996), 325–353. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- A new proof rule for almost-sure termination
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-...
Proving almost-sure termination by omega-regular decomposition
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationAlmost-sure termination is the most basic liveness property of probabilistic programs. We present a novel decomposition-based approach for proving almost-sure termination of probabilistic programs with complex control-flow structure and non-determinism. ...
Comments