Verifying a Behavioural Logic
for Graph Transformation Systems
Paolo Baldan(1) - Andrea Corradini(2) - Barbara König(3) -
Bernhard König(4)
(1) Dipartimento di Informatica, Università
Ca' Foscari di Venezia, Italy
(2) Dipartimento di Informatica, Università di Pisa, Italy.
(3) Institut für Informatik, Technische Universität
München, Germany
(4) Department of Mathematics,
University of California, Irvine, USA
Abstract:
We propose a framework for the verification of behavioural
properties of systems modelled as graph transformation systems. The
properties can be expressed in a temporal logic which is basically a
mu-calculus where the state predicates are formulae of a monadic
second order logic, describing graph properties. The verification
technique relies on an algorithm for the construction of finite
over-approximations of the unfolding of a graph transformation system.