zbMATH — the first resource for mathematics

Model checking coverability graphs of vector addition systems. (English) Zbl 1343.68152
Murlak, Filip (ed.) et al., Mathematical foundations of computer science 2011. 36th international symposium, MFCS 2011, Warsaw, Poland, August 22–26, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22992-3/pbk). Lecture Notes in Computer Science 6907, 108-119 (2011).
Summary: 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.
For the entire collection see [Zbl 1219.68020].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI