2015 ProbabilisticTerminationSoundne

(Ferrer Fioriti & Hermanns, 2015) ⇒ 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. ISBN:978-1-4503-3300-9 doi:10.1145/2676726.2677001

Subject Headings:

Notes

Cited By

Quotes

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.

Body

Theorem 5.6 (Soundness). Let [math]\displaystyle{ P }[/math] be a probabilistic program with semantics [math]\displaystyle{ {(L, X) φ n} }[/math], and a ranking supermartingale [math]\displaystyle{ {Y_n} }[/math] such that [math]\displaystyle{ Y_n = 0 }[/math] implies [math]\displaystyle{ T φ ≤ n }[/math] for all valid schedulers φ. Then, P almost sure terminates, and T ∗ is integrable.

References

1. R. B. Ash and C. Doléans-Dade. Probability and Measure Theory. Harcourt, 2000.
2. Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter O'Hearn, Variance Analyses from Invariance Analyses, Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 17-19, 2007, Nice, France doi:10.1145/1190216.1190249
3. Olivier Bournez, Florent Garnier, Proving Positive Almost-sure Termination, Proceedings of the 16th International Conference on Term Rewriting and Applications, p.323-337, April 19-21, 2005, Nara, Japan doi:10.1007/978-3-540-32033-3_24
4. Aaron R. Bradley, Zohar Manna, Henny B. Sipma, The Polyranking Principle, Proceedings of the 32nd International Conference on Automata, Languages and Programming, July 11-15, 2005, Lisbon, Portugal doi:10.1007/11523468_109
5. Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Linear Ranking with Reachability, Proceedings of the 17th International Conference on Computer Aided Verification, July 06-10, 2005, Edinburgh, Scotland, UK doi:10.1007/11513988_48
6. Tomáš Brázdil, Javier Esparza, Stefan Kiefer, Antonín Kučera, Analyzing Probabilistic Pushdown Automata, Formal Methods in System Design, v.43 n.2, p.124-163, October 2013 doi:10.1007/s10703-012-0166-0
7. Aleksandar Chakarov, Sriram Sankaranarayanan, Probabilistic Program Analysis with Martingales, Proceedings of the 25th International Conference on Computer Aided Verification, July 13-19, 2013, Saint Petersburg, Russia doi:10.1007/978-3-642-39799-8_34
8. M. Codish and S. Genaim. Proving Termination One Loop at a Time. In WLPE, CW371 Report, Pages 48--59. K. U. Leuven, 2003.
9. Michael Colón, Henny Sipma, Synthesis of Linear Ranking Functions, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.67-81, April 02-06, 2001
10. Byron Cook, Abigail See, Florian Zuleger, Ramsey Vs. Lexicographic Termination Proving, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, March 16-24, 2013, Rome, Italy doi:10.1007/978-3-642-36742-7_4
11. 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.
12. Javier Esparza, Andreas Gaiser, Stefan Kiefer, Proving Termination of Probabilistic Programs Using Patterns, Proceedings of the 24th International Conference on Computer Aided Verification, July 07-13, 2012, Berkeley, CA doi:10.1007/978-3-642-31424-7_14
13. Jerzy Filar, Koos Vrieze, Competitive Markov Decision Processes, Springer-Verlag New York, Inc., New York, NY, 1996
14. R. W. Floyd. Assigning Meanings to Programs. Mathematical Aspects of Computer Science, 19:19--32, 1967.
15. F. G. Foster. On the Stochastic Matrices Associated with Certain Queuing Processes. The Annals of Mathematical Statistics, 24(3):355--360, 09 1953.
16. 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.
17. Isabelle Gnaedig, Induction for Positive Almost Sure Termination, Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, July 14-16, 2007, Wroclaw, Poland doi:10.1145/1273920.1273943
18. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, Sriram K. Rajamani, Probabilistic Programming, Proceedings of the on Future of Software Engineering, May 31-June 07, 2014, Hyderabad, India doi:10.1145/2593882.2593900
19. Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver, PRINSYS: On a Quest for Probabilistic Loop Invariants, Proceedings of the 10th International Conference on Quantitative Evaluation of Systems, August 27-30, 2013, Buenos Aires, Argentina doi:10.1007/978-3-642-40196-1_17
20. Friedrich Gretz, Joost-Pieter Katoen, Annabelle Mciver, Operational versus Weakest Pre-expectation Semantics for the Probabilistic Guarded Command Language, Performance Evaluation, 73, p.110-132, March, 2014 doi:10.1016/j.peva.2013.11.004
21. S. Hart and M. Sharir. Concurrent Probabilistic Programs, Or: How to Schedule If You Must. SIAM J. Comput., 14(4):991--1012, 1985.
22. Sergiu Hart, Micha Sharir, Amir Pnueli, Termination of Probabilistic Concurrent Program, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.356-380, July 1983 doi:10.1145/2166.357214
23. Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel, Slicing Probabilistic Programs, Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 09-11, 2014, Edinburgh, United Kingdom doi:10.1145/2594291.2594303
24. Claire Jones, Probabilistic Non-determinism, University of Edinburgh, Edinburgh, Scotland, 1992
25. Joost-Pieter Katoen, Annabelle K. McIver, Larissa A. Meinicke, Carroll C. Morgan, Linear-invariant Generation for Probabilistic Programs: Automated Support for Proof-based Methods, Proceedings of the 17th International Conference on Static Analysis, p.390-406, September 14-16, 2010, Perpignan, France
26. Shmuel Katz, Zohar Manna, A Closer Look at Termination, Acta Informatica, v.5 n.4, p.333-352, December 1975 doi:10.1007/BF00264565
27. D. Kozen. Semantics of Probabilistic Programs. J. Comput. Syst. Sci., 22(3):328--350, 1981.
28. Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, Christoph M. Wintersteiger, Termination Analysis with Compositional Transition Invariants, Proceedings of the 22nd International Conference on Computer Aided Verification, July 15-19, 2010, Edinburgh, UK doi:10.1007/978-3-642-14295-6_9
29. Chin Soon Lee, Neil D. Jones, Amir M. Ben-Amram, The Size-change Principle for Program Termination, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.81-92, January 2001, London, United Kingdom doi:10.1145/360204.360210
30. Annabelle McIver, Carroll Morgan, Abstraction, Refinement And Proof For Probabilistic Systems (Monographs in Computer Science), SpringerVerlag, 2004
31. David Monniaux, An Abstract Analysis of the Probabilistic Termination of Programs, Proceedings of the 8th International Symposium on Static Analysis, p.111-126, July 16-18, 2001
32. Andreas Podelski, Andrey Rybalchenko, Transition Invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.32-41, July 13-17, 2004 doi:10.1109/LICS.2004.50
33. A. Podelski and A. Rybalchenko. A Complete Method for the Synthesis of Linear Ranking Functions. In VMCAI, LNCS 2937:239--251. Springer, 2004.
34. Kirack Sohn, Allen Van Gelder, Termination Detection in Logic Programs Using Argument Sizes (extended Abstract), Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, p.216-226, May 29-31, 1991, Denver, Colorado, USA doi:10.1145/113413.113433
35. D. Williams. Probability with Martingales. Cambridge University Press, 1991.

;

	Author	volume	Date Value	title	type	journal	titleUrl	doi	note	year
2015 ProbabilisticTerminationSoundne	Luis María Ferrer Fioriti Holger Hermanns			Probabilistic Termination: Soundness, Completeness, and Compositionality				10.1145/2676726.2677001		2015