{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T04:26:52Z","timestamp":1781756812978,"version":"3.54.5"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"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":["787367, 101077902"],"award-info":[{"award-number":["787367, 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":[[2024,1,2]]},"abstract":"<jats:p>Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero. Whether the reachability problem is decidable for PVASS is a long-standing open problem.<\/jats:p>\n          <jats:p>\n            We consider\n            <jats:italic toggle=\"yes\">continuous PVASS<\/jats:italic>\n            , which are PVASS with a continuous semantics. This means, the counter values are rational numbers and whenever a vector is added to the current counter values, this vector is first scaled with an arbitrarily chosen rational factor between zero and one.\n          <\/jats:p>\n          <jats:p>\n            We show that reachability in continuous PVASS is\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>NEXPTIME<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -complete. Our result is unusually robust: Reachability can be decided in\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>NEXPTIME<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            even if all numbers are specified in binary. On the other hand,\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>NEXPTIME<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -hardness already holds for coverability, in fixed dimension, for bounded stack, and even if all numbers are specified in unary.\n          <\/jats:p>","DOI":"10.1145\/3633279","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"90-114","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Reachability in Continuous Pushdown VASS"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7258-5445","authenticated-orcid":false,"given":"A. R.","family":"Balasubramanian","sequence":"first","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"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":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533329"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185632.2185647"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2011.152"},{"key":"e_1_3_1_7_1","unstructured":"A. R. Balasubramanian Rupak Majumdar Ramanathan S. Thinniyam and Georg Zetzsche. 2023. Reachability in Continuous Pushdown VASS. arXiv (2023). https:\/\/arxiv.org\/abs2310.16798"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571266"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-663-09367-1"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005068"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328460"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Wojciech Czerwinski and Lukasz Orlikowski. 2022. Reachability in Vector Addition Systems Is Ackermann-complete. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). 1229\u20131240. https:\/\/doi.org\/10.1109\/FOCS52979.2021.00120 10.1109\/FOCS52979.2021.00120","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"e_1_3_1_15_1","unstructured":"Ren\u00e9 David. 1987. Continuous Petri nets. In Proc. 8th European Workshop on Appli. & Theory of Petri nets 1987."},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2020.106079"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2011.03.019"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2015-1168"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2022.124"},{"key":"e_1_3_1_20_1","volume-title":"Decidability questions for Petri Nets","author":"Th\u00e9odore Hack Michel Henri","year":"1976","unstructured":"Michel Henri Th\u00e9odore Hack. 1976. Decidability questions for Petri Nets. Ph. D. Dissertation. Massachusetts Institute of Technology."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498673"},{"key":"e_1_3_1_23_1","doi-asserted-by":"crossref","unstructured":"J\u00e9r\u00f4me Leroux. 2022. The reachability problem for Petri nets is not primitive recursive. In 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). IEEE 1241\u20131252.","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785796"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_26"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434340"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.MFCS.2022.71"},{"key":"e_1_3_1_28_1","unstructured":"Christos H. Papadimitriou. 2007. Computational complexity. Academic Internet Publ."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.042"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837659"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)80006-8"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90006-1"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30806-3_15"},{"key":"e_1_3_1_36_1","unstructured":"Michael Sipser. 2012. Introduction to the Theory of Computation. Cengage Learning."},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90076-6"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"},{"key":"e_1_3_1_40_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\/10.1145\/3633279","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3633279","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:03:10Z","timestamp":1751659390000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633279"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3633279"],"URL":"https:\/\/doi.org\/10.1145\/3633279","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}