Document Open Access Logo

Almost Sure Productivity

Authors Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2018.113.pdf
  • Filesize: 460 kB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Probabilistic computation
  • Theory of computation → Program reasoning
Keywords
  • Coinduction
  • Probabilistic Programming
  • Productivity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We introduce Almost Sure Productivity (ASP), a probabilistic generalization of the productivity condition for coinductively defined structures. Intuitively, a probabilistic coinductive stream or tree is ASP if it produces infinitely many outputs with probability 1. Formally, we define ASP using a final coalgebra semantics of programs inspired by Kerstan and König. Then, we introduce a core language for probabilistic streams and trees, and provide two approaches to verify ASP: a syntactic sufficient criterion, and a decision procedure by reduction to model{-}checking LTL formulas on probabilistic pushdown automata.

Cite As Get BibTex

Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva. Almost Sure Productivity. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 113:1-113:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ICALP.2018.113

Author Details

Alejandro Aguirre
  • IMDEA Software Institute, Madrid, Spain
Gilles Barthe
  • IMDEA Software Institute, Madrid, Spain
Justin Hsu
  • University College London, London, UK
Alexandra Silva
  • University College London, London, UK

References

  1. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: Programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 27-38, 2013. URL: http://dx.doi.org/10.1145/2429069.2429075.
  2. Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proceedings of the ACM on Programming Languages, 2(POPL):34:1-34:32, 2018. URL: http://dx.doi.org/10.1145/3158122.
  3. Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. Relational reasoning for Markov chains in a probabilistic guarded lambda calculus. In European Symposium on Programming (ESOP), Thessaloniki, Greece, Lecture Notes in Computer Science. Springer-Verlag, 2018. Google Scholar
  4. Tamarah Arons, Amir Pnueli, and Lenore D. Zuck. Parameterized verification by probabilistic abstraction. In Andrew D. Gordon, editor, International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Warsaw, Poland, volume 2620 of Lecture Notes in Computer Science, pages 87-102. Springer-Verlag, 2003. URL: http://dx.doi.org/10.1007/3-540-36576-1_6.
  5. S. Awodey. Category Theory. Oxford Logic Guides. Ebsco Publishing, 2006. URL: https://books.google.es/books?id=IK_sIDI2TCwC.
  6. Tomáš Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kučera. Analyzing probabilistic pushdown automata. Formal Methods in System Design, 43(2):124-163, Oct 2013. URL: http://dx.doi.org/10.1007/s10703-012-0166-0.
  7. Venanzio Capretta and Jonathan Fowler. The continuity of monadic stream functions. In IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005119.
  8. Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia, pages 511-526, 2013. URL: https://www.cs.colorado.edu/~srirams/papers/cav2013-martingales.pdf.
  9. Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through Positivstellensatz’s. In International Conference on Computer Aided Verification (CAV), Toronto, Ontario, volume 9779 of Lecture Notes in Computer Science, pages 3-22. Springer-Verlag, 2016. URL: http://dx.doi.org/10.1007/978-3-319-41528-4_1.
  10. Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Saint Petersburg, Florida, pages 327-342, 2016. URL: http://dx.doi.org/10.1145/2837614.2837639.
  11. Krishnendu Chatterjee, Petr Novotný, and \DHorđe Žikelić. Stochastic invariants for probabilistic termination. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pages 145-160, 2017. URL: http://dx.doi.org/10.1145/3009837.3009873.
  12. Ranald Clouston, Ales Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. The guarded lambda-calculus: Programming and reasoning with guarded recursion for coinductive types. Logical Methods in Computer Science, 12(3), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(3:7)2016.
  13. Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks. Data-oblivious stream productivity. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Doha, Qatar, volume 5330 of Lecture Notes in Computer Science, pages 79-96. Springer-Verlag, 2008. URL: http://dx.doi.org/10.1007/978-3-540-89439-1_6.
  14. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem Klop. Productivity of stream definitions. Theor. Comput. Sci., 411(4-5):765-782, 2010. URL: http://dx.doi.org/10.1016/j.tcs.2009.10.014.
  15. Javier Esparza, Andreas Gaiser, and Stefan Kiefer. Proving termination of probabilistic programs using patterns. In P. Madhusudan and Sanjit A. Seshia, editors, International Conference on Computer Aided Verification (CAV), Berkeley, California, volume 7358 of Lecture Notes in Computer Science, pages 123-138. Springer-Verlag, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31424-7_14.
  16. Luis María Ferrer Fioriti and Holger Hermanns. Probabilistic termination: Soundness, completeness, and compositionality. In Sriram K. Rajamani and David Walker, editors, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, pages 489-501, 2015. URL: http://dx.doi.org/10.1145/2676726.2677001.
  17. Sergiu Hart, Micha Sharir, and Amir Pnueli. Termination of probabilistic concurrent program. ACM Trans. Program. Lang. Syst., 5(3):356-380, 1983. URL: http://dx.doi.org/10.1145/2166.357214.
  18. John Hughes, Lars Pareto, and Amr Sabry. Proving the correctness of reactive systems using sized types. In Hans-Juergen Boehm and Guy L. Steele Jr., editors, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 410-423, 1996. URL: http://dx.doi.org/10.1145/237721.240882.
  19. Benjamin Lucien Kaminski and Joost-Pieter Katoen. On the hardness of almost-sure termination. In Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors, Symposium on Mathematical Foundations of Computer Science (MFCS), Milan, Italy, volume 9234 of Lecture Notes in Computer Science, pages 307-318. Springer-Verlag, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48057-1_24.
  20. Henning Kerstan and Barbara König. Coalgebraic trace semantics for continuous probabilistic transition systems. Logical Methods in Computer Science, 9(4), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(4:16)2013.
  21. Ekaterina Komendantskaya, Patricia Johann, and Martin Schmidt. A productivity checker for logic programming. In Manuel V. Hermenegildo and Pedro López-García, editors, International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Edinburgh, Scotland, volume 10184 of Lecture Notes in Computer Science, pages 168-186. Springer-Verlag, 2016. URL: http://dx.doi.org/10.1007/978-3-319-63139-4_10.
  22. Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, 1981. URL: http://dx.doi.org/10.1016/0022-0000(81)90036-2.
  23. Dexter Kozen. A probabilistic PDL. In ACM SIGACT Symposium on Theory of Computing (STOC), Boston, Massachusetts, pages 291-297, 1983. URL: http://dx.doi.org/10.1145/800061.808758.
  24. Dexter Kozen. Realization of coinductive types. Electronic Notes in Theoretical Computer Science, 276:237-246, 2011. URL: http://dx.doi.org/10.1016/j.entcs.2011.09.024.
  25. Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized typing. In Hongseok Yang, editor, European Symposium on Programming (ESOP), Uppsala, Sweden, volume 10201 of Lecture Notes in Computer Science, pages 393-419. Springer-Verlag, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54434-1_15.
  26. David A. Levin, Yuval Peres, and Elizabeth L. Wilmer. Markov Chains and Mixing Times. American Mathematical Society, 2009. URL: https://pages.uoregon.edu/dlevin/MARKOV/markovmixing.pdf.
  27. Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages, 2(POPL):33:1-33:28, 2018. URL: http://dx.doi.org/10.1145/3158121.
  28. Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. toplas, 18(3):325-353, 1996. URL: http://dx.doi.org/10.1145/229542.229547.
  29. Amir Pnueli. The temporal logic of programs. In IEEE Symposium on Foundations of Computer Science (FOCS), Providence, Rhode Island, pages 46-57, 1977. URL: http://dx.doi.org/10.1109/SFCS.1977.32.
  30. Walter Rudin. Real and Complex Analysis. McGraw-Hill, New York, third edition, 1987. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact