Comparing and proving computer system behaviour

Thursday 18 June 2026, 10:30 am
Comparing and Constructing (Co)Inductive Predicates
PhD candidate
R.T.C. Turkenburg
Promotor(s)
dr. J.C. Rot, prof. dr. J.H. Geuvers
Location
Aula

State transition systems are widely used models in computer science. The computers we commonly use, for example, can be viewed as systems with states: the data they contain, and transitions: the changes they make to this data to perform calculations. The aim of this thesis is to develop a better understanding of two aspects of state-transition systems: the effect of modifications to systems on their behaviour; and the comparison of the behaviour of systems. We do this using the theory of coalgebras, in order to develop broadly applicable results. The first part of the thesis presents a new approach to comparing the behaviour of systems (conceived as coalgebras) before and after applying transformations. In doing so, we provide new conditions under which transformations leave the behaviour of systems unchanged. These results are applied to existing transformations of transition systems, and to derive new conditions for important properties of modal logics. The second part delves further into comparing system behaviour, specifically when systems exhibit different behaviour. We provide a new definition of behavioural distinguishability, and show how this can be proven step by step. The main application of this is to systems in which transitions occur with a certain degree of randomness.

Ruben Turkenburg was born in 1997 in York, United Kingdom. He moved to Leiden in 2015 and obtained a double bachelor’s degree in Mathematics and Computer Science from Leiden University in 2019. He then completed a Master’s in Mathematical Foundations of Computer Science at Radboud University between 2019 and 2021. In 2021, he began his PhD at the same university at the Institute for Computing and Information Sciences, in the Software Science group, supervised by Dr Jurriaan Rot.