Geometry of Reachability sets of Vector Addition Systems

TL;DR

This paper advances the geometric understanding of Vector Addition System reachability sets by providing a finite, effective decomposition into well-structured components, enabling new decision procedures for semilinearity.

Contribution

It introduces a finite, effective decomposition of VAS reachability sets into almost hybridlinear sets, facilitating the first new algorithm for semilinearity since 1990.

Findings

Decomposition of reachability sets into disjoint almost hybridlinear sets.

Effective computability of the decomposition.

Decidability of semilinearity for VAS reachability sets.

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