A model for distributed systems based on graph rewriting

In our model, a graph describes a net of processes communicating through ports and, at the same time, its computation history consisting of a partial ordering of events. Stand-alone evolution of processes is specified by context-free productions. From productions and a basic synchronization mechanism, a set of context-sensitive rewriting rules that models the evolution of processes connected to the same ports can be derived. A computation is a sequence of graphs obtained by successive rewritings. The result of a finite computation is its last graph, whereas the result of an infinite computation is the limit, infinite graph defined through a completion technique based on metric spaces. A result characterizes a concurrent computation, since it abstracts from any particular interleaving of concurrent events, while in the meantime providing information about termination, partial or complete deadlocks, and fairness. Not every result is acceptable, however, but only the computations that produce a result no longer rewritable are successful. Infinite successful computations are shown to coincide with weakly fair computations, and a scheduler yielding all and only such computations is defined.