Approximating the behaviour of graph transformation systems
In: Graph Transformations : Proceedings of the First International Conference on Graph Transformation , ICGT 2002. - (Lecture Notes in Computer Science ; 2505)
Berlin [u.a.]: Springer (2002), S. 14-29
Buchaufsatz / Kapitel / Fach: Informatik
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 mu-calculus. This is done by embedding our approach in the general framework of abstract interpretation.