Document Open Access Logo

New Lower Bounds for Reachability in Vector Addition Systems

Authors Wojciech Czerwiński , Ismaël Jecker, Sławomir Lasota , Jérôme Leroux, Łukasz Orlikowski

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2023.35.pdf
  • Filesize: 0.92 MB
  • 22 pages

Document Identifiers

Author Details

Wojciech Czerwiński
  • University of Warsaw, Poland
Ismaël Jecker
  • University of Warsaw, Poland
  • FEMTO-ST, CNRS, Univ. Franche-Comté, France
Sławomir Lasota
  • University of Warsaw, Poland
Jérôme Leroux
  • LaBRI, CNRS, Univ. Bordeaux, France
Łukasz Orlikowski
  • University of Warsaw, Poland

Funding

Wojciech Czerwiński, Ismaël Jecker and Łukasz Orlikowski: Supported by the ERC grant INFSYS, agreement no. 950398.
  • Lasota, Sławomir: Supported by the ERC grant INFSYS, agreement no. 950398 and by the NCN grant 2021/41/B/ST6/00535.
  • Leroux, Jérôme: Supported by the grant ANR-17-CE40-0028 of the French National Research Agency ANR (project BRAVAS).

Acknowledgements

We are grateful to Weijun Chen for his sharp observation that brought to light a technical error in the initial version of this paper.

Cite As Get BibTex

Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSTTCS.2023.35

Abstract

We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be F_d-hard for VASS of dimension 3d+2 (the complexity class F_d corresponds to the kth level of the fast-growing hierarchy), and no essentially better bound is known for pushdown VASS. We provide a new construction that improves the lower bound for VASS: F_d-hardness in dimension 2d+3. Furthermore, building on our new insights we show a new lower bound for pushdown VASS: F_d-hardness in dimension d/2 + 6. This dimension-parametric lower bound is strictly stronger than the upper bound for VASS, which suggests that the (still unknown) complexity of the reachability problem in pushdown VASS is higher than in plain VASS (where it is Ackermann-complete).

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Verification by model checking
  • Theory of computation → Logic and verification
Keywords
  • vector addition systems
  • reachability problem
  • pushdown vector addition system
  • lower bounds

Metrics

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

References

  1. Mohamed Faouzi Atig and Pierre Ganty. Approximating Petri Net Reachability Along Context-free Traces. In Proceedings of FSTTCS 2011, volume 13 of LIPIcs, pages 152-163, 2011. Google Scholar
  2. 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, 2015. Google Scholar
  3. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In Proceedings of STOC 2019, pages 24-33. ACM, 2019. Google Scholar
  4. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The Reachability Problem for Petri Nets Is Not Elementary. Journal of the ACM, 68(1):7:1-7:28, 2021. Google Scholar
  5. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-complete. In Proceedings of FOCS 2021, pages 1229-1240. IEEE, 2021. Google Scholar
  6. 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. Google Scholar
  7. Matthias Englert, Piotr Hofman, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Juliusz Straszynski. A lower bound for the coverability problem in acyclic pushdown VAS. Inf. Process. Lett., 167:106079, 2021. Google Scholar
  8. Matthias Englert, Ranko Lazić, and Patrick Totzke. Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete. In Proceedings of LICS 2016, pages 477-484. ACM, 2016. Google Scholar
  9. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In Proceeding of CONCUR 2009, volume 5710, pages 369-383. Springer, 2009. Google Scholar
  10. 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. Google Scholar
  11. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. CoRR, abs/2104.12695, 2021. URL: https://arxiv.org/abs/2104.12695.
  12. Jérôme Leroux. The Reachability Problem for Petri Nets is Not Primitive Recursive. In Proceedings of FOCS 2021, pages 1241-1252. IEEE, 2021. Google Scholar
  13. Jérôme Leroux, M. Praveen, and Grégoire Sutre. Hyper-Ackermannian bounds for pushdown vector addition systems. In Proceedings of CSL-LICS 2014, pages 63:1-63:10. ACM, 2014. Google Scholar
  14. 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, 2019. Google Scholar
  15. Jérôme Leroux, Grégoire Sutre, and Patrick Totzke. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. In Proceedings of ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 324-336. Springer, 2015. Google Scholar
  16. Richard J. Lipton. The Reachability Problem Requires Exponential Space. Technical report, Yale University, 1976. Google Scholar
  17. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall Series in Automatic Computation. Prentice-Hall, 1967. Google Scholar
  18. Sylvain Schmitz. Complexity Hierarchies beyond Elementary. TOCT, 8(1):3:1-3:36, 2016. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact