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.

Bisimulation Equivalences for Graph Grammars

BALDAN, Paolo;
2002

Abstract

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.
Formal and Natural Computing
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10278/11385
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact