{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:14:20Z","timestamp":1784211260689,"version":"3.55.0"},"reference-count":60,"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":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101077902"],"award-info":[{"award-number":["101077902"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"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                    Counters that hold natural numbers are ubiquitous in modeling and verifying software systems; for example, they model dynamic creation and use of resources in concurrent programs. Unfortunately, such discrete counters often lead to extremely high complexity. Continuous counters are an efficient over-approximation of discrete counters. They are obtained by relaxing the original counters to hold values over the non-negative\n                    <jats:italic toggle=\"yes\">rational<\/jats:italic>\n                    numbers.\n                  <\/jats:p>\n                  <jats:p>This work shows that continuous counters are extraordinarily well-behaved in terms of decidability. Our main result is that, despite continuous counters being infinite-state, the language of sequences of counter instructions that can arrive in a given target configuration, is regular. Moreover, a finite automaton for this language can be computed effectively. This implies that a wide variety of transition systems can be equipped with continuous counters, while maintaining decidability of reachability properties. Examples include higherorder recursion schemes, well-structured transition systems, and decidable extensions of discrete counter systems.<\/jats:p>\n                  <jats:p>We also prove a non-elementary lower bound for the size of the resulting finite automaton.<\/jats:p>","DOI":"10.1145\/3776661","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"540-567","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["General Decidability Results for Systems with Continuous Counters"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7258-5445","authenticated-orcid":false,"given":"A. R.","family":"Balasubramanian","sequence":"first","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4913-3800","authenticated-orcid":false,"given":"Matthew","family":"Hague","sequence":"additional","affiliation":[{"name":"Royal Holloway, University of London, Egham, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9926-0931","authenticated-orcid":false,"given":"Ramanathan S.","family":"Thinniyam","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2843"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67087-0_1"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.4171\/AUTOMATA-1\/17"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30080-9_1"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662124"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_3"},{"key":"e_1_3_1_10_2","unstructured":"A. R. Balasubramanian Matthew Hague Rupak Majumdar Ramanathan S. Thinniyam and Georg Zetzsche. 2025. General Decidability Results for Systems with Continuous Counters. arXiv:2511.21559 [cs.FL]https:\/\/arxiv.org\/abs\/2511.21559"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3633279"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2020.111"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005068"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2018.119"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80016-X"},{"key":"e_1_3_1_19_2","unstructured":"Ren\u00e9 David and Hassane Alla. 1987. Continuous Petri nets. In Proc. 8th European Workshop on Appli. & Theory of Petri nets 1987."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10669-9"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.4171\/AUTOMATA-1\/1"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782630"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2015.470"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2015-1168"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-007-0050-3"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.4171\/AUTOMATA-1\/13"},{"key":"e_1_3_1_31_2","unstructured":"Roland Guttenberg Eren Keskin and Roland Meyer. 2025. PVASS reachability is decidable. arXiv:2504.05015 [cs.LO]https:\/\/arxiv.org\/abs\/2504.05015"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-032-01436-8_6"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_39"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_60"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3091122"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68894-5_7"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2018-1674"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-877-7"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90006-4"},{"key":"e_1_3_1_40_2","unstructured":"Addie Jordon Juri Kol\u010d\u00e1k and Daniel Merkle. 2025. Continuous Petri Nets for Fast Yield Computation: Polynomial-Time and MILP Approaches. arXiv:2509.02371 [cs.DM]https:\/\/arxiv.org\/abs\/2509.02371"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662116"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2018.09.035"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84996-474-6"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90173-D"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926421"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.16"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785796"},{"key":"e_1_3_1_50_2","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1109\/WODES.2006.382530","volume-title":"2006 8th International Workshop on Discrete Event Systems","author":"Mahulea Cristian","year":"2006","unstructured":"Cristian Mahulea, Laura Recalde, and Manuel Silva. 2006. On performance monotonicity and basic servers semantics of continuous Petri nets. In 2006 8th International Workshop on Discrete Event Systems. IEEE, 345\u2013351."},{"key":"e_1_3_1_51_2","first-page":"1170","article-title":"The Hierarchy of Indexed Languages of an Arbitrary Level","volume":"15","author":"Maslov A. N.","year":"1974","unstructured":"A. N. Maslov. 1974. The Hierarchy of Indexed Languages of an Arbitrary Level. Soviet Mathematics Doklady 15 (1974), 1170\u20131174.","journal-title":"Soviet Mathematics Doklady"},{"key":"e_1_3_1_52_2","first-page":"38","article-title":"Multilevel Stack Automata","volume":"12","author":"Maslov A. N.","year":"1976","unstructured":"A. N. Maslov. 1976. Multilevel Stack Automata. Problems of Information Transmission 12 (1976), 38\u201343.","journal-title":"Problems of Information Transmission"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1137\/0213029"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.9"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.4171\/AUTOMATA-1\/2"},{"key":"e_1_3_1_56_2","unstructured":"Sylvain Schmitz. 2017. Algorithmic Complexity of Well-Quasi-Orders. (Complexit\u00e9 algorithmique des beaux pr\u00e9-ordres). https:\/\/tel.archives-ouvertes.fr\/tel-01663266"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.4171\/AUTOMATA-1\/16"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/8811.001.0001"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3143-9"},{"key":"e_1_3_1_60_2","doi-asserted-by":"crossref","unstructured":"Georg Zetzsche. 2015. An approach to computing downward closures. arXiv:1503.01068 [cs.FL]https:\/\/arxiv.org\/abs\/1503.01068","DOI":"10.1007\/978-3-662-47666-6_35"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209201"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776661","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:44:15Z","timestamp":1784209455000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776661"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776661"],"URL":"https:\/\/doi.org\/10.1145\/3776661","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"}}]}}