Robust Verification of Stochastic Systems: Guarantees in the Presence of Uncertainty

Intelligent systems play an increasing role in our lives. We therefore need to be sure that these systems are safe and reliable. For example, we might like to prove that a self-driving car will not crash, that a model used to predict the course of an epidemic is accurate or that a machine that produces computer chips will not break down. But how can we formally analyse systems operating in such complex and uncertain conditions?

In this thesis, we try to answer this question by developing new methods to provide guarantees about the behaviour of this kind of complex system. We focus specifically on systems modelled as a so-called Markov model. This is a category of models widely used in control engineering, artificial intelligence (AI), and operations research. Our results show that modelling uncertainty is necessary for correct analysis. We then develop new algorithms for analysing these models with uncertainty, focusing on robustness and (mathematical) correctness. Finally, we apply these algorithms through numerical experiments in several domains, including planning problems for autonomous drones and models for predictive maintenance. All in all, our techniques can be used to provide guarantees about the behaviour of models with uncertainty.