Research
My research interests lie mainly in the field of automata theory. This means that I am interested in the computational power of different kinds of automata models, and in verification algorithms for them, see for example our paper On the Upward/Downward Closures of Petri Nets.
I am currently mostly working on games with perfect information, two player games, where each player knows before each of her moves the current state of the game. On finite graphs, such games have been considered for years. On infinite graphs, e.g. graphs occurring as computation trees of pushdown automata, games with perfect information are an active field of research.
In our paper Summaries for Context-Free Games, we have introduced an efficient, summary-based algorithm for solving reachability games on the graph of sentential forms for a context-free grammar. We have extended this approach to more involved settings, namely to infinite words generated by grammars in Liveness Verification and Synthesis: New Algorithms for Recursive Programs, and to games defined by higher-order recursion schemes in Domains for Higher-Order Games.
In all of these algorithms, the crucial step is finding the least solution of a system of equations defined by a monotone function over an underlying lattice. Therefore, I am also interested in algorithms to solve such systems of equations in general. We have considered a symbolic variant of Newton iteration for semirings (introduced by Esparza et al.) in our paper Munchausen Iteration.
To understand the practical importance of the games mentioned above, allow me to make a small detour. A verification problem, i.e. "Does a given system satisfy a given specification?" can be rephrased as the problem of checking whether the language of all possible system behaviors is included in the language of all behaviors allowed by the specification. This leads to a research field called language theoretic verification, where one aims to find finite representations for these two languages, and then solve the verification problem by executing an inclusion check. In many cases, the system is too complex and no finite representations that would allow for an inclusion check exists. Then, one can tackle the problem by iteratively refining an approximation of the full system behavior.
While inclusion checks are crucial for verification problems, games generalize this relationship to synthesis problems. In a game, we can use the players to represent two types of non-determinism, a controllable, angelic one, and an uncontrollable, demonic one. Synthesizing a system whose behavior satisfies the specification, no matter how the environment behaves, can be done guided by a winning strategy for the angelic non-determinism.