Unfolding-Based Verification for Graph Transformation Systems

The unfolding semantics of graph transformation systems can represent a basis for their formal verification. For general, possibly infinite-state, graph transformation systems one can construct finite under- and over- approximations of the (infinite) unfolding, with arbitrary accuracy. Such approximations can be used to check properties of a graph transformation system, like safety and liveness properties, expressed in suitable fragments of the μ-calculus. For finite-state graph transformation systems, a variant of McMillan's approach (originally developed for Petri nets) allows us to single out a finite under-approximation which is a so-called complete prefix of the unfolding, i.e., which provides an "exact" representation of the behaviour the original system as far as reachable states are concerned. Some problems related to the constructive definition of the prefix are discussed.