Document Open Access Logo

The Geometry of Reachability in Continuous Vector Addition Systems with States

Authors Shaull Almagor , Arka Ghosh, Tim Leys , Guillermo A. Pérez

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2023.11.pdf
  • Filesize: 0.81 MB
  • 13 pages

Document Identifiers

Author Details

Shaull Almagor
  • Technion - Israel Institute of Technology, Haifa, Israel
Arka Ghosh
  • University of Warsaw, Poland
Tim Leys
  • University of Antwerp - Flanders Make, Belgium
Guillermo A. Pérez
  • University of Antwerp - Flanders Make, Belgium

Funding

  • Almagor, Shaull: supported by the ISRAEL SCIENCE FOUNDATION (grant No. 989/22).
  • Ghosh, Arka: partially supported by the NCN grant 2019/35/B/ST6/02322.

Acknowledgements

We thank anonymous reviewers for their careful reading of a previous version of this work and for their suggestions that greatly improved the presentation of this paper.

Cite AsGet BibTex

Shaull Almagor, Arka Ghosh, Tim Leys, and Guillermo A. Pérez. The Geometry of Reachability in Continuous Vector Addition Systems with States. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.MFCS.2023.11

Abstract

We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are "almost" Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short so-called linear path schemes suffice as witnesses of reachability in continuous VASS. Then, we give new polynomial-time algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Logic and verification
Keywords
  • Vector addition system with states
  • reachability
  • continuous approximation

Metrics

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

Related Versions

References

  1. 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.
  2. Michael Blondin and Christoph Haase. Logics for continuous reachability in Petri nets and vector addition systems with states. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. Google Scholar
  3. Wojciech Czerwinski, 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.
  4. Wojciech Czerwinski, Slawomir Lasota, Christof Löding, and Radoslaw Piórkowski. New pumping technique for 2-dimensional VASS. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 62:1-62:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.62.
  5. Wojciech Czerwinski, Slawomir Lasota, and Lukasz Orlikowski. Improved lower bounds for reachability in vector addition systems. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 128:1-128:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.128.
  6. Wojciech Czerwinski and Lukasz 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.
  7. René David and Hassane Alla. Discrete, continuous, and hybrid Petri nets, volume 1. Springer, 2010. Google Scholar
  8. Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for two-counter machines with one test and one reset. In Sumit Ganguly and Paritosh K. Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India, volume 122 of LIPIcs, pages 31:1-31:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.31.
  9. Christoph Haase. On the complexity of model checking counter automata. PhD thesis, University of Oxford, UK, 2012. URL: http://ora.ox.ac.uk/objects/uuid:f43bf043-de93-4b5c-826f-88f1bd4c191d.
  10. Christoph Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://doi.org/10.1145/3242953.3242964.
  11. Christoph Haase and Simon Halfon. Integer vector addition systems with states. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings, volume 8762 of Lecture Notes in Computer Science, pages 112-124. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-11439-2_9.
  12. 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.
  13. Richard M Karp. Reducibility among combinatorial problems. In Complexity of computer computations, pages 85-103. Springer, 1972. Google Scholar
  14. 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.
  15. 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.
  16. Jérôme Leroux and Grégoire Sutre. On flatness for 2-dimensional vector addition systems with states. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_26.
  17. Marvin Lee Minsky. Computation. Prentice-Hall Englewood Cliffs, 1967. Google Scholar
  18. Christos H. Papadimitriou and Kenneth Steiglitz. Combinatorial Optimization: Algorithms and Complexity. Prentice-Hall, 1982. Google Scholar
  19. Sylvain Schmitz. The complexity of reachability in vector addition systems. ACM SigLog News, 3(1):4-21, 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 Imprint Privacy Contact