The Ackermann Award 2025

Linear dynamical systems are mathematical models widely used in engineering and science to describe systems that evolve over time. For example, they can be used to model simple while-loops in program analysis, or to model stochastic processes in probabilistic model checking. A discrete-time linear dynamical system is given by a matrix $M\in {𝒬}^{d\times d}$ and a starting point $s\in {𝒬}^d$. The trajectory of $(M,s)$ (or orbit) is the sequence ${(M^{n}s)}_{n\in N}$.

Despite their apparent simplicity, many reachability questions concerning linear dynamical systems have remained open for decades. The thesis addresses the Model-Checking Problem, which consists of deciding whether the trajectory of a given linear dynamical system satisfies a specification written as a monadic second-order formula. It generalises the reachability problem and can be alternatively defined using Büchi automata, as in this thesis.

One of the main contributions of the thesis is a novel framework in which decidability of various non-trivial classes of the Model-Checking Problem can be established. Previously, decidability was only known for restricted classes of specifications. The analysis of decidability results using the new approach advocated in the thesis shows that any significant generalisation would entail major mathematical breakthroughs in number theory. These results delineate a sharp boundary for the subclasses of the Model-Checking Problem for which decidability can be proven using contemporary mathematical tools. The thesis is remarkable for its use of deep ideas from algebraic number theory and Diophantine approximation.

In addition, the thesis explores the use of deep model-theoretic tools (in particular o-minimality in the theory of real exponentiation) to obtain decidability results for topological and robust variants of the reachability problem, relying on continuous abstractions of discrete orbits. In particular, the thesis shows that the reachability problem is decidable if we have access to an arbitrarily small control input at each step. This approach opens new directions to address verification problems for other fundamental classes of models, including continuous-time linear dynamical systems and simple forms of non-linear systems.

Toghrul Karimov carried out his PhD studies at Saarland University, under the supervision of Joël Ouaknine, from 2019 to 2024. During his PhD he (co)-authored 16 conference papers, including POPL 2021 and 2022, LICS 2023, 2024 and 2025, and ICALP 2025, and a journal article in Theoretical Computer Science. He obtained a Distinguished Paper Award at LICS 2024 and ACM SIGBED Best Paper Award at HSCC 2024. Currently he is a post-doctoral researcher at the Max Planck Institute for Software Systems, Saarbrücken.

The model checking problem in graph theory consists of deciding whether a given graph $G$ satisfies a given first-order logic formula $\varphi$. A naive branching algorithm solves the problem in time $n^{O(|\varphi |)}$, where $n$ is the number of vertices of $G$ and $|\varphi |$ is the size of $\varphi$. Under standard complexity assumptions, a polynomial in $n$ whose exponent depends on the size of $\varphi$ is unavoidable. However, in practice the classes of interest have additional structure that can be exploited to obtain faster algorithms. The model checking problem is fixed-parameter tractable on a graph class $C$ if it can be solved in time $f(|\varphi |)\cdot n^c$ for some (arbitrarily fast-growing) function $f$ and a constant $c$, on every $n$-vertex graph from $C$ and formula $\varphi$. Well-known examples are the class of planar graphs and more generally the nowhere dense graph classes from sparsity theory. The thesis addresses the open question of characterising graph classes that admit fixed-parameter tractable model checking. It focuses on two important cases: the monadically stable and the monadically dependent graph classes. A graph class is monadically stable if it does not transduce the class of all half-graphs. For example, the nowhere dense classes are monadically stable, as well as all classes transducible from nowhere dense classes. Further generalising monadic stability, a class is monadically dependent if it does not transduce the class of all graphs.

The thesis makes major progress towards a resolution of the model checking conjecture, which predicts that for hereditary classes (i.e., classes closed under deletion of vertices) monadic dependence exactly delimits the tractability of the model checking problem. To analyse the tractability of the model checking problem, the thesis develops novel combinatorial characterisations for monadically stable and monadically dependent classes, which are more amenable to algorithmic treatment than the traditional definitions based on transductions. These combinatorial characterisations form an essential toolkit for the design of algorithms and are the foundation for one of the main results in the thesis: an algorithm that shows that the model checking problem is fixed-parameter tractable on every monadically stable graph class. They are also used to obtain another key contribution of the thesis: the hardness result for hereditary graph classes that are not monadically dependent.

Nikolas Mählmann carried out his PhD studies at the University of Bremen under the supervision of Sebastian Siebertz from 2021 to 2024. During this time he (co-)authored 10 articles, which were published in conference proceedings including LICS 2022, ICALP 2023 and 2025, STOC 2023 and 2024 and FOCS 2024. Currently he is a postdoctoral researcher at the University of Warsaw.