Paolo Baldan,
Verification of Graph Transformation Systems
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.