
arXiv: 2211.02889
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 simple algorithm for deciding semilinearity of VAS reachability sets, the first one since Hauschildt's 1990 algorithm. As a second corollary, we prove that the complement of a reachability set always contains an infinite linear set.
29 pages, 5 figures, full version of paper in CONCUR 2023
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Formal Languages and Automata Theory (cs.FL), Theory of computation → Formal languages and automata theory, Geometry, Computer Science - Formal Languages and Automata Theory, Petri net, Reachability Set, 004, Logic in Computer Science (cs.LO), Almost hybridlinear, Vector Addition System, Partition, ddc: ddc:004
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Formal Languages and Automata Theory (cs.FL), Theory of computation → Formal languages and automata theory, Geometry, Computer Science - Formal Languages and Automata Theory, Petri net, Reachability Set, 004, Logic in Computer Science (cs.LO), Almost hybridlinear, Vector Addition System, Partition, ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
