Categories with algebraic structure are well-known as models of concurrent computations for, e.g., formal grammars, Petri nets, and term rewriting. The approach, of obtaining concurrent computations by means of an algebraic construction from a set of rules, can be generalised to graph transformation systems. The resulting computational model, a free double category with finite horizontal colimits, captures the established notion of concurrency of DPO graph transformation.

Such a construction exposes the intrinsic structure of concurrency in graph transformations and provides the basis for defining a temporal logic for concurrent computations. The logic represents a specialisation of van Benthem's arrow logic to categories, extended by spatial connectives like a concurrent composition of computations.

The talk will present the basics of the categorical model and discuss the definition of the logic, its semantics, deduction rules, and potential applications.