Integrating the Specification Techniques of Graph Transformation and Temporal Logic

The aim of this paper is an integration of graph grammars with different kinds of behavioural constraints, in particular with temporal logic constraints. Since the usual algebraic semantics of graph transformation systems is not able to express constrained behaviour we introduce - in analogy to other approaches - a coalgebraic semantics which associates with each system a category of models (deterministic transition systems). Such category has a final object, which includes all finite and infinite transition sequences. The coalgebraic framework makes it possible to introduce a general notion of `logic of behavioural constraints'. Instances include, for example, graphical consistency constraints and temporal logic constraints. We show that the considered semantics can be restricted to a final coalgebra semantics for systems with behavioural constraints. This result can be instantiated in order to obtain a final coalgebra semantics for graph grammars with temporal logic constraints