Bisimulation Equivalences for Graph Grammars

Along the years the concurrent behaviour of graph grammars has been widely investigated, and, in particular, several classical approaches to the semantics of Petri nets have been extended to graph grammars. Most of the existing semantics for graph grammars provide a (possibly concurrent) operational model of computation, while little interest has been devoted to the definition of abstract observational semantics. The aim of this paper is to introduce and study a behavioural equivalence over graphg rammars, inspired by the classical history preserving bisimulation. Several choices are conceivable according to the kind of concurrent observation one is interested in. We concentrate on the basic case where the concurrent nature of a graph grammar computation is described by means of a prime event structure. As it happens for Petri nets, history preserving bisimulation can be studied in the general framework of causal automata — a variation of ordinary automata introduced to deal withh istory dependent formalisms. In particular, we prove that history preserving bisimulation is decidable for finite-state graph grammars, by showing how the problem can be reduced to deciding the equivalence of finite causal automata.