Sheshansh Agrawal
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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 whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach.
Supplemental Material
- 2010. IBM ILOG CPLEX Optimizer. http://www-01.ibm.com/software/integration/optimization/cplex-optimizer/.Google Scholar
- Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. 2017. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. CoRR abs/1709.04037 (2017). http://arxiv.org/abs/1709.04037Google Scholar
- Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. 2010. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In Proceedings of the 17th International Conference on Static Analysis (SAS’10). Springer-Verlag, Berlin, Heidelberg, 117–133. http://dl.acm.org/citation.cfm?id=1882094.1882102 Google ScholarCross Ref
- R.B. Ash and C. Doléans-Dade. 2000. Probability and Measure Theory. Harcourt/Academic Press.Google Scholar
- Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press, Cambridge, Massachusetts. 984 pages.Google ScholarDigital Library
- Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu. 2016a. Synthesizing Probabilistic Invariants via Doob’s Decomposition. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, 43–61. Google ScholarCross Ref
- Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016b. Proving Differential Privacy via Probabilistic Couplings. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16). ACM, New York, NY, USA, 749–758. Google ScholarDigital Library
- Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin Pierce. 2016c. Programming Language Techniques for Differential Privacy. ACM SIGLOG News 3, 1 (Feb. 2016), 34–53. Google ScholarDigital Library
- Amir M. Ben-Amram and Samir Genaim. 2013. On the Linear Ranking Problem for Integer Linear-constraint Loops. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13). ACM, New York, NY, USA, 51–62. Google ScholarDigital Library
- Amir M. Ben-Amram and Samir Genaim. 2015. Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. In Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, Daniel Kroening and Corina S. Păsăreanu (Eds.). Springer International Publishing, 304–321. Google ScholarCross Ref
- P. Billingsley. 1995. Probability and Measure (3rd ed.). Wiley.Google Scholar
- Olivier Bournez and Florent Garnier. 2005. Proving Positive Almost-Sure Termination. In RTA. 323–337. Google ScholarDigital Library
- Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005a. Linear Ranking with Reachability. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings (Lecture Notes in Computer Science), Kousha Etessami and Sriram K. Rajamani (Eds.), Vol. 3576. Springer, 491–504. Google ScholarDigital Library
- Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005b. The Polyranking Principle. In ICALP. 1349–1361. Google ScholarDigital Library
- Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman. 2016. T2: Temporal Property Verification. In Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Marsha Chechik and Jean-François Raskin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 387–393. Google ScholarDigital Library
- Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 511–526. Google ScholarDigital Library
- Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan. 2016. Deductive Proofs of Almost Sure Persistence and Recurrence Properties. In Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Marsha Chechik and Jean-François Raskin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 260–279. Google ScholarDigital Library
- Krishnendu Chatterjee and Hongfei Fu. 2017. Termination of Nondeterministic Recursive Probabilistic Programs. CoRR abs/1701.02944 (2017). http://arxiv.org/abs/1701.02944Google Scholar
- Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016a. Termination Analysis of Probabilistic Programs Through Positivstellensatz’s. In CAV. 3–22. Google ScholarCross Ref
- Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016b. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 327–342. Google ScholarDigital Library
- Krishnendu Chatterjee, Petr Novotný, and Djordje Ž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
- Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang. 2008. Ranking Abstractions. In Programming Languages and Systems: 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Sophia Drossopoulou (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 148–162. Google ScholarCross Ref
- Michael Colón and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings (Lecture Notes in Computer Science), Tiziana Margaria and Wang Yi (Eds.), Vol. 2031. Springer, 67–81. Google ScholarCross Ref
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination Proofs for Systems Code. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’06). ACM, New York, NY, USA, 415–426. Google ScholarDigital Library
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination. Commun. ACM 54, 5 (2011), 88–98. Google ScholarDigital Library
- Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. Lexicographic Termination Proving. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13). Springer-Verlag, Berlin, Heidelberg, 47–61. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238–252. Google ScholarDigital Library
- Devdatt Dubhashi and Alessandro Panconesi. 2009. Concentration of Measure for the Analysis of Randomized Algorithms (1st ed.). Cambridge University Press, New York, NY, USA. Google ScholarCross Ref
- Javier Esparza, Andreas Gaiser, and Stefan Kiefer. 2012. Proving Termination of Probabilistic Programs Using Patterns. In CAV. 123–138. Google ScholarDigital Library
- Paul Feautrier and Laure Gonnord. 2010. Accelerated Invariant Generation for C Programs with Aspic and C2fsm. Electronic Notes in Theoretical Computer Science 267, 2 (2010), 3 – 13. Google ScholarDigital Library
- Yishai A. Feldman. 1984. A decidable propositional dynamic logic with explicit probabilities. Information and Control 63, 1 (1984), 11–38. Google ScholarDigital Library
- Yishai A Feldman and David Harel. 1982. A probabilistic dynamic logic. In Proceedings of the fourteenth annual ACM Symposium on Theory of computing. ACM, 181–195.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, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 489–501. Google ScholarDigital Library
- Robert W. Floyd. 1967. Assigning meanings to programs. Mathematical Aspects of Computer Science 19 (1967), 19–33. Google ScholarCross Ref
- F. G. Foster. 1953. On the Stochastic Matrices Associated with Certain Queuing Processes. The Annals of Mathematical Statistics 24, 3 (1953), pp. 355–360. Google ScholarCross Ref
- Zoubin Ghahramani. 2015. Probabilistic machine learning and artificial intelligence. Nature 521, 7553 (2015), 452–459. Google ScholarCross Ref
- Laure Gonnord, David Monniaux, and Gabriel Radanne. 2015. Synthesis of Ranking Functions Using Extremal Counterexamples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). ACM, New York, NY, USA, 608–618. Google ScholarDigital Library
- Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. 2014. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Performance Evaluation 73 (2014), 110 – 132. Google ScholarDigital Library
- Sergiu Hart and Micha Sharir. 1985. Concurrent Probabilistic Programs, Or: How to Schedule if You Must. SIAM J. Comput. 14, 4 (1985), 991–1012. Google ScholarCross Ref
- L. P. Kaelbling, M. L. Littman, and A. W. Moore. 1996. Reinforcement learning: A survey. Journal of Artificial Intelligence Research 4 (1996), 237–285.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 Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 364–389. Google ScholarDigital Library
- Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods. In SAS, Vol. LNCS 6337, Springer. 390–406. Google ScholarCross Ref
- Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. System Sci. 22, 3 (1981), 328–350. Google ScholarCross Ref
- Dexter Kozen. 1983. A Probabilistic PDL. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing (STOC ’83). ACM, New York, NY, USA, 291–297. Google ScholarDigital Library
- Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, and Christoph M. Wintersteiger. 2010. Termination Analysis with Compositional Transition Invariants. In Computer Aided Verification: 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 89–103. Google ScholarDigital Library
- Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV (LNCS 6806). 585–591.Google Scholar
- Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In POPL. 81–92. Google ScholarDigital Library
- Annabelle McIver and Carroll Morgan. 2004. Developing and Reasoning About Probabilistic Programs in pGCL. In PSSE. 123–155.Google Scholar
- 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). http://arxiv.org/abs/1612.01091Google Scholar
- David Monniaux. 2001. An Abstract Analysis of the Probabilistic Termination of Programs. In Static Analysis, 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings (Lecture Notes in Computer Science), Patrick Cousot (Ed.), Vol. 2126. Springer, 111–126. Google ScholarCross Ref
- Rajeev Motwani and Prabhakar Raghavan. 1995. Randomized Algorithms. Cambridge University Press, New York, NY, USA. Google ScholarCross Ref
- M. Neuhäußer, M. Stoelinga, and J.-P. Katoen. 2009. Delayed Nondeterminism in Continuous-Time Markov Decision Processes. In Proceedings of FoSSaCS 2009, Vol. 5504. 364–379. Google ScholarDigital Library
- Martin R Neuhäußer and Joost-Pieter Katoen. 2007. Bisimulation and logical preservation for continuous-time Markov decision processes. In International Conference on Concurrency Theory (CONCUR 2007). Springer, 412–427.Google Scholar
- 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
- Andreas Podelski and Andrey Rybalchenko. 2004a. A Complete Method for the Synthesis of Linear Ranking Functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings (Lecture Notes in Computer Science), Bernhard Steffen and Giorgio Levi (Eds.), Vol. 2937. Springer, 239–251. Google ScholarCross Ref
- Andreas Podelski and Andrey Rybalchenko. 2004b. Transition Invariants. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS ’04). IEEE Computer Society, Washington, DC, USA, 32–41. Google ScholarCross Ref
- Jeffrey S Rosenthal. 2006. A First Look at Rigorous Probability Theory (2nd ed.). World Scientific Publishing Company.Google ScholarCross Ref
- Micha Sharir, Amir Pnueli, and Sergiu Hart. 1984. Verification of Probabilistic Programs. SIAM J. Comput. 13, 2 (1984), 292–314. Google ScholarDigital Library
- Kirack Sohn and Allen Van Gelder. 1991. Termination Detection in Logic Programs using Argument Sizes. In Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 29-31, 1991, Denver, Colorado, USA, Daniel J. Rosenkrantz (Ed.). ACM Press, 216–226. Google ScholarDigital Library
Index Terms
- Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs
Recommendations
Stochastic invariants for probabilistic termination
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesTermination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with ...
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 ...
Stochastic invariants for probabilistic termination
POPL '17Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with ...
Comments