An Algebra of Graph Derivations Using Finite (co-) Limit Double Theories

Graph transformation systems have been introduced for the formal specication of software systems. States are thereby modeled as graphs, and computations as graph derivations according to the rules of the specication. Operations on graph derivations provide means to reason about the distribution and composition of computations. In this paper we discuss the development of an algebra of graph derivations as a descriptive model of graph transformation systems. For that purpose we use a categorical three level approach for the construction of models of computations based on structured transition systems. Categorically the algebra of graph derivations can then be characterized as a free double category with nite horizontal colimits. One of the main objectives of this paper is to show how we used algebraic techniques for the development of this formal model, in particular to obtain a clear and well structured theory. Thus it may be seen as a case study in theory design and its support by algebraic development techniques.