Technical Report TR-2004-01

BibliographyEhrig, Hartmut; König, Barbara: Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting (Long Version).
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Technical Report Computer Science No. 2004/01.
30 pages, english.
CR-SchemaF.3.2 (Semantics of Programming Languages)
F.4.2 (Grammars and Other Rewriting Systems)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
G.2.2 (Discrete Mathematics Graph Theory)
Keywordsgraph rewriting; graph transformation; bisimulation; transition systems
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 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.

Full text and
other links
PDF (1084994 Bytes)
PostScript (1833220 Bytes)
Veröffentlichungen der Abteilung SZS
ContactE-Mail an koenigba@fmi.uni-stuttgart.de
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Software Reliability and Security
Entry dateFebruary 27, 2004
New Report   New Article   New Monograph   Computer Science