{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:58Z","timestamp":1780994698407,"version":"3.54.1"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Multiparty session types (MPST) provide a type discipline for ensuring communication safety, deadlockfreedom and liveness for multiple concurrently running participants. The original formulation of MPST takes the top-down approach, where a global type specifies a bird\u2019s eye view of the intended interactions between participants, and each distributed process is locally type-checked against its end-point projection. A more recent one takes the bottom-up approach, where a desired property \ud835\udf11 of a set of participants is ensured if the same property \ud835\udf11 is true for an ensemble of end-point types (a typing context) inferred from each participant.<\/jats:p>\n                  <jats:p>This paper compares these two main procedures of MPST, giving their detailed complexity analyses. To this aim, we build several new algorithms missing from the bottom-up or top-down workflows by using graph representation of session types (type graphs). We first propose a subtyping system based on type graphs, offering more efficient (quadratic) subtype-checking than the existing (exponential) inductive algorithm by Ghilezan et al. Next for the top-down, we measure complexity of the four end-point projections in the literature. For the coinductive projection with full merging, we build a new sound and complete PSPACE-algorithm using type graphs. For bottom-up, we develop a novel type inference system from MPST processes which generates minimum type graphs, succinctly capturing covariance of internal choice and contravariance of external choice. For property-checking of typing contexts, we achieve PSPACE-hardness by reducing it from the quantified Boolean formula (QBF) problem, and build nondeterministic algorithms that search for counterexamples to prove membership in PSPACE. We also present deterministic analogues of these algorithms that run in exponential time. Finally, we calculate the total complexity of the top-down and the bottom-up approaches. Our analyses reveal that the top-down based on global types is more efficient than the bottom-up in many realistic cases; liveness checking for typing contexts in the bottom-up has the highest complexity; and the type inference costs exponential against the size of a process, which impacts the total complexity.<\/jats:p>","DOI":"10.1145\/3704872","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1040-1071","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2320-9178","authenticated-orcid":false,"given":"Thien","family":"Udomsrirungruang","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3925-8557","authenticated-orcid":false,"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_6"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(3:9)2023"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2022.35"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.1"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57246-3_12"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"issue":"1","key":"e_1_3_2_10_2","article-title":"A Sound Algorithm for Asynchronous Session Subtyping and its Implementation","volume":"17","author":"Bravetti Mario","year":"2021","unstructured":"Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. 2021. A Sound Algorithm for Asynchronous Session Subtyping and its Implementation. Log. Methods Comput. Sci. 17, 1 (2021). https:\/\/lmcs.episciences.org\/7238","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_2"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2022.100844"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454041"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377555.3377889"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(2:12)2017"},{"issue":"2","key":"e_1_3_2_16_2","first-page":"238","article-title":"Global Progress for Dynamically Interleaved Multiparty Sessions","volume":"26","author":"Coppo Mario","year":"2015","unstructured":"Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. 2015. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 26 (2015), 238\u2013302. Issue 2.","journal-title":"MSCS"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508404"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23217-6_19"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_6"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_2_21_2","volume-title":"Behavioural Types: from Theory to Tools","author":"Gay Simon","year":"2017","unstructured":"Simon Gay and Ant\u00f3nio Ravara (Eds.). 2017. Behavioural Types: from Theory to Tools. River Publisher."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781009000062"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_5"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.12.002"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.12.002"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547638"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_10"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.15"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_52"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_26"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_8"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_17"},{"key":"e_1_3_2_35_2","unstructured":"Elaine Li Felix Stutz Thomas Wies and Damien Zufferey. 2024. Complete Multiparty Session Type Projection with Automata. arXiv:2305.17079 [cs]"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.35"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108981491"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3229062"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662085"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Gil Silva Andreia Mordido and Vasco T. Vasconcelos. 2023. Subtyping Context-Free Session Types Vol. 279. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 11:1\u201311:19. https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.11 10.4230\/LIPICS.CONCUR.2023.11","DOI":"10.4230\/LIPICS.CONCUR.2023.11"},{"key":"e_1_3_2_43_2","volume-title":"Introduction to the Theory of Computation","author":"Sipser Michael","year":"2012","unstructured":"Michael Sipser . 2012\/2013. Introduction to the Theory of Computation (third edition. ed.). Cengage Learning, Australia."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.32"},{"key":"e_1_3_2_45_2","unstructured":"Felix Stutz . 2024. Implementability of Asynchronous Communication Protocols - The Power of Choice. Ph.D. Dissertation. University of Kaiserslautern-Landau."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2023.28"},{"key":"e_1_3_2_47_2","unstructured":"Thien Udomsrirungruang and Nobuko Yoshida. 2024. Full version of this paper Top-Down or Bottom-Up? Complexity Analyses ofSynchronous Multiparty Session Types. arXiv:2411.07452 [cs.PL] https:\/\/arxiv.org\/abs\/2411.07452"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2404.05480"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_36"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51060-1_6"},{"key":"e_1_3_2_51_2","doi-asserted-by":"crossref","unstructured":"Nobuko Yoshida and Ping Hou. 2024. Less is More Revisited. arXiv:2402.16741 [cs.PL] Accepted by Cliff B. Jones Festschrift Proceeding.","DOI":"10.1007\/978-3-031-66673-5_14"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704872","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704872","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:09Z","timestamp":1770200289000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704872"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704872"],"URL":"https:\/\/doi.org\/10.1145\/3704872","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}