{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:35:20Z","timestamp":1767918920584,"version":"3.49.0"},"reference-count":83,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"name":"ERC","award":["101077902"],"award-info":[{"award-number":["101077902"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>The reachability problem in multi-pushdown automata (MPDA), or equivalently, interleaved Dyck reachability, has many applications in static analysis of recursive programs. An example is safety verification of multi-threaded recursive programs with shared memory. Since these problems are undecidable, the literature contains many decidable (and efficient) underapproximations of MPDA.<\/jats:p>\n                  <jats:p>\n                    A uniform framework that captures many of these underapproximations is that of\n                    <jats:italic toggle=\"yes\">bounded treewidth<\/jats:italic>\n                    : To each execution of the MPDA, we associate a graph; then we consider the subset of all graphs that have a treewidth at most\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    , for some constant\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    . In fact, bounding treewidth is a generic approach to obtain classes of systems with decidable reachability, even beyond MPDA underapproximations. The resulting systems are also called\n                    <jats:italic toggle=\"yes\">MSO-definable bounded-treewidth systems<\/jats:italic>\n                    .\n                  <\/jats:p>\n                  <jats:p>\n                    While bounded treewidth is a powerful tool for reachability and similar types of analysis, the word languages (i.e. action sequences corresponding to executions) of these systems remain far from understood. For the slight restriction of bounded\n                    <jats:italic toggle=\"yes\">special treewidth<\/jats:italic>\n                    , or \u201cbounded-stw\u201d (which is equivalent to bounded treewidth on MPDA, and even includes all bounded-treewidth systems studied in the literature), this work reveals a connection with multiple context-free languages (MCFL), a concept from computational linguistics. We show that the word languages of MSO-definable bounded-stw systems are exactly the MCFL.\n                  <\/jats:p>\n                  <jats:p>\n                    We exploit this connection to provide an optimal algorithm for computing\n                    <jats:italic toggle=\"yes\">downward closures<\/jats:italic>\n                    for MSO-definable bounded-stw systems. Computing downward closures is a notoriously difficult task that has many applications in the verification of complex systems: As an example application, we show that in programs with dynamic spawning of MSO-definable bounded-stw processes, safety verification has the same complexity as in the case of processes with sequential recursive processes.\n                  <\/jats:p>","DOI":"10.1145\/3776716","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2142-2173","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4878-7581","authenticated-orcid":false,"given":"C.","family":"Aiswarya","sequence":"first","affiliation":[{"name":"Chennai Mathematical Institute, Chennai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9371-0807","authenticated-orcid":false,"given":"Pascal","family":"Baumann","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5060-0117","authenticated-orcid":false,"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[{"name":"Institute of Mathematical Sciences, Chennai, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4002-5491","authenticated-orcid":false,"given":"Lia","family":"Sch\u00fctze","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/321479.321488"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2512.01973"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2016.27"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(2:8)2018"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2017.39"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11779148_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2023.39"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_13"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(4:4)2011"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_29"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2020.109"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2023.3"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571266"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2020.111"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498678"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-663-09367-1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054196000191"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_5"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_4"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3210257"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ESA.2016.28"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676979"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349311"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934527"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704854"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-025-00787-0"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02088013"},{"key":"e_1_2_1_30_1","first-page":"178","article-title":"On Constructing Obstruction Sets of","volume":"44","author":"Courcelle Bruno","year":"1991","unstructured":"Bruno Courcelle. 1991. On Constructing Obstruction Sets of Words. Bull. EATCS, 44 (1991), 178\u2013186.","journal-title":"Words. Bull. EATCS"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2010.13"},{"key":"e_1_2_1_32_1","unstructured":"Aiswarya Cyriac. 2014. Verification of communicating recursive programs via split-width. (V\u00e9rification de programmes r\u00e9cursifs et communicants via split-width). Ph.D. Dissertation. \u00c9cole normale sup\u00e9rieure de Cachan France. https:\/\/tel.archives-ouvertes.fr\/tel-01015561"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_38"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_12"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1051\/ITA\/1977110402731"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(91)90018-Z"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90058-6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(76)90086-7"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2022.124"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-24950-1_9"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_39"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSTTCS.2011.457"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48199-0_12"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771803"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3478536"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.STACS.2021.44"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511597855.007"},{"key":"e_1_2_1_50_1","first-page":"499","article-title":"The universal recognition problems for parallel multiple context-free grammars and for their subclasses","volume":"75","author":"Kaji Yuichi","year":"1992","unstructured":"Yuichi Kaji, Ryuichi Nakanishi, Hiroyuki Seki, and Tadao Kasami. 1992. The universal recognition problems for parallel multiple context-free grammars and for their subclasses. IEICE TRANSACTIONS on Information and Systems, 75, 4 (1992), 499\u2013508.","journal-title":"IEICE TRANSACTIONS on Information and Systems"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1111\/J.1467-8640.1994.TB00008.X"},{"key":"e_1_2_1_52_1","first-page":"78","article-title":"The universal recognition problems for multiple context-free grammars and for linear context-free rewriting systems","volume":"75","author":"Kaji Yuichi","year":"1992","unstructured":"Yuichi Kaji, Ryuichi Nakanisi, Hiroyuki Seki, and Tadao Kasami. 1992. The universal recognition problems for multiple context-free grammars and for linear context-free rewriting systems. IEICE Transactions on Information and Systems, 75, 1 (1992), 78\u201388.","journal-title":"IEICE Transactions on Information and Systems"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13089-2_29"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498673"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632884"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.9"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2015.72"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_32"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2020.104588"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0022257"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498724"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434340"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571228"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926419"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(4:2)2022"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48199-0_14"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(80)90867-0"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3583660.3583664"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1969-0246760-1"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90374-B"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1997.2697"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.3115\/981175.981190"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.3115\/981967.981985"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_35"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2016.123"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009848"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776716","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:03:44Z","timestamp":1767899024000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776716"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":83,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776716"],"URL":"https:\/\/doi.org\/10.1145\/3776716","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}