{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:12:26Z","timestamp":1784211146892,"version":"3.55.0"},"reference-count":83,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"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 multithreaded 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                  <\/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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9371-0807","authenticated-orcid":false,"given":"Pascal","family":"Baumann","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/321479.321488"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"C. Aiswarya Pascal Baumann Prakash Saivasan Lia Sch\u00fctze and Georg Zetzsche. 2025. Bounded treewidth multiple context-free grammars and downward closures. CoRR abs\/2512.01973 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2512.01973 10.48550\/ARXIV.2512.01973","DOI":"10.48550\/ARXIV.2512.01973"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_1"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2016.27"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(2:8)2018"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2017.39"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/11779148_1"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2023.39"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_13"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(4:4)2011"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_29"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2020.109"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2023.3"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571266"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2020.111"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498678"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-663-09367-1"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054196000191"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_5"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_4"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3210257"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ESA.2016.28"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676979"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349311"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934527"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704854"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-025-00787-0"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02088013"},{"key":"e_1_3_2_31_2","first-page":"178","article-title":"On Constructing Obstruction Sets of Words","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":"Bull. EATCS"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2010.13"},{"key":"e_1_3_2_33_2","volume-title":"Verification of communicating recursive programs via split-width. (V\u00e9rification de programmes r\u00e9cursifs et communicants via split-width)","author":"Cyriac Aiswarya","year":"2014","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_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_38"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_12"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1051\/ITA\/1977110402731"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(91)90018-Z"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90058-6"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(76)90086-7"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2022.124"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-24950-1_9"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_39"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSTTCS.2011.457"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48199-0_12"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Graham Higman. 1952. Ordering by Divisibility in Abstract Algebras. Proceedings of The London Mathematical Society (1952) 326\u2013336. https:\/\/doi.org\/10.1112\/plms\/s3-2.1.326 10.1112\/plms\/s3-2.1.326","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771803"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3478536"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.STACS.2021.44"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511597855.007"},{"issue":"4","key":"e_1_3_2_51_2","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_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1111\/J.1467-8640.1994.TB00008.X"},{"issue":"1","key":"e_1_3_2_53_2","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_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13089-2_29"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498673"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632884"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.9"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2015.72"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_32"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2020.104588"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0022257"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498724"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434340"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571228"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926419"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(4:2)2022"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48199-0_14"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(80)90867-0"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/3583660.3583664"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1969-0246760-1"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90374-B"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1997.2697"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.3115\/981175.981190"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.3115\/981967.981985"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_35"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2016.123"},{"key":"e_1_3_2_84_2","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,7,16]],"date-time":"2026-07-16T13:43:22Z","timestamp":1784209402000},"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"}}]}}