Probabilistic analysis of binary sessions. (English) Zbl 07559470
Konnov, Igor (ed.) et al., 31st international conference on concurrency theory. CONCUR 2020, September 1–4, 2020, Vienna, Austria, virtual conference. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 171, Article 14, 21 p. (2020).
Summary: 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.
For the entire collection see [Zbl 1445.68020].
For the entire collection see [Zbl 1445.68020].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
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. doi:10.1016/j.ic.2005.10.001. · Zbl 1093.68059 · doi: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. doi:10.4204/EPTCS.303.7. · doi: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. doi:10.24963/ijcai.2019/5. · doi: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. doi:10.1007/978-3-030-17184-1_22. · Zbl 1524.68208 · doi: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. doi:10.1145/3371123. · doi: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. doi:10.1145/3290347. · doi:10.1145/3290347 |
| [7] | Yakov Ben-Haim. Info-gap decision theory: decisions under severe uncertainty. Academic Press, 2006. · Zbl 0985.91013 |
| [8] | Giovanni Bernardi and Matthew Hennessy. Using higher-order contracts to model session types. Logical Methods in Computer Science, 12(2), 2016. doi:10.2168/LMCS-12(2:10)2016. · Zbl 1448.68329 · doi: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. doi:10.1007/978-3-642-54830-7_3. · Zbl 1405.68208 · doi: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. doi: 10.1145/2786805.2786832. · doi: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. doi:10.23638/ LMCS-15(4:17)2019. · Zbl 1427.68186 · doi: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. doi:10.1017/S0960129514000218. · Zbl 1361.68162 · doi: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, edi-tors, Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP), pages 219-230. ACM, 2009. doi:10.1145/1599410.1599437. · doi: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. doi:10.1006/inco.1999.2808. 14:17 · Zbl 1045.68564 · doi: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. doi:10.1017/S0960129514000188. · Zbl 1361.68165 · doi:10.1017/S0960129514000188 |
| [16] | Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95-169, 1983. doi:10.1016/0304-3975(83)90059-2. · Zbl 0521.68013 · doi: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. doi:10. 1145/3371118. · doi: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. doi:10.1007/978-3-319-89366-2_5. · Zbl 1491.68120 · doi: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. doi:10.1145/1066677.1066777. · Zbl 1248.68350 · doi: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. doi:10.1007/978-3-642-04081-8_19. · Zbl 1254.68166 · doi: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. doi:10.1016/j.entcs.2007.02.013. · Zbl 1277.68121 · doi:10.1016/j.entcs.2007.02.013 |
| [22] | Seyedeh Sepideh Emam and James Miller. Inferring extended probabilistic finite-state au-tomaton models from software executions. ACM Trans. Softw. Eng. Methodol., 27(1):4:1-4:39, 2018. doi:10.1145/3196883. · doi: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. doi:10.1145/ 2775051.2677001. · Zbl 1345.68104 · doi: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. doi:10.1007/s00236-005-0177-z. · Zbl 1079.68065 · doi: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. doi:10.1007/978-3-642-28540-0_10. · Zbl 1259.68152 · doi: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. doi:10.1007/978-3-540-76637-7_12. · Zbl 1137.68448 · doi: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. doi:10.1109/EMWRT.1992.637477. · doi: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. doi:10. 1007/3-540-46432-8_10. · Zbl 0961.68088 · doi: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. doi:10.1007/3-540-57208-2_35. · Zbl 0939.68642 · doi:10.1007/3-540-57208-2_35 |
| [30] | C O N C U R 2 0 2 0 |
| [31] | 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. doi:10.1145/2873052. · doi:10.1145/2873052 |
| [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. doi:10.1145/2933575.2934574. · Zbl 1401.68201 · doi:10.1145/2933575.2934574 |
| [33] | Joost-Pieter Katoen and Doron A. Peled. Taming confusion for modeling and implement-ing 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. doi:10.1007/978-3-642-37036-6_23. · Zbl 1381.68206 · doi:10.1007/978-3-642-37036-6_23 |
| [34] | John G. Kemeny and J. Laurie Snell. Finite Markov Chains. Springer-Verlag, 1976. · Zbl 0328.60035 |
| [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. doi:10.1145/3293605. · Zbl 1485.68045 · doi: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. doi:10.1007/978-3-540-68679-8_42. · Zbl 1143.68330 · doi: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. doi:10.1007/978-3-662-54577-5_29. · Zbl 1452.68127 · doi: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. doi:10.1017/S0960129519000045. · Zbl 1434.68091 · doi: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. doi:10.1145/3371087. · doi: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. doi:10.1007/978-3-540-24611-4_3. · Zbl 1203.68115 · doi: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. doi:10.1016/0304-3975(94)00171-E. · Zbl 0874.68163 · doi:10.1016/0304-3975(94)00171-E |
| [42] | Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud. Introduction to Interval Analysis. SIAM, 2009. doi:10.1137/1.9780898717716. · Zbl 1168.65002 · doi: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. doi:10.1109/QEST.2007.31. · doi: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. doi:10.1007/978-0-387-35578-8_8. · Zbl 0952.68091 · doi: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. · Zbl 1334.68155 |
| [46] | Springer, 2013. doi:10.1007/978-3-642-39212-2_34. 14:19 · Zbl 1334.68155 · doi:10.1007/978-3-642-39212-2_34 |
| [47] | 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. doi:10.1145/2603088.2603116. · Zbl 1392.68311 · doi:10.1145/2603088.2603116 |
| [48] | Luca Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424-464, 2016. doi:10.1017/S096012951400022X. · Zbl 1361.68172 · doi:10.1017/S096012951400022X |
| [49] | Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. · Zbl 0995.68018 |
| [50] | 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. · Zbl 1069.68074 |
| [51] | Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250-273, 1995. · Zbl 0839.68067 |
| [52] | 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. doi:10.1007/978-3-540-24611-4_1. · Zbl 1203.68089 · doi:10.1007/978-3-540-24611-4_1 |
| [53] | Joseph Tassarotti and Robert Harper. A separation logic for concurrent randomized programs. Proc. ACM Program. Lang., 3(POPL):64:1-64:30, 2019. doi:10.1145/3290377. · Zbl 1511.68342 · doi:10.1145/3290377 |
| [54] | Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Math. Struct. Comput. Sci., 16(1):87-113, 2006. doi:10.1017/S0960129505005074. · Zbl 1093.18002 · doi:10.1017/S0960129505005074 |
| [55] | Daniele Varacca and Nobuko Yoshida. Probabilistic π-calculus and event structures. Electronic Notes in Theoretical Computer Science, 190(3):147-166, 2007. doi:10.1016/j.entcs.2007. 07.009. · Zbl 1279.68269 · doi:10.1016/j.entcs.2007.07.009 |
| [56] | 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. doi:10.1109/SFCS.1985.12. · doi:10.1109/SFCS.1985.12 |
| [57] | 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. doi: 10.1145/3296979.3192408. · doi:10.1145/3296979.3192408 |
| [58] | Lotfi A. Zadeh. Fuzzy sets. Inf. Control., 8(3):338-353, 1965. doi:10.1016/S0019-9958(65) 90241-X. · Zbl 0139.24606 · doi:10.1016/S0019-9958(65)90241-X |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
