{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:40:22Z","timestamp":1760056822499,"version":"build-2065373602"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"5","funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["462679611"],"award-info":[{"award-number":["462679611"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Polish National Science Centre SONATA BIS-12","award":["2022\/46\/E\/ST6\/00230"],"award-info":[{"award-number":["2022\/46\/E\/ST6\/00230"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2025,10,31]]},"abstract":"<jats:p>\n            Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in\n            <jats:sans-serif>EXPSPACE<\/jats:sans-serif>\n            (Rackoff, \u201978) and is\n            <jats:sans-serif>EXPSPACE<\/jats:sans-serif>\n            -hard already under unary encodings (Lipton, \u201976). More precisely, Rosier and Yen later utilise Rackoff\u2019s bounding technique to show that if coverability holds then there is a run of length at most\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(n^{2^{\\mathcal {O}(d \\log (d))}}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            , where\n            <jats:italic toggle=\"yes\">d<\/jats:italic>\n            is the dimension and\n            <jats:italic toggle=\"yes\">n<\/jats:italic>\n            is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in\n            <jats:italic toggle=\"yes\">d<\/jats:italic>\n            -dimensional unary VASS that are only witnessed by runs of length at least\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(n^{2^{\\Omega (d)}}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            . Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\log (d)\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            factor, thus matching Lipton\u2019s lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(n^{2^{\\mathcal {O}(d)}}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            -time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(n^{2^{o(d)}}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            -time algorithm, conditioned upon the exponential time hypothesis. When analysing coverability, a standard proof technique is to consider VASS with bounded counters. Bounded VASS make for an interesting and popular model due to strong connections with timed automata. Withal, we study a natural setting where the counter bound is linear in the size of the VASS. Here the trivial exhaustive search algorithm runs in\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathcal {O}(n^{d+1})\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            time. We give evidence to this being near-optimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(n^{2-o(1)}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            time is required under the\n            <jats:italic toggle=\"yes\">k<\/jats:italic>\n            -cycle hypothesis. In general, for any fixed dimension\n            <jats:italic toggle=\"yes\">d<\/jats:italic>\n            \u2265 4, we show that\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(n^{d-2-o(1)}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            time is required under the 3-uniform hyperclique hypothesis.\n          <\/jats:p>","DOI":"10.1145\/3762178","type":"journal-article","created":{"date-parts":[[2025,8,29]],"date-time":"2025-08-29T11:47:27Z","timestamp":1756468047000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Coverability in VASS Revisited: Improving Rackoff\u2019s Bounds to Obtain Conditional Optimality"],"prefix":"10.1145","volume":"72","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4813-4852","authenticated-orcid":false,"given":"Marvin","family":"K\u00fcnnemann","sequence":"first","affiliation":[{"name":"Karlsruhe Institute of Technology","place":["Karlsruhe, Germany"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4535-6508","authenticated-orcid":false,"given":"Filip","family":"Mazowiecki","sequence":"additional","affiliation":[{"name":"University of Warsaw","place":["Warszawa, Poland"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4002-5491","authenticated-orcid":false,"given":"Lia","family":"Sch\u00fctze","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS)","place":["Kaiserslautern, Germany"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1653-4069","authenticated-orcid":false,"given":"Henry","family":"Sinclair-Banks","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Warwick","place":["Coventry, United Kingdom of Great Britain and Northern Ireland"]},{"name":"Mathematics, Informatics and Mechanics, University of Warsaw","place":["Coventry, United Kingdom of Great Britain and Northern Ireland"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9746-5733","authenticated-orcid":false,"given":"Karol","family":"W\u0119grzycki","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Informatics","place":["Saarbr\u00fccken, Germany"]}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2843"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.4007\/annals.2004.160.781"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.38"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02523189"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2019.13"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005101"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3464794"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_1"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/1970398.1970403"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24288-5_10"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITCS.2024.22"},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158118","article-title":"Optimal dyck reachability for data-dependence and alias analysis","volume":"2","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis. 2017. Optimal dyck reachability for data-dependence and alias analysis. Proc. ACM Program. Lang. 2, POPL (2017), 1\u201330.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.05.001"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2006.04.007"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS61266.2024.00086"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028751"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21275-3"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2020.48"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3422822"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533357"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS54457.2022.00034"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1137\/20M1335054"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ESA.2023.42"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-65306-6_20"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_21"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.39"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_25"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_6"},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/BFb0028575","volume-title":"Proceedings of the STACS 98: 15th Annual Symposium on Theoretical Aspects of Computer Science Paris","author":"Hagerup Torben","year":"1998","unstructured":"Torben Hagerup. 1998. Sorting and searching on the word RAM. In Proceedings of the STACS 98: 15th Annual Symposium on Theoretical Aspects of Computer Science Paris. Springer, 366\u2013398."},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1727"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2812"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571252"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104582"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:5)2013"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785796"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611975031.80"},{"key":"e_1_3_3_45_2","article-title":"The reachability problem requires exponential space","volume":"62","author":"Lipton Richard","year":"1976","unstructured":"Richard Lipton. 1976. The reachability problem requires exponential space. Dep. Comput. Sci., Yale Univ. 62 (1976), 1\u201316.","journal-title":"Dep. Comput. Sci., Yale Univ."},{"issue":"105","key":"e_1_3_3_46_2","article-title":"Lower bounds based on the exponential time hypothesis","volume":"3","author":"Lokshtanov Daniel","year":"2013","unstructured":"Daniel Lokshtanov, D\u00e1niel Marx, and Saket Saurabh. 2013. Lower bounds based on the exponential time hypothesis. Bulletin of EATCS 3, 105 (2013), 47\u201372.","journal-title":"Bulletin of EATCS"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434315"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1137\/0213029"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(82)90048-2"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2019.28"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30829-1_10"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"issue":"2","key":"e_1_3_3_53_2","first-page":"415","article-title":"On the complexity of the subgraph problem","volume":"26","author":"Ne\u0161et\u0159il Jaroslav","year":"1985","unstructured":"Jaroslav Ne\u0161et\u0159il and Svatopluk Poljak. 1985. On the complexity of the subgraph problem. Comment. Math. Univ. Carol. 26, 2 (1985), 415\u2013419.","journal-title":"Comment. Math. Univ. Carol."},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90006-1"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893585"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ICALP.2024.153"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/230514.571645"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80005-5"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63139-9_48"},{"key":"e_1_3_3_61_2","first-page":"254","volume-title":"Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004","author":"Yuster Raphael","year":"2004","unstructured":"Raphael Yuster and Uri Zwick. 2004. Detecting short directed cycles using rectangular matrix multiplication and dynamic programming. In Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004, J. Ian Munro (Ed.). SIAM, 254\u2013260. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id=982792.982828"},{"issue":"8","key":"e_1_3_3_62_2","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1080\/00029890.1997.11990704","article-title":"Newman\u2019s short proof of the prime number theorem","volume":"104","author":"Zagier Don","year":"1997","unstructured":"Don Zagier. 1997. Newman\u2019s short proof of the prime number theorem. Am. Math. Mon. 104, 8 (1997), 705\u2013708.","journal-title":"Am. Math. Mon."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3762178","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:38:05Z","timestamp":1760017085000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3762178"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":61,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,10,31]]}},"alternative-id":["10.1145\/3762178"],"URL":"https:\/\/doi.org\/10.1145\/3762178","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2024-03-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-29","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}