Luis María Ferrer Fioriti
ABSTRACT
We propose a framework to prove almost sure termination for probabilistic programs with real valued variables. It is based on ranking supermartingales, a notion analogous to ranking functions on non-probabilistic programs. The framework is proven sound and complete for a meaningful class of programs involving randomization and bounded nondeterminism. We complement this foundational insigh by a practical proof methodology, based on sound conditions that enable compositional reasoning and are amenable to a direct implementation using modern theorem provers. This is integrated in a small dependent type system, to overcome the problem that lexicographic ranking functions fail when combined with randomization. Among others, this compositional methodology enables the verification of probabilistic programs outside the complete class that admits ranking supermartingales.
Supplemental Material
- R. B. Ash and C. Doléans-Dade. Probability and Measure Theory. Harcourt, 2000.Google Scholar
- J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W. O'Hearn. Variance analyses from invariance analyses. In POPL, pages 211--224. ACM, 2007. Google ScholarDigital Library
- O. Bournez and F. Garnier. Proving positive almost-sure termination. In RTA, LNCS 3467:323--337. Springer, 2005. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In ICALP, LNCS 3580:1349--1361. Springer, 2005. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In CAV, LNCS 3576:491--504. Springer, 2005. Google ScholarDigital Library
- T. Brézdil, J. Esparza, S. Kiefer, and A. Kucera. Analyzing probabilistic pushdown automata. Formal Methods in System Design, 43 (2):124--163, 2013. Google ScholarDigital Library
- A. Chakarov and S. Sankaranarayanan. Probabilistic program analysis with martingales. In CAV, LNCS 8044:511--526. Springer, 2013. Google ScholarDigital Library
- M. Codish and S. Genaim. Proving termination one loop at a time. In WLPE, CW371 Report, pages 48--59. K. U. Leuven, 2003.Google Scholar
- M. Colón and H. Sipma. Synthesis of linear ranking functions. In TACAS, LNCS 2031:67--81. Springer, 2001. Google ScholarDigital Library
- B. Cook, A. See, and F. Zuleger. Ramsey vs. lexicographic termination proving. In TACAS, LNCS 7795:47--61. Springer, 2013. Google ScholarDigital Library
- N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A general framework for automatic termination analysis of logic programs. Appl. Algebra Eng. Commun. Comput., 12(1/2):117--156, 2001.Google ScholarCross Ref
- J. Esparza, A. Gaiser, and S. Kiefer. Proving termination of probabilistic programs using patterns. In CAV, LNCS 7358:123--138. Springer, 2012. Google ScholarDigital Library
- J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer-Verlag New York, Inc., New York, NY, USA, 1996. Google ScholarCross Ref
- R. W. Floyd. Assigning meanings to programs. Mathematical aspects of computer science, 19:19--32, 1967.Google Scholar
- F. G. Foster. On the stochastic matrices associated with certain queuing processes. The Annals of Mathematical Statistics, 24(3):355--360, 09 1953.Google ScholarCross Ref
- J. Giesl, R. Thiemann, and P. Schneider-Kamp. The dependency pair framework: Combining techniques for automated termination proofs. In LPAR, LNCS 3452:301--331. Springer, 2004.Google Scholar
- I. Gnaedig. Induction for positive almost sure termination. In PPDP, pages 167--178. ACM, 2007. Google ScholarDigital Library
- A. D. Gordon, T. A. Henzinger, A. V. Nori, and S. K. Rajamani. Probabilistic programming. In FOSE, pages 167--181. ACM, 2014. Google ScholarDigital Library
- F. Gretz, J.-P. Katoen, and A. McIver. Prinsys - on a quest for probabilistic loop invariants. In QEST, LNCS 8054:193--208. Springer, 2013. Google ScholarDigital Library
- F. Gretz, J.-P. Katoen, and A. McIver. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval., 73:110--132, 2014. Google ScholarDigital Library
- S. Hart and M. Sharir. Concurrent probabilistic programs, or: How to schedule if you must. SIAM J. Comput., 14(4):991--1012, 1985.Google ScholarDigital Library
- S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst., 5(3):356--380, 1983. Google ScholarDigital Library
- C.-K. Hur, A. V. Nori, S. K. Rajamani, and S. Samuel. Slicing probabilistic programs. In PLDI, pages 133--144. ACM, 2014. Google ScholarDigital Library
- C. Jones. Probabilistic non-determinism. PhD thesis, University of Edinburgh, 1989. Google ScholarDigital Library
- J.-P. Katoen, A. McIver, L. Meinicke, and C. C. Morgan. Linearinvariant generation for probabilistic programs: - automated support for proof-based methods. In SAS, LNCS 6337:390--406. Springer, 2010. Google ScholarDigital Library
- S. Katz and Z. Manna. A closer look at termination. Acta Inf., 5: 333--352, 1975. Google ScholarDigital Library
- D. Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328--350, 1981.Google ScholarCross Ref
- D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination analysis with compositional transition invariants. In CAV, LNCS 6174:89--103. Springer, 2010. Google ScholarDigital Library
- C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In POPL, pages 81--92. ACM, 2001. Google ScholarDigital Library
- A. McIver and C. Morgan. Abstraction, Refinement And Proof For Probabilistic Systems. Springer, 2004. Google ScholarDigital Library
- D. Monniaux. An abstract analysis of the probabilistic termination of programs. In SAS, LNCS 2126:111--126. Springer, 2001. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. Transition invariants. In LICS, pages 32--41. IEEE Computer Society, 2004. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, LNCS 2937:239--251. Springer, 2004.Google ScholarCross Ref
- K. Sohn and A. V. Gelder. Termination detection in logic programs using argument sizes. In PODS, pages 216--226. ACM Press, 1991. Google ScholarDigital Library
- D. Williams. Probability with Martingales. Cambridge University Press, 1991.Google ScholarCross Ref
Recommendations
Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs
Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks ...
A new proof rule for almost-sure termination
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 ...
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 ...
Comments