With the advent of mobile and ubiquitous computing, modern software and computer systems are frequently characterised by a high level of dynamicity. Features such as flexible topologies, the dynamic creation and deletion of objects, and an infinite-state space make them very hard to analyse and verify. In this context, graph transformation systems (GTSs) emerge as an expressive specification formalism for concurrent, distributed and mobile systems, generalising another classical model of concurrency, namely Petri nets. While the semantic theory of GTSs is relatively well-understood, the problem of developing automatic verification techniques for GTSs is still a stimulating and promising research direction.

In this presentation we outline a framework for the verification of infinite and finite-state GTSs based on their unfolding semantics. For general, possibly infinite-state, GTSs one can construct finite under- and over- approximations of the (infinite) unfolding, with arbitrary accuracy. Such approximations can be used to check behavioural properties of a GTS, expressed in a suitable temporal graph logic. For finite-state GTSs, we propose a variant of McMillan's complete prefix approach (originally developed for Petri nets), discussing some issues related to the construction of the prefix and its use.