Model checking coverability graphs of vector addition systems

Abstract

A large number of properties of a vector addition system-for instance coverability, boundedness, or regularity-can be decided using its coverability graph, by looking for some characteristic pattern. We propose to unify the known exponential-space upper bounds on the complexity of such problems on vector addition systems, by seeing them as instances of the model-checking problem for a suitable extension of computation tree logic, which allows to check for the existence of these patterns. This provides new insights into what constitutes a "coverability-like" property. © 2011 Springer-Verlag GmbH.