Properties of Vector Addition Systems

Abstract

We consider vector addition systems (VAS), a model of asynchronous computation which is equivalent to the Petri net model. Reachability is not known to be decidable for arbitrary VAS. The best known lower bound for the general case is exponential space-hard [14]. We first show that reachability for conflict free nets is NP-hard. Our next result, using a reduction similar to that of Jones 151 for reachability, is a PSPACE-hard lower bound on the complexity of deciding various properties of VAS such as safeness, boundedness and persistence, Since safeness can be decided in polynomial space, this result characterizes the space complexity of this problem. The construction also yields a PSPACE-hard lower bound for persistent nets. The next result is a reduction of persistence to reachability, partially answering a question of Keller [8]. Reachability and boundedness are then proved to be undecidable for the time VAS, introduced by Merlin [9].