Embracing Uncertainty in Verification and Control

Thom Badings started his career studying industrial engineering, then changed to a PhD in computer science at Radboud University in Nijmegen, the Netherlands, where he was supervised by Nils Jansen and Marielle Stoelinga. For his dissertation work on the intersection of verification, control theory, and AI, he has received various awards. After his PhD, he moved for a postdoc to Oxford and recently started a new chapter as a postdoc at RWTH Aachen University. On the occasion of receiving this year’s ETAPS dissertation award, we interviewed Thom.

Can you tell us what your thesis is about?

My thesis develops algorithms that provide guarantees on the behavior of systems operating under uncertainty. Think about autonomous systems like warehouse robots and drones, but also models for predicting when a production machine will fail. Markov models are a standard state-based formalism to model the behavior of such systems. The traditional analysis of these models assumes that the transition dynamics are known exactly, but this assumption almost never holds in reality. That tension fascinated me, so my thesis develops verification techniques for Markov models that are robust against such uncertainty.

To capture uncertainty, I built on parametric Markov models, where transition probabilities are symbolic expressions over parameters. This model is then equipped with a model of the parameter uncertainty: either an uncertainty set or a probability distribution over parameters. The set-based view enables robust reasoning (“is the specification satisfied for all valuations?”), while the distributional view allows probabilistic reasoning (“what is the probability of sampling a valuation that violates the specification?”).

My thesis then develops verification and synthesis algorithms over different variations of such models. For example, we construct abstractions with sound error bounds and synthesize correct-by-construction control policies against temporal logic specifications. The result is a sound and automated pipeline yielding provably safe policies under uncertainty. What sets it apart from many approaches in control is that we explicitly do not abstract away from the uncertainty, but develop methods that embrace it.

Your background may be different from many other PhD students in formal verification. Can you tell us about the transition from your studies to your PhD?

I studied Industrial Engineering and Management at the University of Groningen in the Netherlands, specializing in so-called smart systems in control and automation. After graduating, I wasn’t sure whether to pursue a PhD. I had enjoyed the research for writing my Master’s thesis, but I didn’t feel confident enough to commit to four years on a single topic. In hindsight, I didn’t realize how fluid a PhD really is: your topic isn’t set in stone from the outset. After a short period in industry, I changed my mind. As I had moved to Nijmegen, it was natural to also look for opportunities there, noting however that there is no engineering department. Luckily, Nils Jansen—who became one of my PhD advisors—was looking for a PhD student with a background in control theory. In the end, the switch from engineering to computer science worked out really well.

My PhD project was part of PrimaVera, a consortium on the topic of predictive maintenance. Maintenance is a key concern in keeping systems online, and the degradation process is a highly nonlinear and complex process. A background in control theory helps to get a grasp on these complex dynamics. On the other hand, computing the probability that a system reaches a bad state is a typical verification problem. However, in maintenance there is a lot of uncertainty, e.g., about the quality of components. Being a consortium member made me realize two things: first, that predictive maintenance is a hard problem that industrial partners haven’t solved, and second, that there is also a lot of research to be done in that area.

You work in verification and control; what’s your perspective on these areas?

Formal verification and control theory both have a long history of analyzing Markov models and synthesizing control policies for them, but classically, they approach this from quite different angles. Control theory typically uses complex, nonlinear dynamical models but focuses on relatively simple objectives such as stability. Formal verification, by contrast, uses temporal logics to specify complex behavior, but the underlying models are typically finite-state machines. Many modern systems demand both complex models and complex specifications. A large part of my thesis sits at this intersection, where I develop methods for the automated synthesis of control policies for discrete-time stochastic dynamical systems.

The communities also differ quite notably, with a journal culture in control theory and a conference culture in verification. Sitting in the audience, you will immediately realize if you’re attending a formal methods or control conference. Many things differ: how we write a paper, how we approach solving a problem, and so on. That makes it interesting but also challenging. In Aachen, I am excited to continue being in the middle of both communities, working with both Joost-Pieter Katoen in formal methods, and Sebastian Trimpe in learning-based control.

Besides the research, what are the highlights of your PhD?

That’s a tough question, as I’ve had many great moments throughout these four years. I’ve had the privilege of traveling to many conferences and workshops, and to meet amazing people from all around the world. One of the highlights was my research stay in the summer of 2024 with Mykel Kochenderfer at Stanford University, both in terms of research and in terms of sunshine. Besides these trips, the interdisciplinary collaboration is what makes research both exciting and rewarding for me. I don’t think you’ll easily find another profession where people are so driven by curiosity and so eager to work together.

What is next?

One direction I’m particularly excited about is statistical verification and synthesis. These techniques can synthesize systems and prove their correctness with statistical guarantees. Statistical techniques generally scale better than their exact counterparts, at the cost of accepting a (typically tiny) probability that the result is incorrect.

My research focus has also shifted more toward the interaction between learning and verification. My PhD work was largely about verifying “static” systems, but many modern systems aren’t static: they learn, adapt, and update over time. This raises new questions: How do we verify systems that are still learning and, more generally, how can we quantify uncertainty in a way that meaningfully supports safe decision-making? I am happy to work on these types of questions in the coming years.