Algorithmic Comparison of Stochastic Systems

Computers are everywhere: they are embedded in airplanes and medical devices, among many other systems. We depend on them, and their failure can have catastrophic consequences. Computer systems have become far too complex to analyse by hand.

However, their correctness and performance can be systematically analysed with the help of specialised programs. Computer-aided formal verification is based on this idea. Research in this field has led among others to four Turing awards (the "Nobel prize of computing") to date.

The economic importance of formal verification can be illustrated by prominent software errors, such as Tesla's recall of almost 12,000 vehicles in 2021 after drivers had reported that spurious collision threats had activated the automatic emergency braking system, bringing their cars to a sudden stop.

This project focuses on computer-aided verification of probabilistic systems. Such systems involve an element of randomness, either because they run randomised algorithms (which can be more efficient than deterministic algorithms) or because their usage is stochastic.

Specialised tools, such as Prism and Storm, for automatically verifying probabilistic systems are underpinned by mathematical proofs. Thus, their algorithms are based on foundational areas of computer science and mathematics, including computational complexity, automata theory, design and analysis of efficient data structures and algorithms, logics, linear algebra, topology and probability theory. Conducting this research project requires substantial knowledge and background in these fields.

Our goal is to advance the foundations of computer-aided verification of probabilistic systems in two directions.

Make a bedrock of current tools, namely probabilistic bisimilarity, more robust in order to increase the reliability of verification results. Develop much more broadly applicable algorithms for comparing probabilistic systems.

Item 1 is connected to one of the most pressing problems in formal verification: the so-called state-space explosion problem arises because even a small system can have a huge number of states. Therefore, efficient tools need to minimise the state space. This is done by representing equivalent states only once, where the technical meaning of "equivalent" is "probabilistically bisimilar".

Probabilistically bisimilar states behave essentially in the same way, and thus can be "merged" to speed up verification. However, the problem is that equivalent states can quickly become "very" inequivalent, where "very" can be formalised using a notion of distance. Even the tiniest change in the probabilistic behaviour of a component can radically change the overall system behaviour, rendering verification results potentially unreliable.

The problem is exacerbated when some system components are not known exactly. We believe the success of minimisation via probabilistic bisimilarity, on which successful tools rely, has turned into a liability. We want to develop robust notions of probabilistic bisimilarity that avoid this problem.

Item 2 takes a different angle on comparing probabilistic systems. The aforementioned notion of distance does not always adequately describe the speed of behavioural divergence. We will connect the theory of Lyapunov exponents from dynamical systems theory with the algorithmic analysis of probabilistic systems and expect impact on system diagnosability and the verification of privacy.

Furthermore, we will devise novel algorithms for comparing probabilistic systems by allowing infinitely many states, continuous observable behaviour and more classes of nondeterminism. Extending the foundations of probabilistic verification in this way might lead, at least in the long run, to the development of much more powerful and more widely applicable verification tools.