{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,3]],"date-time":"2026-08-03T01:57:14Z","timestamp":1785722234861,"version":"3.56.0"},"reference-count":90,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2304758"],"award-info":[{"award-number":["2304758"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Luxembourg National Research Fund","award":["C22\/IS\/17238244\/AVVA"],"award-info":[{"award-number":["C22\/IS\/17238244\/AVVA"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nOur symbolic protocols describe infinite states and data values using dependent refinement predicates. \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nImplementability 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. \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nWe provide a unified explanation of seemingly disparate sources of non-implementability through a precise semantic characterization of implementability for infinite protocols. \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nOur characterization reduces the problem of implementability to (co)reachability in the global protocol restricted to each participant. \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nThis compositional reduction yields the first sound and relatively complete algorithm for checking implementability of symbolic protocols. \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nWe use our characterization to show that for finite protocols, implementability is co-NP-complete for explicit representations and PSPACE-complete for symbolic representations. \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \nThe 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.<\/jats:p>","DOI":"10.1145\/3720493","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1434-1463","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Characterizing Implementability of Global Protocols with Infinite States and Data"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0173-4498","authenticated-orcid":false,"given":"Elaine","family":"Li","sequence":"first","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3638-4096","authenticated-orcid":false,"given":"Felix","family":"Stutz","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Esch-sur-Alzette, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3197-8736","authenticated-orcid":false,"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[{"name":"NVIDIA, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1214326"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.09.034"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_10"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2018.03.004"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-014-0220-1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41157-1_7"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.356.2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-242188"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290342"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.6"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:9)2022"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-18941-3_4"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.07.005"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508404"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78142-2_3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2010.14"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2020.13"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(1:9)2022"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.6"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-014-0218-8"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Volker Diekert and Grzegorz Rozenberg (Eds.). 1995. The Book of Traces. World Scientific. isbn:978-981-02-2058-7 https:\/\/doi.org\/10.1142\/2563 10.1142\/2563","DOI":"10.1142\/2563"},{"key":"e_1_2_1_27_1","first-page":"143","article-title":"Decidability Issues for Petri Nets - a survey","volume":"30","author":"Esparza Javier","year":"1994","unstructured":"Javier Esparza and Mogens Nielsen. 1994. Decidability Issues for Petri Nets - a survey. J. Inf. Process. Cybern., 30, 3 (1994), 143\u2013160.","journal-title":"J. Inf. Process. Cybern."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(4:33)2023"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_12"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2005.25"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27755-2_15"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.007"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2022.8"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.22"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_16"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_27"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_13"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:16)2022"},{"key":"e_1_2_1_41_1","volume-title":"Multris: Functional Verification of Multiparty Message Passing in Separation Logic. https:\/\/jihgfee.github.io\/papers\/multris_manuscript.pdf","author":"Hinrichsen Jonas Kastberg","year":"2024","unstructured":"Jonas Kastberg Hinrichsen, Jules Jacobs, and Robbert Krebbers. 2024. Multris: Functional Verification of Multiparty Message Passing in Separation Logic. https:\/\/jihgfee.github.io\/papers\/multris_manuscript.pdf"},{"key":"e_1_2_1_42_1","volume-title":"Hirsch and Deepak Garg","author":"Andrew","year":"2021","unstructured":"Andrew K. Hirsch and Deepak Garg. 2021. Pirouette: Higher-Order Typed Functional Choreographies. CoRR, abs\/2111.03484 (2021), arXiv:2111.03484. arxiv:2111.03484"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498684"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33518-1_37"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_7"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2020.9"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.4230\/DARTS.8.2.9"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180157"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_8"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_17"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2305.17079"},{"key":"e_1_2_1_58_1","unstructured":"Elaine Li Felix Stutz Thomas Wies and Damien Zufferey. 2025. Characterizing Implementability of Global Protocols with Infinite States and Data. arxiv:2411.05722. arxiv:2411.05722"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2003.08.002"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2021.35"},{"key":"e_1_2_1_61_1","volume-title":"Generalising Projection in Asynchronous Multiparty Session Types. CoRR, abs\/2107.03984","author":"Majumdar Rupak","year":"2021","unstructured":"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. arxiv:2107.03984"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.28"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428202"},{"key":"e_1_2_1_64_1","volume-title":"8th International SDL Forum","author":"Mauw Sjouke","year":"1997","unstructured":"Sjouke Mauw and Michel A. Reniers. 1997. High-level message sequence charts. In SDL \u201997 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\u2013306."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108981491"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45841-7_43"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6656-1_2"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48340-3_8"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-017-0420-8"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179495"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:17)2017"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_15"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2016.7577359"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/2089116.2089122"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2017.24"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2303.00924"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.32"},{"key":"e_1_2_1_79_1","volume-title":"Implementability of Asynchronous Communication Protocols - The Power of Choice. Ph. D. Dissertation","author":"Stutz Felix","unstructured":"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"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371135"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2016.11.005"},{"key":"e_1_2_1_82_1","volume-title":"Message Sequence Chart","author":"Union International Telecommunication","unstructured":"International Telecommunication Union. 1996. Z.120: Message Sequence Chart. International Telecommunication Union. https:\/\/www.itu.int\/rec\/T-REC-Z.120"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_33"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.15"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51060-1_6"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05119-2_3"},{"key":"e_1_2_1_88_1","volume-title":"Refining Multiparty Session Types. Ph. D. Dissertation","author":"Zhou Fangyi","unstructured":"Fangyi Zhou. 2024. Refining Multiparty Session Types. Ph. D. Dissertation. Imperial College London."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428216"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1051\/ITA\/1987210200991"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720493","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720493","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:06:19Z","timestamp":1760029579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720493"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":90,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720493"],"URL":"https:\/\/doi.org\/10.1145\/3720493","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}