My main interests are logic, games and automata, in particular in the context of verification and complexity. I specialise in all things parity: parity games, parity automata on words and trees, and, of course, the modal $\mu$ calculus.
I am particularly interested in methods to ensure the correctness of reactive systems
A reactive system is a system embedded in an environment with which it interacts continuously, but that it does not control, for example involving users, other programs or the physical environment. Such systems occur routinely within vehicles, mobile devices, as well as in industrial processes. Identifying bugs early is crucial: in the case of widely deployed hardware, late fixes are expensive while in safety-critical systems they are potentially fatal. Methods to ensure the correctness of reactive systems must be able to handle infinite computations as well as the unpredictable interactions of the system with its environment, which could be controlled by malicious programs or users.
In my research, I focus on two types of specifications: branching time properties, which can describe the state-space of a system, for example,
recovery is always possible after a failure
and linear time properties, that is, properties of individual executions, such as
every request is eventually followed by a response.
The modal $\mu$ calculus is a widely studied verification logic, which is expressive enough to subsume most modal and temporal logics used by practitioners, yet has reasonable algorithmic properties. In my work, I have mostly studied properties expressible in the branching-time and linear-time variants of this logic, known as regular languages over infinite trees and infinite words respectively. In some contexts it is usual to work on automata rather than logic.
Model Checking
The model-checking problem asks whether a given system model satisfied the specification. The exact complexity of the model-checking problem for the modal $\mu$ calculus is a long-standing open problem. A breakthrough occurred in the last couple of years during which several quasipolynomial algorithms have been found. I describe my contribution to these developments, including an independent quasipolynomial algorithm, in the Parity Game section.
Runtime Monitoring
When model-checking is not feasible, either because of its computational cost or because the model is not available, runtime monitoring provides a best-effort alternative. The idea is that a monitor analyses the execution of a system as it happens instead of the system’s state-space. While it is computationally easier than model-checking, runtime monitoring does not provide the same completeness guarantees. Exactly what guarantees runtime monitoring can provide depends on the specification. I describe my contribution to establishing rigorous mathematical foundations for runtime monitoring in the Monitorability section.
Specification Formalisms
The feasibility of the above techniques, as well as of reactive synthesis, depends on how specifications are expressed. Some formalisms have better algorithmic properties, while others allow for more succinct representation. In order to develop effective verification and synthesis strategies, it is important to understand these trade-offs and be able to identify when specifications can be rewritten in a more suitable formalism. The Automata Transformations sections discusses size trade-offs between different types of automata; the Good-for-Games section is about automata with good compositional properties, suitable in particular for synthesis; the Modal $\mu$ Index Problem section talks about one of my favourite open problems.