Document Open Access Logo

Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality

Authors Marvin Künnemann, Filip Mazowiecki, Lia Schütze , Henry Sinclair-Banks , Karol Węgrzycki

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2023.131.pdf
  • Filesize: 1 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • Vector Addition System
  • Coverability
  • Reachability
  • Fine-Grained Complexity
  • Exponential Time Hypothesis
  • k-Cycle Hypothesis
  • Hyperclique Hypothesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackoff’s bounding technique to show that if coverability holds then there is a run of length at most n^{2^𝒪(d log d)}, where d is the dimension and n is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in d-dimensional unary VASS that are only witnessed by runs of length at least n^{2^Ω(d)}. Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated log(d) factor, thus matching Lipton’s lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic n^{2^𝒪(d)}-time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic n^{2^o(d)}-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^{d+1})-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^{2-o(1)}-time is required under the k-cycle hypothesis. In general fixed dimension d, we show that n^{d-2-o(1)}-time is required under the 3-uniform hyperclique hypothesis.

Cite As Get BibTex

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 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 131:1-131:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ICALP.2023.131

Author Details

Marvin Künnemann
  • RPTU Kaiserslautern-Landau, Germany
Filip Mazowiecki
  • University of Warsaw, Poland
Lia Schütze
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Henry Sinclair-Banks
  • Centre for Discrete Mathematics and its Applications (DIMAP) & Department of Computer Science, University of Warwick, Coventry, UK
Karol Węgrzycki
  • Saarland University and Max Planck Institute for Informatics, Saarbrücken, Germany

Funding

  • Künnemann, Marvin: Research partially supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 462679611.
  • Mazowiecki, Filip: Supported by the ERC grant INFSYS, agreement no. 950398.
  • Sinclair-Banks, Henry: Supported by EPSRC Standard Research Studentship (DTP), grant number EP/T5179X/1.
  • Węgrzycki, Karol: Supported by the ERC grant TIPEA, agreement no. 850979.

Acknowledgements

We would like to thank our anonymous reviewers for their comments, for their time, and especially for highlighting a piece of related work [Ulla Koppenhagen and Ernst W. Mayr, 2000].

References

  1. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput., 160(1-2):109-127, 2000. URL: https://doi.org/10.1006/inco.1999.2843.
  2. Manindra Agrawal, Neeraj Kayal, and Nitin Saxena. Primes is in P. Annals of Mathematics, pages 781-793, 2004. Google Scholar
  3. Shaull Almagor, Nathann Cohen, Guillermo A. Pérez, Mahsa Shirmohammadi, and James Worrell. Coverability in 1-VASS with Disequality Tests. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 38:1-38:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.38.
  4. Noga Alon, Raphael Yuster, and Uri Zwick. Finding and counting given length cycles. Algorithmica, 17(3):209-223, 1997. URL: https://doi.org/10.1007/BF02523189.
  5. Bertie Ancona, Monika Henzinger, Liam Roditty, Virginia Vassilevska Williams, and Nicole Wein. Algorithms and hardness for diameter in dynamic graphs. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.13.
  6. Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazić, 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.
  7. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the Coverability Problem Continuously. In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, 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.
  8. Michael Blondin, Christoph Haase, and Philip Offtermatt. Directed reachability for infinite-state systems. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 3-23. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_1.
  9. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. URL: https://doi.org/10.1145/1970398.1970403.
  10. Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for VASS. In Giorgio Delzanno and Igor Potapov, editors, Reachability Problems - 5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011. Proceedings, 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.
  11. Jianer Chen, Benny Chor, Mike Fellows, Xiuzhen Huang, David W. Juedes, Iyad A. Kanj, and Ge Xia. Tight lower bounds for certain parameterized NP-hard problems. Inf. Comput., 201(2):216-231, 2005. URL: https://doi.org/10.1016/j.ic.2005.05.001.
  12. Jianer Chen, Xiuzhen Huang, Iyad A. Kanj, and Ge Xia. Strong computational lower bounds via parameterized complexity. J. Comput. Syst. Sci., 72(8):1346-1367, 2006. URL: https://doi.org/10.1016/j.jcss.2006.04.007.
  13. Hubert Comon and Yan Jurski. Multiple counters automata, safety analysis and presburger arithmetic. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, volume 1427 of Lecture Notes in Computer Science, pages 268-279. Springer, 1998. URL: https://doi.org/10.1007/BFb0028751.
  14. Marek Cygan, Fedor V. Fomin, Łukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21275-3.
  15. Wojciech Czerwiński, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 48:1-48:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.48.
  16. Wojciech Czerwiński and Łukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  17. Wojciech Czerwiński and Łukasz Orlikowski. Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2-5, 2022, pages 40:1-40:12. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533357.
  18. Mina Dalirrooyfard, Ce Jin, Virginia Vassilevska Williams, and Nicole Wein. Approximation Algorithms and Hardness for n-Pairs Shortest Paths and All-Nodes Shortest Cycles. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 290-300. IEEE, 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00034.
  19. Mina Dalirrooyfard, Thuy Duong Vuong, and Virginia Vassilevska Williams. Graph pattern detection: Hardness for all induced patterns and faster noninduced cycles. SIAM J. Comput., 50(5):1627-1662, 2021. URL: https://doi.org/10.1137/20M1335054.
  20. Javier Esparza. Decidability and Complexity of Petri Net Problems - An Introduction. In Wolfgang Reisig and Grzegorz Rozenberg, editors, 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.
  21. Javier Esparza, Ruslán Ledesma-Garza, Rupak Majumdar, Philipp J. Meyer, and Filip Niksic. An SMT-Based Approach to Coverability Analysis. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, 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.
  22. John Fearnley and Marcin Jurdziński. Reachability in Two-Clock Timed Automata Is PSPACE-Complete. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 212-223. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_21.
  23. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 269-278. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  24. Pierre Ganty and Rupak Majumdar. Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst., 34(1):6:1-6:48, 2012. URL: https://doi.org/10.1145/2160910.2160915.
  25. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. URL: https://doi.org/10.1145/146637.146681.
  26. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in Succinct and Parametric One-Counter Automata. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 369-383. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04081-8_25.
  27. Christoph Haase, Joël Ouaknine, and James Worrell. On the relationship between reachability problems in timed and counter automata. In Alain Finkel, Jérôme Leroux, and Igor Potapov, editors, Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings, volume 7550 of Lecture Notes in Computer Science, pages 54-65. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33512-9_6.
  28. John E. Hopcroft and Jean-Jacques Pansiot. On the Reachability Problem for 5-Dimensional Vector Addition Systems. Theor. Comput. Sci., 8:135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  29. Russell Impagliazzo and Ramamohan Paturi. On the Complexity of k-SAT. J. Comput. Syst. Sci., 62(2):367-375, 2001. URL: https://doi.org/10.1006/jcss.2000.1727.
  30. Ulla Koppenhagen and Ernst W. Mayr. Optimal algorithms for the coverability, the subword, the containment, and the equivalence problems for commutative semigroups. Inf. Comput., 158(2):98-124, 2000. URL: https://doi.org/10.1006/inco.1999.2812.
  31. 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, 2023. URL: http://arxiv.org/abs/2305.01581.
  32. Ranko Lazic and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. Inf. Comput., 277:104582, 2021. URL: https://doi.org/10.1016/j.ic.2020.104582.
  33. Jérôme Leroux. Vector addition system reversible reachability problem. Log. Methods Comput. Sci., 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:5)2013.
  34. Jérôme Leroux. The Reachability Problem for Petri Nets is Not Primitive Recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241-1252. IEEE, 2021. 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 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  36. Andrea Lincoln, Virginia Vassilevska Williams, and R. Ryan Williams. Tight hardness for shortest cycles and paths in sparse graphs. In Artur Czumaj, editor, Proceedings of the Twenty-Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2018, New Orleans, LA, USA, January 7-10, 2018, pages 1236-1252. SIAM, 2018. URL: https://doi.org/10.1137/1.9781611975031.80.
  37. Richard Lipton. The Reachability Problem Requires Exponential Space. Department of Computer Science. Yale University, 62, 1976. Google Scholar
  38. Daniel Lokshtanov, Dániel Marx, and Saket Saurabh. Lower bounds based on the Exponential Time Hypothesis. Bulletin of EATCS, 3(105), 2013. Google Scholar
  39. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput., 13(3):441-460, 1984. URL: https://doi.org/10.1137/0213029.
  40. Ernst W. Mayr and Albert R. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46(3):305-329, 1982. URL: https://doi.org/10.1016/0001-8708(82)90048-2.
  41. Filip Mazowiecki and Michał Pilipczuk. Reachability for Bounded Branching VASS. In Wan J. Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 28:1-28:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.28.
  42. Filip Mazowiecki, Henry Sinclair-Banks, and Karol Węgrzycki. Coverability in 2-VASS with One Unary Counter is in NP. In Orna Kupferman and Paweł Sobociński, editors, Foundations of Software Science and Computation Structures, pages 196-217. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_10.
  43. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967. Google Scholar
  44. Jaroslav Nešetřil and Svatopluk Poljak. On the complexity of the subgraph problem. Commentationes Mathematicae Universitatis Carolinae, 26(2):415-419, 1985. Google Scholar
  45. Charles Rackoff. The Covering and Boundedness Problems for Vector Addition Systems. Theor. Comput. Sci., 6:223-231, 1978. URL: https://doi.org/10.1016/0304-3975(78)90036-1.
  46. 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.
  47. Sylvain Schmitz. The Complexity of Reachability in Vector Addition Systems. ACM SIGLOG News, 3(1):4-21, 2016. URL: https://dl.acm.org/citation.cfm?id=2893585, URL: https://doi.org/10.1145/2893582.2893585.
  48. 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.
  49. Wil M. P. van der Aalst. Verification of Workflow Nets. In Pierre Azéma and Gianfranco Balbo, editors, Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN '97, Toulouse, France, June 23-27, 1997, Proceedings, volume 1248 of Lecture Notes in Computer Science, pages 407-426. Springer, 1997. URL: https://doi.org/10.1007/3-540-63139-9_48.
  50. Raphael Yuster and Uri Zwick. Detecting short directed cycles using rectangular matrix multiplication and dynamic programming. In J. Ian Munro, editor, Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14, 2004, pages 254-260. SIAM, 2004. URL: http://dl.acm.org/citation.cfm?id=982792.982828.
  51. Don Zagier. Newman’s short proof of the prime number theorem. The American mathematical monthly, 104(8):705-708, 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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