(1) Dipartimento di Informatica, Università Ca' Foscari di Venezia, Italia. (2) Dipartimento di Informatica, Università di Pisa, Italia.
Abstract:
Several applications of graph rewriting systems (notably,
some encodings of calculi with name passing) require rules which,
besides deleting and generating graph items, are able to coalesce
some parts of the graph. This latter feature forbids the
development of a satisfactory concurrent semantics for rewrites
(intended as a partial order description of the steps in a
computation). This paper proposes the use of graphs with
equivalences, i.e., (typed hyper-) graphs equipped with an
equivalence over nodes, for the analysis of distributed systems. The
formalism is amenable to the tools of the double-pushout approach to
rewriting, including the theoretical results associated to its
concurrent features. The formalism is tested against the encoding
of a simple calculus with name mobility, namely the solo
calculus.