{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,7]],"date-time":"2026-03-07T00:35:51Z","timestamp":1772843751941,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2021,8,12]],"date-time":"2021-08-12T00:00:00Z","timestamp":1628726400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003151","name":"Fonds de recherche du Qu\u00e9bec \u2013 Nature et technologies","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003151","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100005713","name":"Technical University of Munich","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005713","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004794","name":"Centre national de la recherche scientifique","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004794","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cChaire Digiteo, ENS Cachan \u2014 \u00c9cole Polytechnique\u201d"},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/M011801\/1 and EP\/M027651\/1"],"award-info":[{"award-number":["EP\/M011801\/1 and EP\/M027651\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Agence nationale de la recherche,","award":["ANR-11-BS02-001"],"award-info":[{"award-number":["ANR-11-BS02-001"]}]},{"name":"Labex Digicosme, Universit\u00e9 Paris-Saclay, project VERICONISS"},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cChaire Digiteo, ENS Cachan \u2014 \u00c9cole Polytechnique\u201d"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>We prove that the reachability problem for two-dimensional vector addition systems with states is NL-complete or PSPACE-complete, depending on whether the numbers in the input are encoded in unary or binary. As a key underlying technical result, we show that, if a configuration is reachable, then there exists a witnessing path whose sequence of transitions is contained in a bounded language defined by a regular expression of pseudo-polynomially bounded length. This, in turn, enables us to prove that the lengths of minimal reachability witnesses are pseudo-polynomially bounded.<\/jats:p>","DOI":"10.1145\/3464794","type":"journal-article","created":{"date-parts":[[2021,8,12]],"date-time":"2021-08-12T19:06:46Z","timestamp":1628795206000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["The Reachability Problem for Two-Dimensional Vector Addition Systems with States"],"prefix":"10.1145","volume":"68","author":[{"given":"Michael","family":"Blondin","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Sherbrooke, Sherbrooke, QC, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Englert","sequence":"additional","affiliation":[{"name":"University of Warwick, Conventry, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Finkel","sequence":"additional","affiliation":[{"name":"Laboratoire LMF, Universit\u00e9 Paris-Saclay, CNRS, ENS Paris-Saclay, IUF, Gif\/Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"G\u00d6ller","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Kassel, Kassel, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Haase","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranko","family":"Lazi\u0107","sequence":"additional","affiliation":[{"name":"University of Warwick, Conventry, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Mckenzie","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Montr\u00e9al, Montr\u00e9al, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Totzke","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1137\/090779401"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11047-010-9180-6"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.14"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488608.2488626"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.15"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800113.803630"},{"key":"e_1_2_1_7_1","volume-title":"Shortest paths in one-counter systems. Logical Methods in Computer Science 15, 1","author":"Chistikov Dmitry","year":"2019","unstructured":"Dmitry Chistikov , Wojciech Czerwinski , Piotr Hofman , Michal Pilipczuk , and Michael Wehar . 2019. Shortest paths in one-counter systems. Logical Methods in Computer Science 15, 1 ( 2019 ). https:\/\/lmcs.episciences.org\/5251. Dmitry Chistikov, Wojciech Czerwinski, Piotr Hofman, Michal Pilipczuk, and Michael Wehar. 2019. Shortest paths in one-counter systems. Logical Methods in Computer Science 15, 1 (2019). https:\/\/lmcs.episciences.org\/5251."},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"The taming of the semi-linear set. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP)","volume":"128","author":"Chistikov Dmitry","year":"2016","unstructured":"Dmitry Chistikov and Christoph Haase . 2016 . The taming of the semi-linear set. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP) . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 128 : 1 \u2013 128 :13. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.128 10.4230\/LIPIcs.ICALP.2016.128 Dmitry Chistikov and Christoph Haase. 2016. The taming of the semi-linear set. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 128:1\u2013128:13. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.128","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330014"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3313276.3316369"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science (MFCS) (LIPIcs)","volume":"138","author":"Czerwinski Wojciech","year":"2019","unstructured":"Wojciech Czerwinski , Slawomir Lasota , Christof L\u00f6ding , and Radoslaw Pi\u00f3rkowski . 2019 . New pumping technique for 2-dimensional VASS . In Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science (MFCS) (LIPIcs) , Vol. 138 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 62:1\u201362:14. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS. 2019.62 10.4230\/LIPIcs.MFCS.2019.62 Wojciech Czerwinski, Slawomir Lasota, Christof L\u00f6ding, and Radoslaw Pi\u00f3rkowski. 2019. New pumping technique for 2-dimensional VASS. In Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science (MFCS) (LIPIcs), Vol. 138. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 62:1\u201362:14. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.62"},{"key":"e_1_2_1_12_1","volume-title":"A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett. 167","author":"Englert Matthias","year":"2021","unstructured":"Matthias Englert , Piotr Hofman , Slawomir Lasota , Ranko Lazic , J\u00e9r\u00f4me Leroux , and Juliusz Straszynski . 2021. A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett. 167 ( 2021 ). https:\/\/doi.org\/10.1016\/j.ipl.2020.106079 10.1016\/j.ipl.2020.106079 Matthias Englert, Piotr Hofman, Slawomir Lasota, Ranko Lazic, J\u00e9r\u00f4me Leroux, and Juliusz Straszynski. 2021. A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett. 167 (2021). https:\/\/doi.org\/10.1016\/j.ipl.2020.106079"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933577"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.12.004"},{"key":"e_1_2_1_15_1","first-page":"1","article-title":"Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In Proceedings of the 44th International Colloquium on Automata, Languages, and Programming (ICALP) (LIPIcs), Vol. 80","volume":"119","author":"Figueira Diego","year":"2017","unstructured":"Diego Figueira , Ranko Lazic , J\u00e9r\u00f4me Leroux , Filip Mazowiecki , and Gr\u00e9goire Sutre . 2017 . Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In Proceedings of the 44th International Colloquium on Automata, Languages, and Programming (ICALP) (LIPIcs), Vol. 80 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 119 : 1 \u2013 119 :14. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.119 10.4230\/LIPIcs.ICALP.2017.119 Diego Figueira, Ranko Lazic, J\u00e9r\u00f4me Leroux, Filip Mazowiecki, and Gr\u00e9goire Sutre. 2017. Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In Proceedings of the 44th International Colloquium on Automata, Languages, and Programming (ICALP) (LIPIcs), Vol. 80. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 119:1\u2013119:14. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2017.119","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 38th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) (LIPIcs)","volume":"122","author":"Finkel Alain","year":"2018","unstructured":"Alain Finkel , J\u00e9r\u00f4me Leroux , and Gr\u00e9goire Sutre . 2018 . Reachability for two-counter machines with one test and one reset . In Proceedings of the 38th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) (LIPIcs) , Vol. 122 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 31:1\u201331:14. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS. 2018.31 10.4230\/LIPIcs.FSTTCS.2018.31 Alain Finkel, J\u00e9r\u00f4me Leroux, and Gr\u00e9goire Sutre. 2018. Reachability for two-counter machines with one test and one reset. In Proceedings of the 38th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) (LIPIcs), Vol. 122. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 31:1\u201331:14. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2018.31"},{"key":"e_1_2_1_17_1","first-page":"1","article-title":"A polynomial-time algorithm for reachability in branching VASS in dimension one. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP) (LIPIcs), Vol. 55","volume":"105","author":"G\u00f6ller Stefan","year":"2016","unstructured":"Stefan G\u00f6ller , Christoph Haase , Ranko Lazic , and Patrick Totzke . 2016 . A polynomial-time algorithm for reachability in branching VASS in dimension one. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP) (LIPIcs), Vol. 55 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 105 : 1 \u2013 105 :13. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.105 10.4230\/LIPIcs.ICALP.2016.105 Stefan G\u00f6ller, Christoph Haase, Ranko Lazic, and Patrick Totzke. 2016. A polynomial-time algorithm for reachability in branching VASS in dimension one. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP) (LIPIcs), Vol. 55. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 105:1\u2013105:13. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.105","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_25"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/21545.21546"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629608"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90173-D"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2015.2435696"},{"key":"e_1_2_1_25_1","volume-title":"The general vector addition system reachability problem by Presburger inductive invariants. Logical Methods in Computer Science 6, 3","author":"Leroux J\u00e9r\u00f4me","year":"2010","unstructured":"J\u00e9r\u00f4me Leroux . 2010. The general vector addition system reachability problem by Presburger inductive invariants. Logical Methods in Computer Science 6, 3 ( 2010 ). https:\/\/doi.org\/10.2168\/LMCS-6(3:22)2010 10.2168\/LMCS-6(3:22)2010 J\u00e9r\u00f4me Leroux. 2010. The general vector addition system reachability problem by Presburger inductive invariants. Logical Methods in Computer Science 6, 3 (2010). https:\/\/doi.org\/10.2168\/LMCS-6(3:22)2010"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926421"},{"key":"e_1_2_1_27_1","volume-title":"Turing-100 (EPiC Series in Computing)","author":"Leroux J\u00e9r\u00f4me","unstructured":"J\u00e9r\u00f4me Leroux . 2012. Vector addition systems reachability problem (a simpler solution) . In Turing-100 (EPiC Series in Computing) , Vol. 10 . EasyChair , 214\u2013228. http:\/\/www.easychair.org\/publications\/paper\/106497. J\u00e9r\u00f4me Leroux. 2012. Vector addition systems reachability problem (a simpler solution). In Turing-100 (EPiC Series in Computing), Vol. 10. EasyChair, 214\u2013228. http:\/\/www.easychair.org\/publications\/paper\/106497."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/3470152.3470202"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_26"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) (LIPIcs)","volume":"171","author":"Leroux J\u00e9r\u00f4me","year":"2020","unstructured":"J\u00e9r\u00f4me Leroux and Gr\u00e9goire Sutre . 2020 . Reachability in two-dimensional vector addition systems with states: One test is for free . In Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) (LIPIcs) , Vol. 171 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 37:1\u201337:17. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR. 2020.37 10.4230\/LIPIcs.CONCUR.2020.37 J\u00e9r\u00f4me Leroux and Gr\u00e9goire Sutre. 2020. Reachability in two-dimensional vector addition systems with states: One test is for free. In Proceedings of the 31st International Conference on Concurrency Theory (CONCUR) (LIPIcs), Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 37:1\u201337:17. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2020.37"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_26"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.14778\/3157794.3157798"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_2_1_35_1","volume-title":"Proc. 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 43:1\u201343:15","author":"Michaliszyn Jakub","year":"2017","unstructured":"Jakub Michaliszyn , Jan Otop , and Piotr Wieczorek . 2017 . Querying best paths in graph databases . In Proc. 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 43:1\u201343:15 . https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2017.43 10.4230\/LIPIcs.FSTTCS.2017.43 Jakub Michaliszyn, Jan Otop, and Piotr Wieczorek. 2017. Querying best paths in graph databases. In Proc. 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 43:1\u201343:15. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2017.43"},{"key":"e_1_2_1_36_1","volume-title":"Computational Complexity","author":"Papadimitriou Christos H.","unstructured":"Christos H. Papadimitriou . 1994. Computational Complexity . Addison-Wesley . Christos H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/111853.111867"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/800105.803396"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858784"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80005-5"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464794","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3464794","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:11Z","timestamp":1750191431000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,12]]},"references-count":40,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3464794"],"URL":"https:\/\/doi.org\/10.1145\/3464794","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,12]]},"assertion":[{"value":"2019-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-08-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}