Difference between revisions of "2015 ProbabilisticTerminationSoundne"

From GM-RKB
Jump to: navigation, search
m (Omoreira moved page Test:2015 ProbabilisticTerminationSoundne to 2015 ProbabilisticTerminationSoundne without leaving a redirect)
Line 21: Line 21:
 
This is integrated in a [[small dependent type system]], to overcome the problem that lexicographic [[ranking function]]s fail when combined with [[randomization]]. </s>
 
This is integrated in a [[small dependent type system]], to overcome the problem that lexicographic [[ranking function]]s fail when combined with [[randomization]]. </s>
 
Among others, [[this compositional methodology]] enables the verification of [[probabilistic program]]s outside the [[complete class]] that admits [[ranking]] [[supermartingale]]s. </s>
 
Among others, [[this compositional methodology]] enables the verification of [[probabilistic program]]s outside the [[complete class]] that admits [[ranking]] [[supermartingale]]s. </s>
 +
 +
=== Body ===
 +
<B>Theorem 5.6 (Soundness).</B> Let <math>P</math> be a [[probabilistic program]] with [[semantics]]] <math>{(L, X) φ n}</math>, and a [[ranking]] [[supermartingale]] <math>{Y_n}</math> such that <math>Y_n = 0</math> implies <math>T φ ≤ n</math> for all valid schedulers φ. Then, P almost sure terminates, and T ∗ is integrable.
  
 
==References==
 
==References==
{{#ifanon:|
+
 
 
* 1. R. B. Ash and C. Doléans-Dade. Probability and Measure Theory. Harcourt, 2000.
 
* 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 [http://doi.acm.org/10.1145/1190216.1190249 doi:10.1145/1190216.1190249]
 
* 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 [http://doi.acm.org/10.1145/1190216.1190249 doi:10.1145/1190216.1190249]
Line 59: Line 62:
 
* 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 [http://doi.acm.org/10.1145/113413.113433 doi:10.1145/113413.113433]
 
* 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 [http://doi.acm.org/10.1145/113413.113433 doi:10.1145/113413.113433]
 
* 35. D. Williams. Probability with Martingales. Cambridge University Press, 1991.
 
* 35. D. Williams. Probability with Martingales. Cambridge University Press, 1991.
 
}}
 
  
 
__NOTOC__
 
__NOTOC__

Revision as of 04:53, 14 June 2019

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]P[/math] be a probabilistic program with semantics] [math]{(L, X) φ n}[/math], and a ranking supermartingale [math]{Y_n}[/math] such that [math]Y_n = 0[/math] implies [math]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.;


 AuthorvolumeDate ValuetitletypejournaltitleUrldoinoteyear
2015 ProbabilisticTerminationSoundneLuis María Ferrer Fioriti
Holger Hermanns
Probabilistic Termination: Soundness, Completeness, and Compositionality10.1145/2676726.26770012015
AuthorLuis María Ferrer Fioriti + and Holger Hermanns +
doi10.1145/2676726.2677001 +
titleProbabilistic Termination: Soundness, Completeness, and Compositionality +
year2015 +