Document Open Access Logo

Probabilistic Analysis of Binary Sessions

Authors Omar Inverso , Hernán Melgratti , Luca Padovani , Catia Trubiani , Emilio Tuosto

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.14.pdf
  • Filesize: 0.56 MB
  • 21 pages

Document Identifiers

Author Details

Omar Inverso
  • Gran Sasso Science Institute, L'Aquila, Italy
Hernán Melgratti
  • ICC, Universidad de Buenos Aires, Conicet, Argentina
Luca Padovani
  • Università di Torino, Italy
Catia Trubiani
  • Gran Sasso Science Institute, L'Aquila, Italy
Emilio Tuosto
  • Gran Sasso Science Institute, L'Aquila, Italy

Funding

Hernán Melgratti, Luca Padovani and Emilio Tuosto have been partially supported by EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No 778233.
  • Inverso, Omar: Omar Inverso has been partially supported by MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems).
  • Melgratti, Hernán: Hernán Melgratti has been partially supported by UBACyT projects 20020170100544BA and 20020170100086BA and PIP project 11220130100148CO.
  • Trubiani, Catia: Catia Trubiani has been partially supported by MIUR project PRIN 2017TWRCNB SEDUCE (Designing Spatially Distributed Cyber-Physical Systems under Uncertainty).

Acknowledgements

#2{The authors are grateful to the anonymous reviewers for their detailed feedback. }

Cite AsGet BibTex

Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani, and Emilio Tuosto. Probabilistic Analysis of Binary Sessions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.14

Abstract

We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
Keywords
  • Probabilistic choices
  • session types
  • static analysis
  • deadlock freedom

Metrics

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

Related Versions

References

  1. Samy Abbes and Albert Benveniste. True-concurrency probabilistic models: Branching cells and distributed probabilities for event structures. Information and Computation, 204(2):231-274, 2006. URL: https://doi.org/10.1016/j.ic.2005.10.001.
  2. Bogdan Aman and Gabriel Ciobanu. Probabilities in session types. In Mircea Marin and Adrian Craciun, editors, Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timişoara, Romania, 3-5 September 2019, volume 303 of EPTCS, pages 92-106, 2019. URL: https://doi.org/10.4204/EPTCS.303.7.
  3. Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, and Sasha Rubin. Probabilistic strategy logic. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), pages 32-38, 2019. URL: https://doi.org/10.24963/ijcai.2019/5.
  4. Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In Proceedings of the European Symposium on Programming Languages (ESOP), volume 11423, pages 611-639. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_22.
  5. Gilles Barthe, Justin Hsu, and Kevin Liao. A probabilistic separation logic. Proc. ACM Program. Lang., 4(POPL):55:1-55:30, 2020. URL: https://doi.org/10.1145/3371123.
  6. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang., 3(POPL):34:1-34:29, 2019. URL: https://doi.org/10.1145/3290347.
  7. Yakov Ben-Haim. Info-gap decision theory: decisions under severe uncertainty. Academic Press, 2006. Google Scholar
  8. Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, 12(2), 2016. URL: https://doi.org/10.2168/LMCS-12(2:10)2016.
  9. Rémi Bonnet, Stefan Kiefer, and Anthony Widjaja Lin. Analysis of probabilistic basic parallel processes. In Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 8412, pages 43-57. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_3.
  10. Mateus Borges, Antonio Filieri, Marcelo d'Amorim, and Corina S. Pasareanu. Iterative distribution-aware sampling for probabilistic symbolic execution. In Proceedings of the Joint Meeting on Foundations of Software Engineering (ESEC/FSE), pages 866-877, 2015. URL: https://doi.org/10.1145/2786805.2786832.
  11. Roberto Bruni, Hernán C. Melgratti, and Ugo Montanari. Concurrency and probability: Removing confusion, compositionally. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:17)2019.
  12. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Math. Struct. Comput. Sci., 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  13. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. Foundations of session types. In António Porto and Francisco Javier López-Fraguas, editors, Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP), pages 219-230. ACM, 2009. URL: https://doi.org/10.1145/1599410.1599437.
  14. Rance Cleaveland, Zeynep Dayar, Scott A. Smolka, and Shoji Yuen. Testing preorders for probabilistic processes. Inf. Comput., 154(2):93-148, 1999. URL: https://doi.org/10.1006/inco.1999.2808.
  15. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci., 26(2):238-302, 2016. URL: https://doi.org/10.1017/S0960129514000188.
  16. Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95-169, 1983. URL: https://doi.org/10.1016/0304-3975(83)90059-2.
  17. David Darais, Ian Sweet, Chang Liu, and Michael Hicks. A language for probabilistically oblivious computation. Proc. ACM Program. Lang., 4(Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)):50:1-50:31, 2020. URL: https://doi.org/10.1145/3371118.
  18. Ornela Dardha and Simon J. Gay. A new linear logic for deadlock-free session-typed processes. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 91-109. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_5.
  19. Rocco De Nicola, Diego Latella, and Mieke Massink. Formal modeling and quantitative analysis of klaim-based mobile systems. In Proceedings of the ACM symposium on Applied computing (SAC), pages 428-435, 2005. URL: https://doi.org/10.1145/1066677.1066777.
  20. Yuxin Deng, Rob Van Glabbeek, Matthew Hennessy, and Carroll Morgan. Testing finitary probabilistic processes. In Proceedings of the International Conference on Concurrency Theory (CONCUR), pages 274-288. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_19.
  21. Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan, and Chenyi Zhang. Remarks on testing probabilistic processes. Electron. Notes Theor. Comput. Sci., 172:359-397, 2007. URL: https://doi.org/10.1016/j.entcs.2007.02.013.
  22. Seyedeh Sepideh Emam and James Miller. Inferring extended probabilistic finite-state automaton models from software executions. ACM Trans. Softw. Eng. Methodol., 27(1):4:1-4:39, 2018. URL: https://doi.org/10.1145/3196883.
  23. Luis María Ferrer Fioriti and Holger Hermanns. Probabilistic termination: Soundness, completeness, and compositionality. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 489-501. ACM, 2015. URL: https://doi.org/10.1145/2775051.2677001.
  24. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Inf., 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/s00236-005-0177-z.
  25. Sonja Georgievska and Suzana Andova. Probabilistic CSP: preserving the laws via restricted schedulers. In Proceedings of the International GI/ITG Conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB/DFT), volume 7201, pages 136-150. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28540-0_10.
  26. Jean Goubault-Larrecq, Catuscia Palamidessi, and Angelo Troina. A probabilistic applied pi-calculus. In Zhong Shao, editor, Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings, volume 4807 of Lecture Notes in Computer Science, pages 175-190. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76637-7_12.
  27. Hans A. Hansson. Time and probabilities in specification and verification of real-time systems. In Proceedings of the Euromicro workshop on Real-Time Systems (RTS), pages 92-97, 1992. URL: https://doi.org/10.1109/EMWRT.1992.637477.
  28. Oltea Mihaela Herescu and Catuscia Palamidessi. Probabilistic asynchronous π-calculus. In Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 1784, pages 146-160. Springer, 2000. URL: https://doi.org/10.1007/3-540-46432-8_10.
  29. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, Proceedings of the International Conference on Concurrency Theory (CONCUR), volume 715, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  30. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  31. Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani, and Emilio Tuosto. Probabilistic Analysis of Binary Sessions. Technical report, Università di Torino, 2020. URL: https://doi.org/10.5281/zenodo.3951070.
  32. Joost-Pieter Katoen. The probabilistic model checking landscape. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 31-45. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934574.
  33. Joost-Pieter Katoen and Doron A. Peled. Taming confusion for modeling and implementing probabilistic concurrent systems. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7792 of Lecture Notes in Computer Science, pages 411-430. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_23.
  34. John G. Kemeny and J. Laurie Snell. Finite Markov Chains. Springer-Verlag, 1976. Google Scholar
  35. Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst., 41(2):10:1-10:65, 2019. URL: https://doi.org/10.1145/3293605.
  36. Cosimo Laneve and Luca Padovani. The pairing of contracts and session types. In Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, volume 5065, pages 681-700. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-68679-8_42.
  37. Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Philipp Rümmer. Fair termination for parameterized probabilistic concurrent systems. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 10205, pages 499-517, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_29.
  38. Thomas Leventis. A deterministic rewrite system for the probabilistic λ-calculus. Math. Struct. Comput. Sci., 29(10):1479-1512, 2019. URL: https://doi.org/10.1017/S0960129519000045.
  39. Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka. Trace types and denotational semantics for sound programmable inference in probabilistic languages. Proc. ACM Program. Lang., 4(POPL):19:1-19:32, 2020. URL: https://doi.org/10.1145/3371087.
  40. Natalia López and Manuel Núñez. An overview of probabilistic process algebras and their equivalences. In Validation of Stochastic Systems - A Guide to Current Research, volume 2925, pages 89-123. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24611-4_3.
  41. Gavin Lowe. Probabilistic and prioritized models of timed CSP. Theor. Comput. Sci., 138(2):315-352, 1995. URL: https://doi.org/10.1016/0304-3975(94)00171-E.
  42. Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud. Introduction to Interval Analysis. SIAM, 2009. URL: https://doi.org/10.1137/1.9780898717716.
  43. Gethin Norman, Catuscia Palamidessi, David Parker, and Peng Wu. Model checking the probabilistic pi-calculus. In Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST 2007), 17-19 September 2007, Edinburgh, Scotland, UK, pages 169-178. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/QEST.2007.31.
  44. Manuel Núñez and David Rupérez. Fair testing through probabilistic testing. In Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (PSTV), volume 156, pages 135-150. Kluwer, 1999. URL: https://doi.org/10.1007/978-0-387-35578-8_8.
  45. Luca Padovani. Fair subtyping for open session types. In Proceedings of the International Colloquium on Automata, Languages, and Programming (ICALP), volume 7966, pages 373-384. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_34.
  46. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Proceedings of the Joint Meeting of the EACSL Annual Conference on Computer Science Logic and the Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS), pages 72:1-72:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603116.
  47. Luca Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424-464, 2016. URL: https://doi.org/10.1017/S096012951400022X.
  48. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  49. Jan J. M. M. Rutten, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Prakash Panangaden. Mathematical techniques for analyzing concurrent and probabilistic systems, volume 23 of CRM monograph series. American Mathematical Society, 2004. Google Scholar
  50. Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250-273, 1995. Google Scholar
  51. Ana Sokolova and Erik P. de Vink. Probabilistic automata: System types, parallel composition and comparison. In Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen, and Markus Siegle, editors, Validation of Stochastic Systems - A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, pages 1-43. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24611-4_1.
  52. Joseph Tassarotti and Robert Harper. A separation logic for concurrent randomized programs. Proc. ACM Program. Lang., 3(POPL):64:1-64:30, 2019. URL: https://doi.org/10.1145/3290377.
  53. Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Math. Struct. Comput. Sci., 16(1):87-113, 2006. URL: https://doi.org/10.1017/S0960129505005074.
  54. Daniele Varacca and Nobuko Yoshida. Probabilistic π-calculus and event structures. Electronic Notes in Theoretical Computer Science, 190(3):147-166, 2007. URL: https://doi.org/10.1016/j.entcs.2007.07.009.
  55. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21-23 October 1985, pages 327-338. IEEE Computer Society, 1985. URL: https://doi.org/10.1109/SFCS.1985.12.
  56. Di Wang, Jan Hoffmann, and Thomas W. Reps. PMAF: an algebraic framework for static analysis of probabilistic programs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 513-528, 2018. URL: https://doi.org/10.1145/3296979.3192408.
  57. Lotfi A. Zadeh. Fuzzy sets. Inf. Control., 8(3):338-353, 1965. URL: https://doi.org/10.1016/S0019-9958(65)90241-X.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact