{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T20:31:20Z","timestamp":1792787480414,"version":"4.5.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\/legalcode"}],"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. 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.<\/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":5,"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_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1214326"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.09.034"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_10"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/JJLAMP.2018.03.004"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-014-0220-1"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41157-1_7"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"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\u201323. https:\/\/doi.org\/10.4204\/EPTCS.356.2 10.4204\/EPTCS.356.2","DOI":"10.4204\/EPTCS.356.2"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-242188"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290342"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.6"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:9)2022"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-18941-3_4"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.07.005"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508404"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78142-2_3"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2010.14"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_1"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2020.13"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(1:9)2022"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.6"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-014-0218-8"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1142\/2563"},{"issue":"3","key":"e_1_3_1_28_2","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_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(4:33)2023"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_12"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2005.25"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27755-2_15"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.007"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2022.8"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.22"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_16"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_27"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_13"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:16)2022"},{"key":"e_1_3_1_42_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1145\/3689762"},{"key":"e_1_3_1_43_2","unstructured":"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"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498684"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33518-1_37"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_7"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.EC00P.2020.9"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.4230\/DARTS.8.2.9"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180157"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_8"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_17"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","unstructured":"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 10.48550\/ARXIV.2305.17079 arXiv:2305.17079","DOI":"10.48550\/ARXIV.2305.17079"},{"key":"e_1_3_1_59_2","unstructured":"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"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2003.08.002"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2021.35"},{"key":"e_1_3_1_62_2","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 https:\/\/arxiv.org\/abs\/2107.03984"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.28"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428202"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482816-3\/50020-4"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108981491"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45841-7_43"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-6656-1_2"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48340-3_8"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-017-0420-8"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179495"},{"key":"e_1_3_1_72_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:17)2017"},{"key":"e_1_3_1_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_15"},{"key":"e_1_3_1_74_2","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2016.7577359"},{"key":"e_1_3_1_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/2089116.2089122"},{"key":"e_1_3_1_76_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2017.24"},{"key":"e_1_3_1_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_3_1_78_2","doi-asserted-by":"publisher","unstructured":"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 10.48550\/ARXIV.2303.00924 arXiv:2303.00924","DOI":"10.48550\/ARXIV.2303.00924"},{"key":"e_1_3_1_79_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.32"},{"key":"e_1_3_1_80_2","volume-title":"Implementability of Asynchronous Communication Protocols - The Power of Choice","author":"Stutz Felix","year":"2024","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_3_1_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371135"},{"key":"e_1_3_1_82_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2016.11.005"},{"key":"e_1_3_1_83_2","volume-title":"Z.120: Message Sequence Chart. Technical Report","author":"International Telecommunication Union","year":"1996","unstructured":"International Telecommunication Union. 1996. Z.120: Message Sequence Chart. Technical Report. International Telecommunication Union. https:\/\/www.itu.int\/rec\/T-REC-Z.120"},{"key":"e_1_3_1_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_3_1_85_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_33"},{"key":"e_1_3_1_86_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.15"},{"key":"e_1_3_1_87_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51060-1_6"},{"key":"e_1_3_1_88_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05119-2_3"},{"key":"e_1_3_1_89_2","volume-title":"Refining Multiparty Session Types","author":"Zhou Fangyi","year":"2024","unstructured":"Fangyi Zhou. 2024. Refining Multiparty Session Types. Ph.D. Dissertation. Imperial College London."},{"key":"e_1_3_1_90_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428216"},{"key":"e_1_3_1_91_2","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":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720493","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:28:18Z","timestamp":1787588898000},"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"}}]}}