Document Open Access Logo

Geometry of Reachability Sets of Vector Addition Systems

Authors Roland Guttenberg , Mikhail Raskin , Javier Esparza

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.6.pdf
  • Filesize: 0.8 MB
  • 16 pages

Document Identifiers

Author Details

Roland Guttenberg
  • Technical University of Munich, Germany
Mikhail Raskin
  • LaBRI, University of Bordeaux, France
Javier Esparza
  • Technical University of Munich, Germany

Funding

The project has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 787367.

Cite AsGet BibTex

Roland Guttenberg, Mikhail Raskin, and Javier Esparza. Geometry of Reachability Sets of Vector Addition Systems. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.6

Abstract

Vector Addition Systems (VAS), aka Petri nets, are a popular model of concurrency. The reachability set of a VAS is the set of configurations reachable from the initial configuration. Leroux has studied the geometric properties of VAS reachability sets, and used them to derive decision procedures for important analysis problems. In this paper we continue the geometric study of reachability sets. We show that every reachability set admits a finite decomposition into disjoint almost hybridlinear sets enjoying nice geometric properties. Further, we prove that the decomposition of the reachability set of a given VAS is effectively computable. As a corollary, we derive a new proof of Hauschildt’s 1990 result showing the decidability of the question whether the reachability set of a given VAS is semilinear. As a second corollary, we prove that the complement of a reachability set, if it is infinite, always contains an infinite linear set.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Vector Addition System
  • Petri net
  • Reachability Set
  • Almost hybridlinear
  • Partition
  • Geometry

Metrics

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

Related Versions

References

  1. Dmitry Chistikov and Christoph Haase. The Taming of the Semi-Linear Set. In ICALP, volume 55 of LIPIcs, pages 128:1-128:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  2. 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. Google Scholar
  3. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-complete. In FOCS, pages 1229-1240. IEEE, 2021. Google Scholar
  4. Seymour Ginsburg and Edwin H Spanier. Bounded ALGOL-like Languages. SDC, 1963. Google Scholar
  5. Roland Guttenberg, Mikhail Raskin, and Javier Esparza. Geometry of Reachability Sets of Vector Addition Systems, 2023. URL: https://arxiv.org/abs/2211.02889.
  6. Dirk Hauschildt. Semilinearity of the Reachability Set is decidable for Petri Nets. PhD thesis, University of Hamburg, Germany, 1990. Google Scholar
  7. Petr Jancar, Jérôme Leroux, and Grégoire Sutre. Co-Finiteness and Co-Emptiness of Reachability Sets in Vector Addition Systems with States. Fundam. Informaticae, 169(1-2):123-150, 2019. Google Scholar
  8. S. Rao Kosaraju. Decidability of Reachability in Vector Addition Systems. In STOC, pages 267-281. ACM, 1982. Google Scholar
  9. Jean-Luc Lambert. A Structure to Decide Reachability in Petri Nets. Theor. Comput. Sci., 99(1):79-104, 1992. Google Scholar
  10. Jérôme Leroux. The General Vector Addition System Reachability Problem by Presburger Inductive Invariants. In LICS, pages 4-13. IEEE Computer Society, 2009. Google Scholar
  11. Jérôme Leroux. Vector Addition System Reachability Problem: A Short Self-Contained Proof. In LATA, volume 6638 of Lecture Notes in Computer Science, pages 41-64. Springer, 2011. Google Scholar
  12. Jérôme Leroux. Vector Addition Systems Reachability Problem (A Simpler Solution). In Turing-100, volume 10 of EPiC Series in Computing, pages 214-228. EasyChair, 2012. Google Scholar
  13. Jérôme Leroux. Presburger Vector Addition Systems. In LICS, pages 23-32. IEEE Computer Society, 2013. URL: https://hal.science/hal-00780462v2.
  14. Jérôme Leroux. The Reachability Problem for Petri Nets is not Primitive Recursive. In FOCS, pages 1241-1252. IEEE, 2021. Google Scholar
  15. Jérôme Leroux and Sylvain Schmitz. Demystifying Reachability in Vector Addition Systems. In LICS, pages 56-67. IEEE Computer Society, 2015. Google Scholar
  16. 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. Google Scholar
  17. Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In STOC, pages 238-246. ACM, 1981. Google Scholar
  18. Danny Nguyen and Igor Pak. Enumerating Projections of Integer Points in Unbounded Polyhedra. SIAM J. Discret. Math., 32(2):986-1002, 2018. Google Scholar
  19. Alexander Schrijver. Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, 1999. Google Scholar
  20. Kevin Woods. Presburger Arithmetic, Rational Generating Functions, and Quasi-Polynomials. J. Symb. Log., 80(2):433-449, 2015. 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