Ackermannian Completion of Separators

Vector addition systems (VAS for short), or equivalently vector addition systems with states, or Petri nets are a long established model of concurrency with extensive applications in modeling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem is reachability: whether from a given initial configuration there exists a sequence of valid execution steps that reaches a given final configuration. The complexity of the problem has remained unsettled since the 1960 s, and was recently proved to be Ackermannian-complete. In 2009, we proved that the reachability problem can be decided with a simple algorithm by observing that negative instances of the reachability problem can be witnessed by partitioning the set configurations into semilinear sets called complete separators. Since we can decide in elementary time if a pair of semilinear sets denotes a complete separator, the size of such a witness is Ackermannian in the worst case. In this paper, we show how recent results about the reachability problem can be combined to derive a matching upper-bound, i.e. for every negative instance of the reachability problem, we can effectively compute in Ackermannian time a complete separator witnessing that property.