Comparing and Constructing (Co)Inductive Predicates

State-transition systems are extensively used models in computer science. They consist of the states in which a system can exist, and transitions between these states indicating how the state can evolve. The computers which many of us use can be seen as having a state: the data they store, and transitions: the changes they make to these data to perform computations. In this thesis, we aim to better understand two main aspects of these models: how manipulations of systems affect their behaviour; and how to compare the behaviour of systems.

The first part of this thesis gives a new approach for the comparison of the behaviour of systems (modelled as coalgebras) before and after the application of transformations. We apply this framework to give new conditions under which transformations leave observable behaviour unchanged. These conditions are then applied to a number of known system transformations, as well as to obtain new conditions for important properties of (coalgebraic) modal logics.
The second part deals directly with the comparison of system behaviours, specifically when systems exhibit different behaviours. We give a new definition of behavioural apartness, and show how it can be proved inductively. The most important application is in reasoning about differing behaviours between systems with probabilistic transitions.