TY - GEN

T1 - Geometry of Reachability Sets of Vector Addition Systems

AU - Guttenberg, Roland

AU - Raskin, Mikhail

AU - Esparza, Javier

N1 - Publisher Copyright:
© 2023 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.

PY - 2023/9

Y1 - 2023/9

N2 - 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.

AB - 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.

KW - Almost hybridlinear

KW - Geometry

KW - Partition

KW - Petri net

KW - Reachability Set

KW - Vector Addition System

UR - http://www.scopus.com/inward/record.url?scp=85172366753&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CONCUR.2023.6

DO - 10.4230/LIPIcs.CONCUR.2023.6

M3 - Conference contribution

AN - SCOPUS:85172366753

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 34th International Conference on Concurrency Theory, CONCUR 2023

A2 - Perez, Guillermo A.

A2 - Raskin, Jean-Francois

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 34th International Conference on Concurrency Theory, CONCUR 2023

Y2 - 18 September 2023 through 23 September 2023

ER -