Modelling Concurrent Computations: from Contextual Petri Nets to Graph Grammars

Graph grammars (or graph transformation systems), originally introduced as a generalization of string grammars, can be seen as a powerful formalism for the specification of concurrent and distributed systems, which properly extends Petri nets. The idea is that the state of a distributed system can be naturally represented (at a suitable level of abstraction) as a graph and local state transformations can be expressed as production applications. With the aim of consolidating the foundations of the concurrency theory for graph transformation systems, the thesis extends to this more general setting some fundamental approaches to the semantics coming from Petri net theory. More specifically, focusing on the so-called double pushout (DPO) algebraic approach to graph rewriting, the thesis provides graph transformation systems with truly concurrent semantics based on (concatenable) processes and on a Winskel's style unfolding construction, as well as with more abstract semantics based on event structures and domains. The first part of the thesis studies two generalizations of Petri nets, already known in the literature, which reveal a close relationship with graph transformation systems, namely contextual nets (also called nets with read, activator or test arcs) and inhibitor nets (or nets with inhibitor arcs). Extending Winskel's seminal work on safe nets, the truly concurrent semantics of contextual nets is given via a chain of coreflections leading from the category of contextual nets to the category of finitary coherent prime algebraic domains. A basic role is played by asymmetric event structures, which generalize prime event structures by allowing a non-symmetric conflict relation. The work is then generalized to inhibitor nets, where, due to the non-monotonicity of the enabling, the causal structure of computations is far more complex, and a new, very general, notion of event structure, called inhibitor event structure, is needed to faithfully describe them. The second part of the thesis, relying on the conceptual basis drawn in the first part, focuses on graph grammars. Inhibitor event structures turn out to be expressive enough to model graph grammar computations, and the theory developed for contextual and inhibitor nets, comprising the unfolding and the (concatenable) process semantics, can be lifted to graph grammars. The developed semantics is shown to to be consistent also with the classical theory of concurrency for DPO graph grammars relying on shift-equivalence.