| The topic of graph grammars originates in the 60's, when it is was mainly viewed as a generalization of Chomsky grammars. The motivation came from a variety of areas, such as pattern recognition, compiler construction, and concurrent systems. In much of the early work, graph grammars were viewed as systems defining a graph language; this view implies that a fixed graph is given that serves as the starting point for the derivations. Later, much of the attention has shifted to situations where a system is used to transform graphs by the application of productions. In this case one refers to them as graph rewriting systems. The aim of this thesis is to provide an overview of the theory of Local Action Systems. These are a type of graph rewriting systems based on node rewriting and embedding. The emphasis is on the process semantics of Local Action Systems. The semantic theory is based on the notion of a process which is known to be a useful tool for describing concurrency. The thesis is divided into three parts.; In the first part of the thesis, the basic definitions concerning Local Action Systems and their process semantics are given. Then the properties of this semantics are investigated; in particular the algebraic properties of the embedding mechanism and the issue of compositionality are considered. One focuses on the analysis of individual processes and on the way one can deal with the additional complexity of incorporating an embedding mechanism. Several versions of a compositional semantics for Local Action Systems are considered.; The second part of the thesis explores the value of graph rewriting, and more in particular graph rewriting processes, for the verification of concurrent systems. It has been widely recognized that the verification of concurrent systems is considerably more difficult than that of sequential ones. Therefore there is a potential use for new conceptual tools supporting this task, in particular if they support compositional reasoning, where separate proofs for system components can be combined to a proof of a global system property. A distributed shortest path algorithm and the Alternating Bit ( AB) protocol are considered as test cases. In the correctness proof of the shortest path algorithm one focuses on applying the results about the algebraic properties of the embedding mechanism. The aim of the section concerning the Alternating Bit protocol is to give a compositional proof.; In the last part of the thesis it is demonstrated that Local Action Systems may be viewed as a unifying framework for a number of other models of concurrent computation: for several versions of Petri Nets, as well as for several types of embedding-based graph rewriting it is shown that they can be modeled as Local Action Systems. |
