Document Open Access Logo

Reachability in VASS Extended with Integer Counters

Authors Clotilde Bizière , Wojciech Czerwiński , Roland Guttenberg , Jérôme Leroux , Vincent Michielini , Łukasz Orlikowski , Antoni Puch , Henry Sinclair-Banks

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.19.pdf
  • Filesize: 0.97 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
Keywords
  • vector addition systems
  • Petri nets
  • counter automata
  • reachability

Metrics

Abstract

We consider a variant of VASS extended with integer counters, denoted VASS+ℤ. These are automata equipped with ℕ- and ℤ-counters; the ℕ-counters are required to remain nonnegative and the ℤ-counters do not have this restriction. We study the complexity of the reachability problem for VASS+ℤ when the number of ℕ-counters is fixed. We show that reachability is NP-complete in 1-VASS+ℤ (i.e. when there is only one ℕ-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+ℤ lies in the complexity class ℱ_{d+2}. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the ℤ-counters with ℕ-counters.
To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of ℕ-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+ℤ is PSpace-hard; without ℤ-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+ℤ is Tower-hard. Without ℤ-counters, reachability in 3-VASS has elementary complexity and Tower-hardness is only known in dimension 8.

Cite As Get BibTex

Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, Antoni Puch, and Henry Sinclair-Banks. Reachability in VASS Extended with Integer Counters. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 19:1-19:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.19

Author Details

Clotilde Bizière
  • University of Bordeaux, France
  • University of Warsaw, Poland
Wojciech Czerwiński
  • University of Warsaw, Poland
Roland Guttenberg
  • University of Warsaw, Poland
Jérôme Leroux
  • University of Bordeaux, France
Vincent Michielini
  • University of Bordeaux, France
Łukasz Orlikowski
  • University of Warsaw, Poland
Antoni Puch
  • University of Warsaw, Poland
Henry Sinclair-Banks
  • University of Warsaw, Poland
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

  • Bizière, Clotilde: Supported by Polish National Science Centre SONATA BIS-12 grant number 2022/46/E/ST6/00230.
  • Czerwiński, Wojciech: Supported by the ERC grant INFSYS, agreement no. 950398.
  • Guttenberg, Roland: Supported by the ERC grant INFSYS, agreement no. 950398.
  • Leroux, Jérôme: Supported by the grant ANR-25-CE48-6933 of the French National Research Agency ANR (project CoqoPetri).
  • Michielini, Vincent: Supported by the ANR grant INTENDED (ANR-19-CHIA-0014).
  • Orlikowski, Łukasz: Supported by the ERC grant INFSYS, agreement no. 950398.
  • Puch, Antoni: Supported by the Polish National Science Centre Maestro grant no. 2022/46/A/ST6/ 00072.
  • Sinclair-Banks, Henry: Supported by the ERC grant INFSYS, agreement no. 950398.

Acknowledgements

We thank Kyveli Doveri and Georg Zetzsche for inspiring discussions about VASS extended with integer counters.

References

  1. Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, and Georg Zetzsche. The complexity of regular abstractions of one-counter languages. In Proceedings of LICS 2016, pages 207-216. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934561.
  2. Clotilde Bizière, Wojciech Czerwinski, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Lukasz Orlikowski, Antoni Puch, and Henry Sinclair-Banks. Reachability in VASS extended with integer counters. CoRR, abs/2603.05221, 2026. URL: https://doi.org/10.48550/arXiv.2603.05221.
  3. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazic, Pierre McKenzie, and Patrick Totzke. The reachability problem for two-dimensional vector addition systems with states. J. ACM, 68(5):34:1-34:43, 2021. URL: https://doi.org/10.1145/3464794.
  4. Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. In Proceedings of LICS 2015, pages 32-43. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.14.
  5. Dmitry Chistikov, Wojciech Czerwinski, Filip Mazowiecki, Lukasz Orlikowski, Henry Sinclair-Banks, and Karol Wegrzycki. The Tractability Border of Reachability in Simple Vector Addition Systems with States. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024, pages 1332-1354. IEEE, 2024. URL: https://doi.org/10.1109/FOCS61266.2024.00086.
  6. Dmitry Chistikov and Christoph Haase. The taming of the semi-linear set. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, Rome, Italy, July 11-15, 2016, volume 55 of LIPIcs, pages 128:1-128:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.128.
  7. Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, Jérôme Leroux, and Lukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In Proceedings of FSTTCS 2023, volume 284 of LIPIcs, pages 35:1-35:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2023.35.
  8. Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, and Lukasz Orlikowski. Reachability in 3-VASS Is Elementary. In Proceedings of ICALP 2025, volume 334 of LIPIcs, pages 153:1-153:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ICALP.2025.153.
  9. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The Reachability Problem for Petri Nets is not Elementary. In STOC, pages 24-33. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  10. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-Complete. In FOCS, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  11. Wojciech Czerwinski and Lukasz Orlikowski. Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes. In Proceedings of LICS 2022, pages 40:1-40:12. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533357.
  12. Stéphane Demri. On selective unboundedness of VASS. J. Comput. Syst. Sci., 79(5):689-713, 2013. URL: https://doi.org/10.1016/J.JCSS.2013.01.014.
  13. Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564-568, 2006. URL: https://doi.org/10.1016/J.ORL.2005.09.008.
  14. Javier Esparza. Decidability and Complexity of Petri Net Problems - An Introduction. In Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science, pages 374-428. Springer, 1996. URL: https://doi.org/10.1007/3-540-65306-6_20.
  15. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma. In LICS, pages 269-278. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  16. Patrick C. Fischer, Albert R. Meyer, and Arnold L. Rosenberg. Counter machines and counter languages. Mathematical Systems Theory, 2(3):265-283, 1968. URL: https://doi.org/10.1007/BF01694011.
  17. Yuxi Fu, Qizhe Yang, and Yangluo Zheng. Improved Algorithm for Reachability in d-VASS. In ICALP, volume 297 of LIPIcs, pages 136:1-136:18. Schloss Dagstuhl, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.136.
  18. Roland Guttenberg, Wojciech Czerwinski, and Slawomir Lasota. Reachability and Related Problems in Vector Addition Systems with Nested Zero Tests. In LICS, pages 581-593. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00050.
  19. Roland Guttenberg, Eren Keskin, and Roland Meyer. PVASS reachability is decidable. CoRR, abs/2504.05015, 2025. URL: https://doi.org/10.48550/arXiv.2504.05015.
  20. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In Proceedings of CONCUR 2009, pages 369-383. Springer Berlin Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  21. Rodney R. Howell, Louis E. Rosier, Dung T. Huynh, and Hsu-Chun Yen. Some Complexity Bounds for Problems Concerning Finite and 2-Dimensional Vector Addition Systems with States. Theor. Comput. Sci., 46(3):107-140, 1986. URL: https://doi.org/10.1016/0304-3975(86)90026-5.
  22. Lukasz Kaminski and Slawomir Lasota. Bi-reachability in petri nets with data. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory, CONCUR 2024, Calgary, Canada, September 9-13, 2024, LIPIcs, pages 31:1-31:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.31.
  23. Eren Keskin and Roland Meyer. On the Separability Problem of VASS Reachability Languages. In LICS, pages 49:1-49:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662116.
  24. S. Rao Kosaraju. Decidability of Reachability in Vector Addition Systems. In STOC, pages 267-281. ACM, 1982. Google Scholar
  25. Jean-Luc Lambert. A Structure to Decide Reachability in Petri Nets. Theor. Comput. Sci., 99(1):79-104, 1992. URL: https://doi.org/10.1016/0304-3975(92)90173-D.
  26. Slawomir Lasota. Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem. In Proceedings of STACS 2022, volume 219 of LIPIcs, pages 46:1-46:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.STACS.2022.46.
  27. Jérôme Leroux. The Reachability Problem for Petri Nets is Not Primitive Recursive. In FOCS, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  28. Jérôme Leroux and Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In LICS, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  29. Richard J. Lipton. The Reachability Problem Requires Exponential Space. Technical report, Yale University, 1976. Google Scholar
  30. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In STOC, pages 238-246. ACM, 1981. URL: https://doi.org/10.1145/800076.802477.
  31. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall Series in Automatic Computation. Prentice-Hall, 1967. Google Scholar
  32. Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. TCS, 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  33. Wolfgang Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-33278-4.
  34. Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci., 32(1):105-135, 1986. URL: https://doi.org/10.1016/0022-0000(86)90006-1.
  35. George S. Sacerdote and Richard L. Tenney. The Decidability of the Reachability Problem for Vector Addition Systems (Preliminary Version). In STOC, pages 61-76. ACM, 1977. URL: https://doi.org/10.1145/800105.803396.
  36. Sylvain Schmitz. Complexity Hierarchies beyond Elementary. ACM Trans. Comput. Theory, 8(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2858784.
  37. Alexander Schrijver. Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, 1999. Google Scholar
  38. Leslie G. Valiant and Mike Paterson. Deterministic one-counter automata. J. Comput. Syst. Sci., 10(3):340-350, 1975. URL: https://doi.org/10.1016/S0022-0000(75)80005-5.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact