Concurrent Derivations as Single Pushout Graph Grammar Processes
Martin Korff, Leila Ribeiro · Electronic Notes in Theoretical Computer Science · 1995
Algebraic graph transformations visually support intuition, have a strong theoretical basis, and provide a formal, implementation independent basis for the description of discretely evolving computational systems and their formal and tractable analysis. Graph grammar models of concurrent systems (petri nets, actor systems) have inspired corresponding semantics developments. Recently this led to the introduction of partial orders of concurrent derivations (concurrent computations). A concurrent derivation (CDer) abstracts from the (sequential) order of rule applications in the sequential derivation and thus can be considered as a concurrent process. Complementary, a morphism between two concurrent derivations expresses that the first is a computational approximation of the second. In this paper we newly introduce non-deterministic concurrent derivations (CTrees) as classes of concurrently equivalent sequential derivation trees. Due to the fact that also infinite computations are represented by CTrees, the category of all CTrees of a given graph grammar has a final object (the concurrent counterpart of the whole sequential tree of the given grammar) which is approximated by all other CTrees. We show that (syntactical) morphisms between two graph grammars induce corresponding adjunction between the corresponding (semantic) categories of CDers and CTrees respectively.