A model for distributed systems based on graph rewriting

A model for distributed systems based on graph rewriting
P. Degano and U. Montanari
J ACM 34(2):411-449

I was pointed to this paper by Eric Griffis, a student who will be visiting this summer as part of a NSF PIRE program.  Eric is interested in graph rewriting and distributed systems.

The paper presents a generic computational model for concurrent/distributed computation based on graphs (really, hypergraphs).  The "nodes" of the hypergraphs correspond to channels, and the "hyperedges" correspond to either events (interactions in the past) or processes (placeholders for possible interactions in the future).  Thus, the graph as a whole describes both the past (previous events), present (frontier of active processes that can make progress now) and future (processes whose progress is blocked by other processes).

The execution behavior of the system can be specified using graph rewriting.  Production rules are specified as mappings from nonterminal labels to graph fragments.  Rewrite rules are obtained from these by merging concurrent events.  The meaning of a system (that possibly runs forever) is defined by setting up a ultrametric space on graph states and taking limits.  (This is a large oversimplification.)

Graph-based techniques for describing concurrent/distributed systems are widespread - for example, scientific or business workflow systems (or older dataflow computation models) are based on graphs, with the nodes representing processes or functions and edges representing wires or streams. On the other hand, graphs (for example, Milner's bigraphs, or Harel's statecharts or higraphs) are also widely used as visual formalisms for studying distributed systems.  Looking at the list of other work that cites Degano's and Montanari's paper, it seems that most of the influence of this work has been on graph grammars/transformation.

I find two things particularly interesting about this model:

1. the capability to describe different parts with "productions", which are then composed with each other to form "rewrite rules"; the latter can express multiple concurrent operations taking place in one step.  It seems that this "fusion" behavior has been explored in subsequent work; it seems closely related to (maybe the same as?) pushout-based techniques for graph transformation.
2. the presence in the same model of past (event history/provenance), present (current computational state) and future (not-yet-executed processes).  Often one only has the present/future part.

On the other hand, I didn't find the running examples particularly easy to absorb.  This may be due to the unfamiliarity of the notation.

It might be interesting to translate this formalism to something like bigraphs (which seem sufficiently expressive).  A longer-term goal might be to look at how to instrument the semantics of different concurrency calculi with an explicit "past", which would hopefully align fairly well with notions of provenance being explored in other communities (OPM, W3C PROV).  Some recent work by Dezani-Ciancaglini et al. and earlier by Souliah et al. has started to investigate provenance from a concurrency theory perspective.  However, it's still not clear to me what the design goals/correctness criteria for provenance tracking in such a system should be.