Document Open Access Logo

A Note on the Parameterised Complexity of Coverability in Vector Addition Systems

Authors Michał Pilipczuk , Sylvain Schmitz , Henry Sinclair-Banks

PDF

File

Thumbnail PDF
PDF
LIPIcs.IPEC.2025.24.pdf
  • Filesize: 1.44 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Parameterized complexity and exact algorithms
  • Software and its engineering → Model checking
  • Theory of computation → Concurrency
Keywords
  • vector addition system
  • Petri net
  • parameterised complexity
  • coverability

Metrics

Abstract

We investigate the parameterised complexity of the classic coverability problem for vector addition systems (VAS): V ⊆ ℤ^d, an initial configuration s ∈ ℕ^d, and a target configuration t ∈ ℕ^d, decide whether starting from s, one can iteratively add vectors from V to ultimately arrive at a configuration that is larger than or equal to t on every coordinate, while not observing any negative value on any coordinate along the way. We consider two natural parameters for the problem: the dimension d and the size of V, defined as the total bitsize of its encoding. We present several results charting the complexity of those two parameterisations, among which the highlight is that coverability for VAS parameterised by the dimension and with all the numbers in the input encoded in unary is complete for the class XNL under PL-reductions. We also discuss open problems in the topic, most notably the question about fixed-parameter tractability for the parameterisation by the size of V.

Cite As Get BibTex

Michał Pilipczuk, Sylvain Schmitz, and Henry Sinclair-Banks. A Note on the Parameterised Complexity of Coverability in Vector Addition Systems. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.IPEC.2025.24

Author Details

Michał Pilipczuk
  • Institute of Informatics, University of Warsaw, Poland
Sylvain Schmitz
  • Université Paris Cité, CNRS, IRIF, France
Henry Sinclair-Banks
  • Institute of Informatics, University of Warsaw, Poland

Funding

  • Pilipczuk, Michał: This work is a part of project BOBR that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 948057).
  • Sinclair-Banks, Henry: This work is a part of project INFSYS that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 950398).

Acknowledgements

This research was initiated during the InfAut 2024 workshop in Warlity Wielkie, Poland. The authors thank the organisers for launching such a fruitful event. They also thank an anonymous reviewer for pointing them to a relevant discussion in Hack’s PhD thesis [Michel Hack, 1976].

References

  1. Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig, Marco Montali, and Othmane Rezine. Complexity of reachability for data-aware dynamic systems. In Proceedings of ACSD 2018, pages 11-20. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/ACSD.2018.000-3.
  2. Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham, and Yaron Velner. Some complexity results for stateful network verification. Formal Methods in System Design, 54:191-231, 2019. URL: https://doi.org/10.1007/s10703-018-00330-9.
  3. Rutherford Aris. Prolegomena to the rational analysis of systems of chemical reactions. Archive for Rational Mechanics and Analysis, 19(2):81-99, 1965. URL: https://doi.org/10.1007/BF00282276.
  4. Rutherford Aris. Prolegomena to the rational analysis of systems of chemical reactions II. Some addenda. Archive for Rational Mechanics and Analysis, 27(5):356-364, 1968. URL: https://doi.org/10.1007/BF00251438.
  5. Paolo Baldan, Nicoletta Cocco, Andrea Marin, and Marta Simeoni. Petri nets for modelling metabolic pathways: A survey. Natural Computing, 9(4):955-989, 2010. URL: https://doi.org/10.1007/S11047-010-9180-6.
  6. Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Context-bounded verification of thread pools. In Proceedings of POPL 2012, volume 6 of Proceedings of the ACM on Programming Languages. ACM, 2022. URL: https://doi.org/10.1145/3498678.
  7. 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.
  8. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the coverability problem continuously. In Proceedings of TACAS 2016, volume 9636 of Lecture Notes in Computer Science, pages 480-496. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_28.
  9. Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for VASS. In Proceedings of RP 2011, volume 6945 of Lecture Notes in Computer Science, pages 96-109. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24288-5_10.
  10. Jin-Yi Cai and D. Sivakumar. Resolution of Hartmanis' conjecture for NL-hard sparse sets. Theoretical Computer Science, 240(2):257-269, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00234-0.
  11. Yijia Chen, Jörg Flum, and Martin Grohe. Bounded nondeterminism and alternation in parameterized complexity theory. In Proceedings of CCC 2003, pages 13-29. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/CCC.2003.1214407.
  12. Wojciech Czerwiński. Open problems in infinite-states systems, 2024. Webpage accessed on http://web.archive.org/web/20241207075917/https://www.mimuw.edu.pl/~wczerwin/research.html. URL: https://www.mimuw.edu.pl/~wczerwin/research.html.
  13. Wojciech Czerwiński and Lukasz Orlikowski. Reachability in vector addition systems is ACKERMANN-complete. In Proceedings of FOCS 2021, pages 1229-1240. IEEE Computer Society, 2022. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  14. Ronald de Haan and Stefan Szeider. A compendium of parameterized problems at higher levels of the polynomial hierarchy. Algorithms, 12(9):188, 2019. URL: https://doi.org/10.3390/A12090188.
  15. Normann Decker, Peter Habermehl, Martin Leucker, and Daniel Thoma. Ordered navigation on multi-attributed data words. In Proceedings of CONCUR 2014, volume 8704 of Lecture Notes in Computer Science, pages 497-511. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44584-6_34.
  16. Roberto Di Cosmo, Jacopo Mauro, Stefano Zacchiroli, and Gianluigi Zavattaro. Component reconfiguration in the presence of conflicts. In Proceedings of ICALP 2013, volume 7966 of Lecture Notes in Computer Science, pages 187-198. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_19.
  17. Andrei Draghici, Christoph Haase, and Andrew Ryzhikov. Reachability in fixed VASS: expressiveness and lower bounds. In Proceedings of FoSSaCS 2024, volume 14575 of Lecture Notes in Computer Science, pages 185-205. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57231-9_9.
  18. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification. In Proceedings of STACS 2014, volume 25 of Leibniz International Proceedings in Informatics, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.STACS.2014.1.
  19. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp Meyer, and Filip Niksic. An SMT-based approach to coverability analysis. In Proceedings of CAV 2014, volume 8559 of Lecture Notes in Computer Science, pages 603-619. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_40.
  20. John Fearnley and Marcin Jurdziński. Reachability in two-clock timed automata is PSPACE-complete. Information and Computation, 243:26-36, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.004.
  21. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Texts in Theoretical Computer Science. Springer, 2006. URL: https://doi.org/10.1007/3-540-29953-X.
  22. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems, 34(1), 2012. URL: https://doi.org/10.1145/2160910.2160915.
  23. Gilles Geeraerts, Alexander Heußner, and Jean-François Raskin. On the verification of concurrent, asynchronous programs with waiting queues. ACM Transactions on Embedded Computing Systems, 14(3), 2015. URL: https://doi.org/10.1145/2700072.
  24. Thomas Geffroy, Jérôme Leroux, and Grégoire Sutre. Occam’s Razor applied to the Petri net coverability problem. Theoretical Computer Science, 750:38-52, 2018. URL: https://doi.org/10.1016/j.tcs.2018.04.014.
  25. Radu Grigore and Nikos Tzevelekos. History-register automata. Logical Methods in Computer Science, 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:7)2016.
  26. Michel Hack. Decidability questions for Petri Nets. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1976. URL: https://hdl.handle.net/1721.1/27441.
  27. John Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theoretical Computer Science, 8(2):135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  28. Ismaël Jecker. Open problems in automata theory: 22.1 Complexity of fixed VAS reachability, 2022. Webpage accessed on https://web.archive.org/web/20250513003911/https://automata.exchange/22.01-complexity-fixed-vas-reachability/. URL: https://automata.exchange/22.01-complexity-fixed-vas-reachability/.
  29. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In Proceedings of CAV 2010, volume 6174 of Lecture Notes in Computer Science, pages 645-659. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_55.
  30. Max Kanovich, Paul Rowe, and Andre Scedrov. Policy compliance in collaborative systems. In Proceedings of CSF 2009, pages 218-233. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/CSF.2009.19.
  31. Richard M. Karp and Raymond E. Miller. Parallel program schemata. Journal of Computer and System Sciences, 3(2):147-195, 1969. URL: https://doi.org/10.1016/S0022-0000(69)80011-5.
  32. Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Węgrzycki. Coverability in VASS revisited: Improving Rackoff’s bound to obtain conditional optimality. In Proceedings of ICALP 2023, volume 261 of Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.131.
  33. Ranko Lazić and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. Information and Computation, 277:104582, 2021. URL: https://doi.org/10.1016/j.ic.2020.104582.
  34. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In Proceedings of FOCS 2021, pages 1241-1252. IEEE Computer Society, 2022. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  35. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In Proceedings of LICS 2019, pages 1-13. IEEE Computer Society, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  36. Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Department of Computer Science, Yale University, January 1976. URL: http://www.cs.yale.edu/publications/techreports/tr63.pdf.
  37. Stephen R. Mahaney. Sparse complete sets for NP: Solution of a conjecture of Berman and Hartmanis. Journal of Computer and System Sciences, 25(2):130-143, 1982. URL: https://doi.org/10.1016/0022-0000(82)90002-2.
  38. Carl A. Petri. Kommunikation mit Automaten. PhD thesis, Universität Bonn, 1962. URL: http://edoc.sub.uni-hamburg.de/informatik/volltexte/2011/160/.
  39. M. Praveen. Small vertex cover makes Petri net coverability and boundedness easier. Algorithmica, 65(4):713-753, 2013. URL: https://doi.org/10.1007/S00453-012-9687-6.
  40. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  41. Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. Journal of Computer and System Sciences, 32(1):105-135, 1986. URL: https://doi.org/10.1016/0022-0000(86)90006-1.
  42. Sylvain Schmitz. Automata column: The complexity of reachability in vector addition systems. ACM SIGLOG News, 3(1):3-21, 2016. URL: https://doi.org/10.1145/2893582.2893585.
  43. Sylvain Schmitz. Complexity hierarchies beyond ELEMENTARY. ACM Transactions on Computation Theory, 8(1), 2016. URL: https://doi.org/10.1145/2858784.
  44. Sylvain Schmitz and Lia Schütze. On the length of strongly monotone descending chains over ℕ^d. In Proceedings of ICALP 2024, volume 297 of Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.153.
  45. Dimitri Watel, Marc-Antoine Weisser, and Dominique Barth. Parameterized complexity and approximability of coverability problems in weighted Petri nets. In Proceedings of Petri Nets 2017, volume 10258 of Lecture Notes in Computer Science, pages 330-349. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-57861-3_19.
  46. Michael Wehar. On the Complexity of Intersection Non-Emptiness Problems. PhD thesis, University at Buffalo, State University of New York, USA, 2016. URL: http://www.michaelwehar.com/documents/mwehar_dissertation.pdf.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact