Deriving Process Congruences from Reaction Rules

This thesis is concerned with the development of a theory which, given a formalism with a reduction semantics, allows the derivation of a canonical labelled transition system on which bisimilarity as well as other other equivalences are congruences; provided that the contexts of the formalism form a category which has certain colimits.

We shall begin by extending Leifer and Milner's theory of reactive systems to a 2-categorical setting. This development is motivated by the common situation in which the contexts of a reactive system contain non-trivial algebraic structure with an associated notion of context isomorphism. Forgetting this structure often leads to problems and we shall show that the theory can be extended smoothly, retaining this useful information as well as the congruence theorems.

Technically, the generalisation includes defining the central notion of groupoidal-relative-pushout (GRPO) (categorically: a bipushout in a pseudoslice category), which turns out to provide a suitable generalisation of Leifer and Milner's relative pushout (RPO). The congruence theorems are then reproved in this more general setting. We shall also show how previously introduced alternative solutions to the problem of forgetting the two-dimensional structure can be reduced to the 2-categorical approach.

Secondly, we shall construct GRPOs in settings which are general enough to allow the theory to be applied to useful, previously studied examples. We shall begin by constructing GRPOs in a category whose arrows correspond closely to the contexts a simple process calculus, and extend this construction further to cover the category of bunch contexts, studied previously by Leifer and Milner. The constructions use the structure of extensive categories.

We shall argue that cospans provide an interesting notion of ``generalised contexts''. In an effort to find a natural class of categories which allows the construction of GRPOs in the corresponding cospan bicategory, we shall introduce the class of adhesive categories. As extensive categories have well-behaved coproducts, so adhesive categories have well-behaved pushouts along monomorphisms. Adhesive categories also turn out to be a useful tool in the study and generalisation of the theory of double-pushout graph transformation systems, indeed, such systems have a rich rewriting theory when defined over adhesive categories.

Armed with the theory of adhesive categories, we shall present a construction of GRPOs in input-linear cospan bicategories. As an immediate application, we shall shed light on as well as extend the theory of rewriting via borrowed contexts, due to Ehrig and König. Secondly, we shall examine the implications of the construction for Milner's bigraphs

Abstract: