Algorithmic Comparison of Stochastic Systems

Computer systems are woven into almost every aspect of modern life, from aircraft and medical devices to the software that underpins transport, communication, and industry. As these systems grow ever more complex, their correctness and performance can no longer be assessed reliably by hand. Formal verification addresses this challenge by using mathematical and algorithmic methods to analyse systems automatically. This project focuses on the formal verification of probabilistic systems, whose behaviour involves randomness, whether through randomised algorithms or through uncertain and stochastic environments.

The first aim of the project is to strengthen one of the central foundations of current probabilistic verification tools: probabilistic bisimilarity. This notion is crucial for combating the state-space explosion problem, since it allows verification tools to reduce large models by merging states that are behaviourally equivalent. Yet existing equivalence notions can be fragile: even very small changes in probabilities may produce disproportionately large changes in behaviour, potentially undermining the reliability of verification results, especially when parts of a system are only approximately known. The project therefore seeks robust new forms of probabilistic bisimilarity that preserve the practical benefits of minimisation while making verification results more stable and trustworthy.

The second aim is to develop broader and more powerful methods for comparing probabilistic systems. This includes bringing ideas from dynamical systems theory, such as Lyapunov exponents, into algorithmic verification in order to better capture how behavioural differences evolve over time, with potential applications to diagnosability and privacy verification. The project will also design new algorithms that can handle much richer classes of systems, including those with infinitely many states, continuous observations, and more general forms of nondeterminism. In the longer term, this research aims to extend the foundations of probabilistic verification and enable a new generation of more expressive, reliable, and widely applicable verification tools.