Deriving bisimulation congruences in the DPO approach to graph rewriting. Long version
Files
Date
2004
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
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
natureand 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.