Paper published in a book (Scientific congresses, symposiums and conference proceedings)
An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
STUTZ, Felix; D’Osualdo, Emanuele
2025 • In Vafeiadis, Viktor (Ed.) Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings
Communicating state machines; Communication protocols; Multiparty session types; Type checking; Verification; Communicating-state machines; Communications protocols; Multi-party protocols; Multiparty session type; Multiparty sessions; Protocol framework; Protocol state machines; Session types; Typechecking; Theoretical Computer Science; Computer Science (all)
Abstract :
[en] We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a π-calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called “tame”, for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection).
Disciplines :
Computer science
Author, co-author :
STUTZ, Felix ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) ; MPI-SWS, Germany
D’Osualdo, Emanuele ; MPI-SWS, Germany ; University of Konstanz, Konstanz, Germany
External co-authors :
yes
Language :
English
Title :
An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols
Publication date :
01 May 2025
Event name :
34th European Symposium on Programming
Event place :
Hamilton, Canada
Event date :
03-05-2025 => 08-05-2025
Main work title :
Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings
Editor :
Vafeiadis, Viktor
Publisher :
Springer Science and Business Media Deutschland GmbH
Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, 10th International Conference, CAV’98, Vancouver, BC, Canada, June 28-July 2, 1998, Proceedings, Lecture Notes in Computer Science, vol. 1427, pp. 305–318, Springer (1998), https://doi. org/10.1007/BFb0028754
Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. Theor. Comput. Sci. 331(1), 97–114 (2005), https://doi.org/10.1016/j.tcs.2004.09.034
Ancona, D., Bono, V., Bravetti, M., Campos, J., Castagna, G., Deniélou, P., Gay, S.J., Gesbert, N., Giachino, E., Hu, R., Johnsen, E.B., Martins, F., Mascardi, V., Montesi, F., Neykova, R., Ng, N., Padovani, L., Vasconcelos, V.T., Yoshida, N.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2-3), 95–230 (2016), https://doi.org/10. 1561/2500000031
Barbanera, F., Lanese, I., Tuosto, E.: Choreography automata. In: Bliudze, S., Bocchi, L. (eds.) Coordination Models and Languages-22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12134, pp. 86–106, Springer (2020), https://doi.org/10.1007/978-3-030-50029-0_6
Barbanera, F., Lanese, I., Tuosto, E.: Formal choreographic languages. In: ter Beek, M.H., Sirjani, M. (eds.) Coordination Models and Languages-24th IFIP WG 6.1 International Conference, COORDINATION 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13-17, 2022, Proceedings, Lecture Notes in Computer Science, vol. 13271, pp. 121–139, Springer (2022), https://doi.org/10.1007/978-3-031-08143-9_8
Barwell, A.D., Scalas, A., Yoshida, N., Zhou, F.: Generalised multiparty session types with crash-stop failures. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, LIPIcs, vol. 243, pp. 35:1– 35:25, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2022), https://doi.org/10.4230/LIPIcs.CONCUR.2022.35
Bejleri, A., Domnori, E., Viering, M., Eugster, P., Mezini, M.: Comprehensive multiparty session types. Art Sci. Eng. Program. 3(3), 6 (2019), https://doi.org/10.22152/programming-journal.org/2019/3/6
Bocchi, L., Murgia, M., Vasconcelos, V.T., Yoshida, N.: Asynchronous timed session types-from duality to time-sensitive processes. In: Caires, L. (ed.) Programming Languages and Systems-28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11423, pp. 583–610, Springer (2019), https://doi.org/10.1007/978-3-030-17184-1_21
Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification-30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, Lecture Notes in Computer Science, vol. 10982, pp. 372–391, Springer (2018), https://doi.org/10.1007/978-3-319-96142-2_23
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983), https://doi.org/10.1145/322374.322380
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1–8:78 (2012), https://doi.org/10.1145/2220365.2220367
Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Log. Methods Comput. Sci. 8(1) (2012), https://doi. org/10.2168/LMCS-8(1:24)2012
Castellani, I., Dezani-Ciancaglini, M., Giannini, P.: Asynchronous sessions with input races. In: Carbone, M., Neykova, R. (eds.) Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES@ETAPS 2022, Munich, Germany, 3rd April 2022, EPTCS, vol. 356, pp. 12–23 (2022), https://doi.org/10.4204/EPTCS.356.2
Castro-Perez, D., Ferreira, F., Gheri, L., Yoshida, N.: Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In: Freund, S.N., Yahav, E. (eds.) PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, pp. 237–251, ACM (2021), https://doi.org/10.1145/3453483.3454041
Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005), https://doi.org/10.1016/j.ic. 2005.05.006
Chen, R., Balzer, S., Toninho, B.: Ferrite: A judgmental embedding of session types in rust. In: Ali, K., Vitek, J. (eds.) 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany, LIPIcs, vol. 222, pp. 22:1–22:28, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2022), https://doi.org/10.4230/LIPIcs.ECOOP.2022.22
Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci. 26(2), 238–302 (2016), https://doi.org/10.1017/S0960129514000188
Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38–66 (2020), https://doi.org/10.1016/j.tcs.2019. 07.005
Cruz-Filipe, L., Montesi, F., Peressotti, M.: Communications in choreographies, revisited. In: Haddad, H.M., Wainwright, R.L., Chbeir, R. (eds.) Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018, pp. 1248–1255, ACM (2018), https://doi.org/10.1145/3167132.3167267
Dagnino, F., Giannini, P., Dezani-Ciancaglini, M.: Deconfined global types for asynchronous sessions. In: Damiani, F., Dardha, O. (eds.) Coordination Models and Languages-23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, Lecture Notes in Computer Science, vol. 12717, pp. 41–60, Springer (2021), https://doi.org/10.1007/978-3-030-78142-2_3
Das, A., Balzer, S., Hoffmann, J., Pfenning, F., Santurkar, I.: Resource-aware session types for digital contracts. In: 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, pp. 1–16, IEEE (2021), https://doi.org/10.1109/CSF51468.2021.00004
Deniélou, P., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) Programming Languages and Systems-21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24-April 1, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7211, pp. 194–213, Springer (2012), https://doi. org/10.1007/978-3-642-28869-2_10
Deniélou, P., Yoshida, N., Bejleri, A., Hu, R.: Parameterised multiparty session types. Log. Methods Comput. Sci. 8(4) (2012), https://doi.org/10. 2168/LMCS-8(4:6)2012
Fähndrich, M., Aiken, M., Hawblitzel, C., Hodson, O., Hunt, G.C., Larus, J.R., Levi, S.: Language support for fast and reliable message-based communication in singularity OS. In: Berbers, Y., Zwaenepoel, W. (eds.) Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, pp. 177–190, ACM (2006), https://doi.org/10.1145/1217935.1217953
Genest, B., Kuske, D., Muscholl, A.: On communicating automata with bounded channels. Fundam. Inform. 80(1-3), 147–167 (2007), URL http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09
Genest, B., Muscholl, A.: Message sequence charts: A survey. In: Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 6-9 June 2005, St. Malo, France, pp. 2–4, IEEE Computer Society (2005), https://doi.org/10.1109/ACSD.2005.25
Genest, B., Muscholl, A., Peled, D.A.: Message sequence charts. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichstätt, Germany in September 2003. In addition to lectures given at ACPN 2003, additional chapters have been commissioned], Lecture Notes in Computer Science, vol. 3098, pp. 537–558, Springer (2003), https://doi.org/10.1007/978-3-540-27755-2_15
Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state high-level mscs: Model-checking and realizability. J. Comput. Syst. Sci. 72(4), 617– 647 (2006), https://doi.org/10.1016/j.jcss.2005.09.007
Gheri, L., Lanese, I., Sayers, N., Tuosto, E., Yoshida, N.: Design-by-contract for flexible multiparty session protocols. In: Ali, K., Vitek, J. (eds.) 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany, LIPIcs, vol. 222, pp. 8:1–8:28, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2022), https://doi.org/10.4230/LIPICS. ECOOP.2022.8
Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G., Weisenburger, P.: Multiparty languages: The choreographic and multitier cases (pearl). In: Møller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), LIPIcs, vol. 194, pp. 22:1–22:27, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2021), https://doi.org/10.4230/LIPIcs.ECOOP.2021.22
Giusto, C.D., Laversa, L., Lozes, É.: On the k-synchronizability of systems. In: Goubault-Larrecq, J., König, B. (eds.) Foundations of Software Science and Computation Structures-23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12077, pp. 157–176, Springer (2020), https://doi.org/10.1007/978-3-030-45231-5_9
Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, Lecture Notes in Computer Science, vol. 715, pp. 509–523, Springer (1993), https://doi.org/10.1007/3-540-57208-2_35
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp. 273– 284, ACM (2008), https://doi.org/10.1145/1328438.1328472
Hu, R., Yoshida, N.: Explicit connection actions in multiparty session types. In: Huisman, M., Rubin, J. (eds.) Fundamental Approaches to Software Engineering-20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10202, pp. 116–133, Springer (2017), https://doi. org/10.1007/978-3-662-54494-5_7
Jacobs, J., Balzer, S., Krebbers, R.: Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang. 6(POPL), 1–33 (2022), https://doi.org/10.1145/3498662
Jacobs, J., Balzer, S., Krebbers, R.: Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang. 6(ICFP), 466–495 (2022), https://doi.org/10.1145/3547638
Jespersen, T.B.L., Munksgaard, P., Larsen, K.F.: Session types for rust. In: Bahr, P., Erdweg, S. (eds.) Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP 2015, Vancouver, BC, Canada, August 30, 2015, pp. 13–22, ACM (2015), https://doi.org/10.1145/2808098.2808100
Keizer, A.C., Basold, H., Pérez, J.A.: Session coalgebras: A coalgebraic view on regular and context-free session types. ACM Trans. Program. Lang. Syst. 44(3), 18:1–18:45 (2022), https://doi.org/10.1145/3527633
Kobayashi, N.: A new type system for deadlock-free processes. In: CON-CUR, Lecture Notes in Computer Science, vol. 4137, pp. 233–247, Springer (2006), https://doi.org/10.1007/11817949_16
Kouzapas, D., Gutkovas, R., Voinea, A.L., Gay, S.J.: A session type system for asynchronous unreliable broadcast communication. CoRR abs/1902.01353 (2019), URL http://arxiv.org/abs/1902.01353
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978), https://doi.org/10.1145/359545.359563
Lange, J., Ng, N., Toninho, B., Yoshida, N.: A static verification framework for message passing in go using behavioural types. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothen-burg, Sweden, May 27-June 03, 2018, pp. 1137–1148, ACM (2018), https://doi.org/10.1145/3180155.3180157
Li, E., Stutz, F., Wies, T., Zufferey, D.: Complete multiparty session type projection with automata. In: Enea, C., Lal, A. (eds.) Computer Aided Verification-35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, Lecture Notes in Computer Science, vol. 13966, pp. 350–373, Springer (2023), https://doi.org/10.1007/978-3-031-37709-9_17
Lindley, S., Morris, J.G.: Embedding session types in haskell. In: Mainland, G. (ed.) Proceedings of the 9th International Symposium on Haskell, Haskell 2016, Nara, Japan, September 22-23, 2016, pp. 133–145, ACM (2016), https://doi.org/10.1145/2976002.2976018
Lohrey, M.: Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci. 309(1-3), 529–554 (2003), https://doi.org/10. 1016/j.tcs.2003.08.002
Majumdar, R., Mukund, M., Stutz, F., Zufferey, D.: Generalising projection in asynchronous multiparty session types. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, LIPIcs, vol. 203, pp. 35:1–35:24, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2021), https://doi.org/10.4230/LIPIcs.CONCUR.2021.35
Majumdar, R., Pirron, M., Yoshida, N., Zufferey, D.: Motion session types for robotic interactions (brave new idea paper). In: Donaldson, A.F. (ed.) 33rd European Conference on Object-Oriented Programming, ECOOP 2019, July 15-19, 2019, London, United Kingdom, LIPIcs, vol. 134, pp. 28:1–28:27, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2019), https://doi.org/10.4230/LIPIcs.ECOOP.2019.28
Mauw, S., Reniers, M.A.: High-level message sequence charts. In: Cavalli, A.R., Sarma, A. (eds.) SDL ’97 Time for Testing, SDL, MSC and Trends-8th International SDL Forum, Evry, France, 23-29 September 1997, Proceedings, pp. 291–306, Elsevier (1997)
Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in f#. In: Dubach, C., Xue, J. (eds.) Proceedings of the 27th International Conference on Compiler Construction, CC 2018, February 24-25, 2018, Vienna, Austria, pp. 128–138, ACM (2018), https://doi.org/10.1145/3178372. 3179495
Peng, W., Purushothaman, S.: Analysis of a class of communicating finite state machines. Acta Informatica 29(6/7), 499–522 (1992), https://doi.org/10.1007/BF01185558
Roychoudhury, A., Goel, A., Sengupta, B.: Symbolic message sequence charts. ACM Trans. Softw. Eng. Methodol. 21(2), 12:1–12:44 (2012), https://doi.org/10.1145/2089116.2089122
Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: Krishnamurthi, S., Lerner, B.S. (eds.) 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy, LIPIcs, vol. 56, pp. 21:1–21:28, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2016), https://doi.org/10.4230/LIPIcs.ECOOP.2016.21
Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Technical Report 6. Imperial College London (2018), URL https://www. doc.ic.ac.uk/research/technicalreports/2018/DTRS18-6.pdf
Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1–30:29 (2019), https://doi.org/10.1145/3290343
Stutz, F.: Asynchronous multiparty session type implementability is decidable-lessons learned from message sequence charts. In: Ali, K., Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, LIPIcs, vol. 263, pp. 32:1–32:31, Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2023), https://doi.org/10.4230/LIPIcs.ECOOP.2023.32
Stutz, F.: Implementability of Asynchronous Communication Protocols-The Power of Choice. Ph.D. thesis, Kaiserslautern University of Technology, Germany (2024), URL https://kluedo.ub.rptu.de/frontdoor/index/index/docId/8077
Stutz, F., D’Osualdo, E.: An automata-theoretic basis for specification and type checking of multiparty protocols. CoRR abs/2501.16977 (2025), https://doi.org/10.48550/arXiv.2501.16977
Stutz, F., Zufferey, D.: Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types. In: Ganty, P., Monica, D.D. (eds.) Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2022, Madrid, Spain, September 21-23, 2022, EPTCS, vol. 370, pp. 194–212 (2022), https://doi.org/10.4204/EPTCS.370.13
Thiemann, P.: Intrinsically-typed mechanized semantics for session types. In: Komendantskaya, E. (ed.) Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pp. 19:1–19:15, ACM (2019), https://doi.org/10.1145/3354166.3354184
Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pp. 462–475, ACM (2016), https://doi.org/10.1145/2951913.2951926
Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Schneider-Kamp, P., Hanus, M. (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark, pp. 161–172, ACM (2011), https://doi.org/10.1145/2003476.2003499
Toninho, B., Yoshida, N.: Depending on session-typed processes. In: Baier, C., Lago, U.D. (eds.) 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, Lecture Notes in Computer Science, vol. 10803, pp. 128–145, Springer (2018), https: //doi.org/10.1007/978-3-319-89366-2_7
Torre, S.L., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 299–314, Springer (2008), https://doi.org/10.1007/978-3-540-78800-3_21
Union, I.T.: Z.120: Message sequence chart. Tech. rep., International Telecommunication Union (October 1996), URL https://www.itu.int/rec/T-REC-Z.120
Viering, M., Hu, R., Eugster, P., Ziarek, L.: A multiparty session typing discipline for fault-tolerant event-driven distributed programming. Proc. ACM Program. Lang. 5(OOPSLA), 1–30 (2021), https://doi.org/10.1145/3485501
Yoshida, N., Hu, R., Neykova, R., Ng, N.: The scribble protocol language. In: Abadi, M., Lluch-Lafuente, A. (eds.) Trustworthy Global Computing-8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, Lecture Notes in Computer Science, vol. 8358, pp. 22–41, Springer (2013), https://doi.org/10.1007/978-3-319-05119-2_3
