A categorical setting for transition systems

Abstract

Transition systems of various "transition types" are used to model various computational phenomena in many aspects of theoretical computer science. A convenient categorical approach is to model transition systems as coalgebras for a monad T. Possible transition types include non-determinism, probability, divergence, or weights in a semiring. There are several interesting notions of morphisms of transition systems—transition preserving functions, functional bisimulations, and relation-based like simulations and bisimulations. This thesis takes the analogy of "simulations as relational morphisms" seriously, and expresses simulations as Kleisli morphisms for a powerset-like monad on the category of non-deterministic transition systems (analogous to the relationship between Rel and Set). This monad is shown to be an instance of a lax distributive law PP -> PP. In a more general setting, we seek to exhibit a correspondence theorem between lax distributive laws ST -> TS and monads on categories of T-transition systems. The simple category of T-coalgebras turns out to be too small, so we introduce a notion of T-actions, which simultaneously generalise T-coalgebras and monoid actions. We frame many well known constructions of transition systems (including the cartesian closed structure, and a notion of graph homotopy) in terms of T-actions.

Date of Award	1 Aug 2023
Original language	English
Awarding Institution	The University of Manchester
Supervisor	Renate Schmidt (Supervisor) & Andrea Schalk (Supervisor)