Characterizing Implementability of Global Protocols with Infinite States and Data

Li, Elaine; STUTZ, Felix; Wies, Thomas; Zufferey, Damien

doi:10.1145/3720493

Download

Paper published in a journal (Scientific congresses, symposiums and conference proceedings)

Characterizing Implementability of Global Protocols with Infinite States and Data

Li, Elaine; STUTZ, Felix; Wies, Thomas et al.

2025 • In Proceedings of the ACM on Programming Languages, 9 (1), p. 1434-1463

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/10993/67528

DOI
10.1145/3720493

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

oopsla25-symbolic.pdf

Publisher postprint (419.78 kB)

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Data refinements; Implementability; Message-passing; Protocol verification; Synthesis; μCLP reduction; Communications protocols; Infinite-state; State values; ΜCLP reduction; Safety, Risk, Reliability and Quality

Abstract :

[en] We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. Our symbolic protocols describe infinite states and data values using dependent refinement predicates. Implementability asks whether a global protocol specification admits a distributed, asynchronous implementation, namely one for each participant, that is deadlock-free and exhibits the same behavior as the specification. We provide a unified explanation of seemingly disparate sources of non-implementability through a precise semantic characterization of implementability for infinite protocols. Our characterization reduces the problem of implementability to (co)reachability in the global protocol restricted to each participant. This compositional reduction yields the first sound and relatively complete algorithm for checking implementability of symbolic protocols. We use our characterization to show that for finite protocols, implementability is co-NP-complete for explicit representations and PSPACE-complete for symbolic representations. The finite, explicit fragment subsumes a previously studied fragment of multiparty session types for which our characterization yields a co-NP decision procedure, tightening a prior PSPACE upper bound.

Disciplines :

Computer science

Author, co-author :

Li, Elaine ; New York University, United States

STUTZ, Felix ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)

Wies, Thomas ; New York University, United States

Zufferey, Damien ; NVIDIA, Switzerland

External co-authors :

yes

Language :

English

Title :

Characterizing Implementability of Global Protocols with Infinite States and Data

Publication date :

09 April 2025

Event name :

OOPSLA 2025

Event date :

Sun 12 - Sat 18 October 2025

Journal title :

Proceedings of the ACM on Programming Languages

eISSN :

2475-1421

Publisher :

Association for Computing Machinery

Volume :

Issue :

Pages :

1434-1463

Peer reviewed :

Peer Reviewed verified by ORBi

Additional URL :

https://dl.acm.org/doi/10.1145/3720493

FnR Project :

C22/IS/17238244/AVVA

Funders :

NSF
FNR - Luxembourg National Research Fund

Available on ORBilu :

since 28 January 2026

Statistics

Number of views

6 (0 by Unilu)

Number of downloads

2 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

WoS citations^™

Bibliography

Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. 2003. Inference of Message Sequence Charts. IEEE Trans. Software Eng. 29, 7 (2003), 623-633. https://doi. org/10. 1109/TSE. 2003. 1214326
Rajeev Alur, Kousha Etessami, and Mihalis Yannakakis. 2005. Realizability and verification of MSC graphs. Theor. Comput. Sci. 331, 1 (2005), 97-114. https://doi. org/10. 1016/J. TCS. 2004. 09. 034
Rajeev Alur and Mihalis Yannakakis. 1999. Model Checking of Message Sequence Charts. In CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings (Lecture Notes in Computer Science, Vol. 1664), Jos C. M. Baeten and Sjouke Mauw (Eds.). Springer, 114-129. https://doi. org/10. 1007/3-540-48320-9_10
Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Pierre Carlier. 2018. When are stochastic transition systems tameable? J. Log. Algebraic Methods Program. 99 (2018), 41-96. https://doi. org/10. 1016/J. JLAMP. 2018. 03. 004
Nathalie Bertrand, Amélie Stainer, Thierry Jéron, and Moez Krichen. 2015. A game approach to determinize timed automata. Formal Methods Syst. Des. 46, 1 (2015), 42-80. https://doi. org/10. 1007/S10703-014-0220-1
Laura Bocchi, Romain Demangeon, and Nobuko Yoshida. 2012. A Multiparty Multi-session Logic. In Trustworthy Global Computing-7th International Symposium, TGC 2012, Newcastle upon Tyne, UK, September 7-8, 2012, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 8191), Catuscia Palamidessi and Mark Dermot Ryan (Eds.). Springer, 97-111. https://doi. org/10. 1007/978-3-642-41157-1_7
Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. 2010. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In CONCUR 2010-Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6269), Paul Gastin and François Laroussinie (Eds.). Springer, 162-176. https://doi. org/10. 1007/978-3-642-15375-4_12
Daniel Brand and Pitro Zafiropulo. 1983. On Communicating Finite-State Machines. J. ACM 30, 2 (1983), 323-342. https://doi. org/10. 1145/322374. 322380
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2022. Asynchronous Sessions with Input Races. In 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), Marco Carbone and Rumyana Neykova (Eds.). 12-23. https://doi. org/10. 4204/EPTCS. 356. 2
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. 2024. Global Types and Event Structure Semantics for Asynchronous Multiparty Sessions. Fundam. Informaticae 192, 1 (2024), 1-75. https://doi. org/10. 3233/FI-242188
David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. 2019. Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. Proc. ACM Program. Lang. 3, POPL (2019), 29:1-29:30. https://doi. org/10. 1145/3290342
David Castro-Perez and Nobuko Yoshida. 2023. Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols. In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States (LIPIcs, Vol. 263), Karim Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 6:1-6:30. https://doi. org/10. 4230/LIPICS. ECOOP. 2023. 6
Lorenzo Clemente, Slawomir Lasota, and Radoslaw Piórkowski. 2022. Determinisability of register and timed automata. Log. Methods Comput. Sci. 18, 2 (2022). https://doi. org/10. 46298/LMCS-18(2:9)2022
Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. 2015. A Gentle Introduction to Multiparty Asynchronous Session Types. In Formal Methods for Multicore Programming-15th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2015, Bertinoro, Italy, June 15-19, 2015, Advanced Lectures (Lecture Notes in Computer Science, Vol. 9104), Marco Bernardo and Einar Broch Johnsen (Eds.). Springer, 146-178. https://doi. org/10. 1007/978-3-319-18941-3_4
Luís Cruz-Filipe and Fabrizio Montesi. 2020. A core model for choreographic programming. Theor. Comput. Sci. 802 (2020), 38-66. https://doi. org/10. 1016/j. tcs. 2019. 07. 005
Zak Cutner, Nobuko Yoshida, and Martin Vassor. 2022. Deadlock-free asynchronous message reordering in rust with multiparty session types. In PPoPP '22: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2-6, 2022, Jaejin Lee, Kunal Agrawal, and Michael F. Spear (Eds.). ACM, 246-261. https://doi. org/10. 1145/3503221. 3508404
Francesco Dagnino, Paola Giannini, and Mariangiola Dezani-Ciancaglini. 2021. Deconfined Global Types for Asynchronous Sessions. In 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), Ferruccio Damiani and Ornela Dardha (Eds.). Springer, 41-60. https://doi. org/10. 1007/978-3-030-78142-2_3
Haitao Dan, Robert M. Hierons, and Steve Counsell. 2010. Non-local Choice and Implied Scenarios. In 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, Pisa, Italy, 13-18 September 2010, José Luiz Fiadeiro, Stefania Gnesi, and Andrea Maggiolo-Schettini (Eds.). IEEE Computer Society, 53-62. https: //doi. org/10. 1109/SEFM. 2010. 14
Loris D'Antoni, Tiago Ferreira, Matteo Sammartino, and Alexandra Silva. 2019. Symbolic Register Automata. In Computer Aided Verification-31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 11561), Isil Dillig and Serdar Tasiran (Eds.). Springer, 3-21. https://doi. org/10. 1007/978-3-030-25540-4_1
Loris D'Antoni and Margus Veanes. 2017. The Power of Symbolic Automata and Transducers. In Computer Aided Verification-29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 10426), Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 47-67. https://doi. org/10. 1007/978-3-319-63387-9_3
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar. 2021. Resource-Aware Session Types for Digital Contracts. In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021. IEEE, 1-16. https://doi. org/10. 1109/CSF51468. 2021. 00004
Ankush Das and Frank Pfenning. 2020. Session Types with Arithmetic Refinements. In 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference) (LIPIcs, Vol. 171), Igor Konnov and Laura Kovács (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 13:1-13:18. https://doi. org/10. 4230/LIPICS. CONCUR. 2020. 13
Ankush Das and Frank Pfenning. 2022. Rast: A Language for Resource-Aware Session Types. Log. Methods Comput. Sci. 18, 1 (2022). https://doi. org/10. 46298/LMCS-18(1:9)2022
Jan de Muijnck-Hughes and Wim Vanderbauwhede. 2019. A Typing Discipline for Hardware Interfaces. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 134), Alastair F. Donaldson (Ed.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 6:1-6:27. https://doi. org/10. 4230/LIPIcs. ECOOP. 2019. 6
Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. 2015. Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Formal Methods Syst. Des. 46, 3 (2015), 197-225. https://doi. org/10. 1007/S10703-014-0218-8
Volker Diekert and Grzegorz Rozenberg (Eds.). 1995. The Book of Traces. World Scientific. https://doi. org/10. 1142/2563
Javier Esparza and Mogens Nielsen. 1994. Decidability Issues for Petri Nets-a survey. J. Inf. Process. Cybern. 30, 3 (1994), 143-160.
Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen C. Hunt, James R. Larus, and Steven Levi. 2006. Language support for fast and reliable message-based communication in singularity OS. In Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, Yolande Berbers and Willy Zwaenepoel (Eds.). ACM, 177-190. https://doi. org/10. 1145/1217935. 1217953
Alain Finkel and Étienne Lozes. 2023. Synchronizability of Communicating Finite State Machines is not Decidable. Log. Methods Comput. Sci. 19, 4 (2023). https://doi. org/10. 46298/LMCS-19(4:33)2023
Thomas Gazagnaire, Blaise Genest, Loïc Hélouët, P. S. Thiagarajan, and Shaofa Yang. 2007. Causal Message Sequence Charts. In CONCUR 2007-Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings (Lecture Notes in Computer Science, Vol. 4703), Luís Caires and Vasco Thudichum Vasconcelos (Eds.). Springer, 166-180. https://doi. org/10. 1007/978-3-540-74407-8_12
Blaise Genest and Anca Muscholl. 2005. 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. IEEE Computer Society, 2-4. https://doi. org/10. 1109/ACSD. 2005. 25
Blaise Genest, Anca Muscholl, and Doron A. Peled. 2003. Message Sequence Charts. In 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), Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg (Eds.). Springer, 537-558. https://doi. org/10. 1007/978-3-540-27755-2_15
Blaise Genest, Anca Muscholl, Helmut Seidl, and Marc Zeitoun. 2006. Infinite-state high-level MSCs: Model-checking and realizability. J. Comput. Syst. Sci. 72, 4 (2006), 617-647. https://doi. org/10. 1016/j. jcss. 2005. 09. 007
Lorenzo Gheri, Ivan Lanese, Neil Sayers, Emilio Tuosto, and Nobuko Yoshida. 2022. Design-By-Contract for Flexible Multiparty Session Protocols. In 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany (LIPIcs, Vol. 222), Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 8:1-8:28. https://doi. org/10. 4230/LIPICS. ECOOP. 2022. 8
Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger. 2021. Multiparty Languages: The Choreographic and Multitier Cases (Pearl). In 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference) (LIPIcs, Vol. 194), Anders Møller and Manu Sridharan (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 22:1-22:27. https://doi. org/10. 4230/LIPIcs. ECOOP. 2021. 22
Patrice Godefroid and Mihalis Yannakakis. 2013. Analysis of Boolean Programs. In Tools and Algorithms for the Construction and Analysis of Systems-19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7795), Nir Piterman and Scott A. Smolka (Eds.). Springer, 214-229. https://doi. org/10. 1007/978-3-642-36742-7_16
Hannah Gommerstadt, Limin Jia, and Frank Pfenning. 2018. Session-Typed Concurrent Contracts. In Programming Languages and Systems-27th European Symposium on Programming, ESOP 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. 10801), Amal Ahmed (Ed.). Springer, 771-798. https://doi. org/10. 1007/978-3-319-89884-1_27
Dennis Griffith and Elsa L. Gunter. 2013. LiquidPi: Inferrable Dependent Session Types. In NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7871), Guillaume Brat, Neha Rungta, and Arnaud Venet (Eds.). Springer, 185-197. https://doi. org/10. 1007/ 978-3-642-38088-4_13
Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. 2020. Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4, POPL (2020), 6:1-6:30. https://doi. org/10. 1145/3371074
Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. 2022. Actris 2. 0: Asynchronous Session-Type Based Reasoning in Separation Logic. Log. Methods Comput. Sci. 18, 2 (2022). https://doi. org/10. 46298/LMCS-18(2:16)2022
Jonas Kastberg Hinrichsen, Jules Jacobs, and Robbert Krebbers. 2024. Multris: Functional Verification of Multiparty Message Passing in Separation Logic. (2024). https://jihgfee. github. io/papers/multris_manuscript. pdf
Andrew K. Hirsch and Deepak Garg. 2021. Pirouette: Higher-Order Typed Functional Choreographies. CoRR abs/2111. 03484 (2021). arXiv:2111. 03484 https://arxiv. org/abs/2111. 03484
Andrew K. Hirsch and Deepak Garg. 2022. Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang. 6, POPL (2022), 1-27. https://doi. org/10. 1145/3498684
Kohei Honda, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2012. Verification of MPI Programs Using Session Types. In Recent Advances in the Message Passing Interface-19th European MPI Users' Group Meeting, EuroMPI 2012, Vienna, Austria, September 23-26, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7490), Jesper Larsson Träff, Siegfried Benkner, and Jack J. Dongarra (Eds.). Springer, 291-293. https://doi. org/10. 1007/978-3-642-33518-1_37
Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, George C. Necula and Philip Wadler (Eds.). ACM, 273-284. https://doi. org/10. 1145/1328438. 1328472
Raymond Hu and Nobuko Yoshida. 2016. Hybrid Session Verification Through Endpoint API Generation. In Fundamental Approaches to Software Engineering-19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Computer Science, Vol. 9633), Perdita Stevens and Andrzej Wasowski (Eds.). Springer, 401-418. https://doi. org/10. 1007/978-3-662-49665-7_24
Raymond Hu and Nobuko Yoshida. 2017. Explicit Connection Actions in Multiparty Session Types. In 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), Marieke Huisman and Julia Rubin (Eds.). Springer, 116-133. https://doi. org/10. 1007/978-3-662-54494-5_7
Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. 2020. Multiparty Session Programming With Global Protocol Combinators. In 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference) (LIPIcs, Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 9:1-9:30. https://doi. org/10. 4230/LIPICS. ECOOP. 2020. 9
Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers. 2024. Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. Proc. ACM Program. Lang. 8, POPL (2024), 1385-1417. https://doi. org/10. 1145/3632889
Sung-Shik Jongmans and Petra van den Bos. 2022. A Predicate Transformer for Choreographies-Computing Preconditions in Choreographic Programming. In Programming Languages and Systems-31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings (Lecture Notes in Computer Science, Vol. 13240), Ilya Sergey (Ed.). Springer, 520-547. https://doi. org/10. 1007/978-3-030-99336-8_19
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20. https://doi. org/10. 1017/S0956796818000151
Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2022. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types (Artifact). Dagstuhl Artifacts Ser. 8, 2 (2022), 09:1-09:16. https://doi. org/10. 4230/DARTS. 8. 2. 9
Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (1978), 558-565. https://doi. org/10. 1145/359545. 359563
Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2018. A static verification framework for message passing in Go using behavioural types. In Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27-June 03, 2018, Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman (Eds.). ACM, 1137-1148. https://doi. org/10. 1145/3180155. 3180157
Elaine Li, Felix Stutz, and Thomas Wies. 2024. Deciding Subtyping for Asynchronous Multiparty Sessions. In Programming Languages and Systems-33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 14576), Stephanie Weirich (Ed.). Springer, 176-205. https://doi. org/10. 1007/978-3-031-57262-3_8
Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. 2023. Complete Multiparty Session Type Projection with Automata. In Computer Aided Verification-35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III (Lecture Notes in Computer Science, Vol. 13966), Constantin Enea and Akash Lal (Eds.). Springer, 350-373. https://doi. org/10. 1007/978-3-031-37709-9_17
Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. 2023. Complete Multiparty Session Type Projection with Automata. CoRR abs/2305. 17079 (2023). https://doi. org/10. 48550/ARXIV. 2305. 17079 arXiv:2305. 17079
Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. 2025. Characterizing Implementability of Global Protocols with Infinite States and Data. arXiv:2411. 05722 [cs. PL] https://arxiv. org/abs/2411. 05722
Markus Lohrey. 2003. Realizability of high-level message sequence charts: closing the gaps. Theor. Comput. Sci. 309, 1-3 (2003), 529-554. https://doi. org/10. 1016/J. TCS. 2003. 08. 002
Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. 2021. Generalising Projection in Asynchronous Multiparty Session Types. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference (LIPIcs, Vol. 203), Serge Haddad and Daniele Varacca (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 35:1-35:24. https://doi. org/10. 4230/LIPICS. CONCUR. 2021. 35
Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. 2021. Generalising Projection in Asynchronous Multiparty Session Types. CoRR abs/2107. 03984 (2021). arXiv:2107. 03984 https://arxiv. org/abs/2107. 03984
Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, and Damien Zufferey. 2019. Motion Session Types for Robotic Interactions (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming, ECOOP 2019, July 15-19, 2019, London, United Kingdom (LIPIcs, Vol. 134), Alastair F. Donaldson (Ed.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 28:1-28:27. https://doi. org/10. 4230/LIPIcs. ECOOP. 2019. 28
Rupak Majumdar, Nobuko Yoshida, and Damien Zufferey. 2020. Multiparty motion coordination: from choreographies to robotics programs. Proc. ACM Program. Lang. 4, OOPSLA (2020), 134:1-134:30. https://doi. org/10. 1145/3428202
Sjouke Mauw and Michel A. Reniers. 1997. High-level message sequence charts. In SDL '97 Time for Testing, SDL, MSC and Trends-8th International SDL Forum, Evry, France, 23-29 September 1997, Proceedings, Ana R. Cavalli and Amardeo Sarma (Eds.). Elsevier, 291-306.
Fabrizio Montesi. 2023. Introduction to Choreographies. Cambridge University Press. https://doi. org/10. 1017/ 9781108981491
Rémi Morin. 2002. Recognizable Sets of Message Sequence Charts. In STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes-Juan les Pins, France, March 14-16, 2002, Proceedings (Lecture Notes in Computer Science, Vol. 2285), Helmut Alt and Afonso Ferreira (Eds.). Springer, 523-534. https://doi. org/10. 1007/3-540-45841-7_43
Madhavan Mukund. 2002. From Global Specifications to Distributed Implementations. Springer US, Boston, MA, 19-35. https://doi. org/10. 1007/978-1-4757-6656-1_2
Anca Muscholl and Doron A. Peled. 1999. Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces. In Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS'99, Szklarska Poreba, Poland, September 6-10, 1999, Proceedings (Lecture Notes in Computer Science, Vol. 1672), Miroslaw Kutylowski, Leszek Pacholski, and Tomasz Wierzbicki (Eds.). Springer, 81-91. https://doi. org/10. 1007/3-540-48340-3_8
Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. 2017. Timed runtime monitoring for multiparty conversations. Formal Aspects Comput. 29, 5 (2017), 877-910. https://doi. org/10. 1007/S00165-017-0420-8
Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. 2018. A session type provider: compile-time API generation of distributed protocols with refinements in F#. In Proceedings of the 27th International Conference on Compiler Construction, CC 2018, February 24-25, 2018, Vienna, Austria, Christophe Dubach and Jingling Xue (Eds.). ACM, 128-138. https://doi. org/10. 1145/3178372. 3179495
Rumyana Neykova and Nobuko Yoshida. 2017. Multiparty Session Actors. Log. Methods Comput. Sci. 13, 1 (2017). https://doi. org/10. 23638/LMCS-13(1:17)2017
Nicholas Ng, Nobuko Yoshida, and Kohei Honda. 2012. Multiparty Session C: Safe Parallel Programming with Message Optimisation. In Objects, Models, Components, Patterns-50th International Conference, TOOLS 2012, Prague, Czech Republic, May 29-31, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7304), Carlo A. Furia and Sebastian Nanz (Eds.). Springer, 202-218. https://doi. org/10. 1007/978-3-642-30561-0_15
Xinyu Niu, Nicholas Ng, Tomofumi Yuki, ShaojunWang, Nobuko Yoshida, andWayne Luk. 2016. EURECA compilation: Automatic optimisation of cycle-reconfigurable circuits. In 26th International Conference on Field Programmable Logic and Applications, FPL 2016, Lausanne, Switzerland, August 29-September 2, 2016, Paolo Ienne, Walid A. Najjar, Jason Helge Anderson, Philip Brisk, and Walter Stechele (Eds.). IEEE, 1-4. https://doi. org/10. 1109/FPL. 2016. 7577359
Abhik Roychoudhury, Ankit Goel, and Bikram Sengupta. 2012. Symbolic Message Sequence Charts. ACM Trans. Softw. Eng. Methodol. 21, 2 (2012), 12:1-12:44. https://doi. org/10. 1145/2089116. 2089122
Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. 2017. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain (LIPIcs, Vol. 74), Peter Müller (Ed.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 24:1-24:31. https://doi. org/10. 4230/LIPICS. ECOOP. 2017. 24
Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3, POPL (2019), 30:1-30:29. https://doi. org/10. 1145/3290343
Gan Shen, Shun Kashiwa, and Lindsey Kuper. 2023. HasChor: Functional Choreographic Programming for All (Functional Pearl). CoRR abs/2303. 00924 (2023). https://doi. org/10. 48550/ARXIV. 2303. 00924 arXiv:2303. 00924
Felix Stutz. 2023. Asynchronous Multiparty Session Type Implementability is Decidable-Lessons Learned from Message Sequence Charts. In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States (LIPIcs, Vol. 263), Karim Ali and Guido Salvaneschi (Eds.). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 32:1-32:31. https://doi. org/10. 4230/LIPICS. ECOOP. 2023. 32
Felix Stutz. 2024. Implementability of Asynchronous Communication Protocols-The Power of Choice. Ph. D. Dissertation. Kaiserslautern University of Technology, Germany. https://kluedo. ub. rptu. de/frontdoor/index/index/docId/8077
Peter Thiemann and Vasco T. Vasconcelos. 2020. Label-dependent session types. Proc. ACM Program. Lang. 4, POPL (2020), 67:1-67:29. https://doi. org/10. 1145/3371135
Bernardo Toninho and Nobuko Yoshida. 2017. Certifying data in multiparty session types. J. Log. Algebraic Methods Program. 90 (2017), 61-83. https://doi. org/10. 1016/J. JLAMP. 2016. 11. 005
International Telecommunication Union. 1996. Z. 120: Message Sequence Chart. Technical Report. International Telecommunication Union. https://www. itu. int/rec/T-REC-Z. 120
Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. 2023. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. Proc. ACM Program. Lang. 7, POPL (2023), 2111-2140. https://doi. org/10. 1145/3571265
Margus Veanes and Nikolaj S. Bjørner. 2012. Symbolic Automata: The Toolkit. In Tools and Algorithms for the Construction and Analysis of Systems-18th International Conference, TACAS 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. 7214), Cormac Flanagan and Barbara König (Eds.). Springer, 472-477. https: //doi. org/10. 1007/978-3-642-28756-5_33
Margus Veanes, Peli de Halleux, and Nikolai Tillmann. 2010. Rex: Symbolic Regular Expression Explorer. In Third International Conference on Software Testing, Verification and Validation, ICST 2010, Paris, France, April 7-9, 2010. IEEE Computer Society, 498-507. https://doi. org/10. 1109/ICST. 2010. 15
Nobuko Yoshida. 2024. Programming Language Implementations with Multiparty Session Types. In Active Object Languages: Current Research Trends, Frank S. de Boer, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, and Eduard Kamburjan (Eds.). Lecture Notes in Computer Science, Vol. 14360. Springer, 147-165. https://doi. org/10. 1007/978-3-031-51060-1_6
Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. 2013. The Scribble Protocol Language. In 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), Martín Abadi and Alberto Lluch-Lafuente (Eds.). Springer, 22-41. https://doi. org/10. 1007/978-3-319-05119-2_3
Fangyi Zhou. 2024. Refining Multiparty Session Types. Ph. D. Dissertation. Imperial College London.
Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. 2020. Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang. 4, OOPSLA (2020), 148:1-148:30. https://doi. org/10. 1145/3428216
Wieslaw Zielonka. 1987. Notes on Finite Asynchronous Automata. RAIRO Theor. Informatics Appl. 21, 2 (1987), 99-135. https://doi. org/10. 1051/ITA/1987210200991