Observational Equivalence for Synchronized Graph Rewriting with Mobility
In: Proceedings of the 4th International Symposium of Theoretical Aspects of Computer Software, TACS 2001. - (Lecture Notes in Computer Science ; 2215)
Berlin [u.a.]: Springer (2001), S. 145-164
Buchaufsatz / Kapitel / Fach: Informatik
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.