Approximating the behaviour of graph transformation systems

Reference

Paolo Baldan and Barbara König. Approximating the behaviour of graph transformation systems. In Proc. of ICGT '02 (International Conference on Graph Transformation), pages 14–29. Springer-Verlag, 2002. LNCS 2505.

Abstract

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.

Suggested BibTeX entry:

@inproceedings{BK02,
    author = {Paolo Baldan and Barbara K{\"o}nig},
    booktitle = {Proc. of ICGT '02 (International Conference on Graph Transformation)},
    note = {{LNCS} 2505},
    pages = {14--29},
    publisher = {Springer-Verlag},
    title = {Approximating the behaviour of graph transformation systems},
    year = {2002}
}



GZipped PostScript (115 kB)PDF (208 kB)
© University of Duisburg-Essen, Theoretical Computer Science group