{"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":1784211146990,"version":"3.55.0"},"reference-count":28,"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"}],"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>\n                    We extend the scope of context-free-language (CFL) reachability to a new class of infinite-state systems. Parikh's Theorem is a useful tool for solving CFL-reachability problems for transition systems that consist of\n                    <jats:italic toggle=\"yes\">commuting<\/jats:italic>\n                    transition relations. It implies that the image of a context-free language under a homomorphism into a commutative monoid is semi-linear, and that there is a linear-time algorithm for constructing a Presburger arithmetic formula that represents it. However, for many transition systems of interest, transitions do not commute.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we introduce\n                    <jats:italic toggle=\"yes\">almost-commuting transition systems<\/jats:italic>\n                    , which pair finite-state control with commutative components, but which are in general not commutative. We extend Parikh's theorem to show that the image of a context-free language under a homomorphism into an\n                    <jats:italic toggle=\"yes\">almost-commuting monoid<\/jats:italic>\n                    is semi-linear and that there is a polynomial-time algorithm for constructing a Presburger arithmetic formula that represents it. This result yields a general framework for solving CFL-reachability problems over\n                    <jats:italic toggle=\"yes\">almost commuting transition systems<\/jats:italic>\n                    . We describe several examples of systems within this class. Finally, we examine closure properties of almost-commuting monoids that can be used to modularly compose almost-commuting transition systems while remaining in the class.\n                  <\/jats:p>","DOI":"10.1145\/3776686","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1270-1295","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Context-Free-Language Reachability for Almost-Commuting Transition Systems"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-5405-9129","authenticated-orcid":false,"given":"Nikhil","family":"Pimpalkhare","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7294-9165","authenticated-orcid":false,"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-66335-7_1","volume-title":"Quantitative Evaluation of Systems","author":"Bhattiprolu Vijay","year":"2017","unstructured":"Vijay Bhattiprolu, Spencer Gordon, and Mahesh Viswanathan. 2017. Extending Parikh's Theorem to Weighted and Probabilistic Context-Free Grammars. In Quantitative Evaluation of Systems, Nathalie Bertrand and Luca Bortolussi (Eds.). Springer International Publishing, Cham, 3\u201319."},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:1)2021"},{"key":"e_1_3_2_4_1","volume-title":"Symbolic Methods for Exploring Infinite State Spaces. Ph. D. Dissertation","author":"Boigelot Bernard","year":"1998","unstructured":"Bernard Boigelot. 1998. Symbolic Methods for Exploring Infinite State Spaces. Ph. D. Dissertation. University of Li\u00e8ge, Belgium. https:\/\/orbi.uliege.be\/handle\/2268\/74874"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604137"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(59)90362-6"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Bart De Schutter and Ton van den Boom. 2008. Max-plus algebra and max-plus linear discrete event systems: An introduction. In 2008 9th International Workshop on Discrete Event Systems. 36\u201342. doi:10.1109\/WODES.2008.4605919","DOI":"10.1109\/WODES.2008.4605919"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_20"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1857914.1857917"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36206-1_14"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2018.32"},{"issue":"2","key":"e_1_3_2_14_1","first-page":"285","article-title":"Semigroups, Presburger Formulas, and Languages","volume":"7","author":"Ginsburg Seymour","year":"1966","unstructured":"Seymour Ginsburg and Edwin H. Spanier. 1966. Semigroups, Presburger Formulas, and Languages. Pacific 7. Math. 16, 2 (1966), 285\u2013296.","journal-title":"Pacific"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01692511"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37051-9_4"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689777"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-72621-7_11"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_7"},{"key":"e_1_3_2_22_1","unstructured":"Moj\u017cesz Presburger. 1929. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I Congr\u00e8s de Math\u00e9maticiens des Pays Slaves."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360208"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2005.02.009"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Yu Su Ding Ye and Jingling Xue. 2014. Parallel Pointer Analysis with CFL-Reachability. In 2014 43rd International Conference on Parallel Processing. 451\u2013460. doi:10.1109\/ICPP.2014.54","DOI":"10.1109\/ICPP.2014.54"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776686","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:42:41Z","timestamp":1784209361000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776686"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":28,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776686"],"URL":"https:\/\/doi.org\/10.1145\/3776686","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"}}]}}