Observational Equivalence for Synchronized Graph Rewriting with ...


Barbara König and Ugo Montanari. Observational equivalence for synchronized graph rewriting with mobility. In Proc. of TACS '01, pages 145–164. Springer-Verlag, 2001. LNCS 2215.


We introduce a notion of bisimulation for graph rewriting systems, allowing us to prove observational equivalence for dynamically evolving graphs and networks. We use the framework of synchronized graph rewriting with mobility which we describe in two different, but operationally equivalent ways: on graphs defined as syntactic judgements and by using tile logic. One of the main results of the paper says that bisimilarity for synchronized graph rewriting is a congruence whenever the rewriting rules satisfy the basic source property. Furthermore we introduce an up-to technique simplifying bisimilarity proofs and use it in an example to show the equivalence of a communication network and its specification.

Suggested BibTeX entry:

    author = {Barbara K{\"o}nig and Ugo Montanari},
    booktitle = {Proc. of TACS '01},
    note = {{LNCS} 2215},
    pages = {145--164},
    publisher = {Springer-Verlag},
    title = {Observational Equivalence for Synchronized Graph Rewriting with Mobility},
    year = {2001}

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