Geometry of Reachability Sets of Vector Addition Systems
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.
Vector Addition System
Petri net
Reachability Set
Almost hybridlinear
Partition
Geometry
Theory of computation~Formal languages and automata theory
6:1-6:16
Regular Paper
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.
https://arxiv.org/abs/2211.02889
Roland
Guttenberg
Roland Guttenberg
Technical University of Munich, Germany
https://orcid.org/0000-0001-6140-6707
Mikhail
Raskin
Mikhail Raskin
LaBRI, University of Bordeaux, France
https://orcid.org/0000-0002-6660-5673
Javier
Esparza
Javier Esparza
Technical University of Munich, Germany
https://orcid.org/0000-0001-9862-4919
10.4230/LIPIcs.CONCUR.2023.6
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.
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.
Wojciech Czerwinski and Lukasz Orlikowski. Reachability in Vector Addition Systems is Ackermann-complete. In FOCS, pages 1229-1240. IEEE, 2021.
Seymour Ginsburg and Edwin H Spanier. Bounded ALGOL-like Languages. SDC, 1963.
Roland Guttenberg, Mikhail Raskin, and Javier Esparza. Geometry of Reachability Sets of Vector Addition Systems, 2023. URL: https://arxiv.org/abs/2211.02889.
https://arxiv.org/abs/2211.02889
Dirk Hauschildt. Semilinearity of the Reachability Set is decidable for Petri Nets. PhD thesis, University of Hamburg, Germany, 1990.
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.
S. Rao Kosaraju. Decidability of Reachability in Vector Addition Systems. In STOC, pages 267-281. ACM, 1982.
Jean-Luc Lambert. A Structure to Decide Reachability in Petri Nets. Theor. Comput. Sci., 99(1):79-104, 1992.
Jérôme Leroux. The General Vector Addition System Reachability Problem by Presburger Inductive Invariants. In LICS, pages 4-13. IEEE Computer Society, 2009.
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.
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.
Jérôme Leroux. Presburger Vector Addition Systems. In LICS, pages 23-32. IEEE Computer Society, 2013. URL: https://hal.science/hal-00780462v2.
https://hal.science/hal-00780462v2
Jérôme Leroux. The Reachability Problem for Petri Nets is not Primitive Recursive. In FOCS, pages 1241-1252. IEEE, 2021.
Jérôme Leroux and Sylvain Schmitz. Demystifying Reachability in Vector Addition Systems. In LICS, pages 56-67. IEEE Computer Society, 2015.
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.
Ernst W. Mayr. An Algorithm for the General Petri Net Reachability Problem. In STOC, pages 238-246. ACM, 1981.
Danny Nguyen and Igor Pak. Enumerating Projections of Integer Points in Unbounded Polyhedra. SIAM J. Discret. Math., 32(2):986-1002, 2018.
Alexander Schrijver. Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, 1999.
Kevin Woods. Presburger Arithmetic, Rational Generating Functions, and Quasi-Polynomials. J. Symb. Log., 80(2):433-449, 2015.
Roland Guttenberg, Mikhail Raskin, and Javier Esparza
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode