Graph Transformations

Abstract

Bigraphical reactive systems are an emerging graphical framework proposed by Milner and others [4,5,2,3] as a unifying theory of process models for distributed, concurrent and ubiquitous computing. A bigraphical reactive system consists of a category of bigraphs (usually generated over a given signature of controls ) and a set of reaction rules . Bigraphs can be seen as representations of the possible configurations of the system, and the reaction rules specify how these configuration can evolve. The advantage of using bigraphical reactive systems is that they provide general results for deriving a labelled transition system automatically from the reaction rules, via the so-called IPO construction . Notably, the bisimulation on this transition system is always a congruence.