Approximating the Behaviour of Graph Transformation Systems

We propose a technique for the analysis of graph transformation systems based on the construction of finite structures approximating the behaviour of such systems with arbitrary accuracy. Following a classical approach, one can construct a chain of finite under-approximations (k-truncations) of the Winskel’s style unfolding of a graph grammar. More interestingly, also a chain of finite over-approximations (k-coverings) of the unfolding can be constructed and both chains converge (in a categorical sense) to the full unfolding. The finite over- and under-approximations can be used to check properties of a graph transformation system, like safety and liveness properties, expressed in (meaningful fragments of) the modal μ-calculus. This is done by embedding our approach in the general framework of abstract interpretation. Research partially supported by the EC TMR Network GETGRATS, by the IST Project AGILE, and by the MURST project TOSCA.