Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting
In: Proceedings of the 7th International Conference of Foundations of Software Science and Computation Structures, FOSSACS 2004. - (Lecture Notes in Computer Science ; 2987)
Berlin [u.a.]: Springer (2004), S. 151-166
Buchaufsatz / Kapitel / Fach: Informatik
Motivated by recent work on the derivation of labelled transitions and bisimulation congruences from unlabelled reaction rules, we show how to solve this problem in the DPO (double-pushout) approach to graph rewriting. Unlike in previous approaches, we consider graphs as objects, instead of arrows, of the category under consideration. This allows us to present a very simple way of deriving labelled transitions (called rewriting steps with borrowed context) which smoothly integrates with the DPO approach, has a very constructive nature and requires only a minimum of category theory. The core part of this paper is the proof sketch that the bisimilarity based on rewriting with borrowed contexts is a congruence relation.