Baldan, Paolo; König, Barbara:
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
2002Buchaufsatz/Kapitel in SammelwerkInformatik
Approximating the behaviour of graph transformation systems
Baldan, Paolo; König, BarbaraLSF


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.