Research projects

bisimulation-invariant model theory

In classical model theory, many questions (such as uniqueness or number of models satysfying certain properties) is usually treated up to isomorphism. But in many contexts bisimulation, not isomorphism, is the right equivalence relation. I am therefore interested in investigating classical model theoretic questions - but up to bisimulation instead of isomorphism. Here are some results:

A challenging open problem is to provide an analogous characterization for the fixpoint extension of modal logic. Unfortunately, the situation changes dramatically once we leave the world of compact logics:

expressive extensions of the modal fixpoint calculus μ-ML

I investigate an extension of the modal μ-calculus with new, bounded variants of the μ and ν operators. Such logic is capable of expressing natural unboundedness properties. At the same time, it still has many good features of MSO that MSO+U (which turned out to be undecidable) misses - e.g. existence of equivalent automata model, characterization of semantics in terms of games (generalizing parity games), or low topological complexity. The quest for solving satisfiability problem for this logic is in progress (with some partial results).

coalgebraic model theory

Coalgebraic logic is an elegant way to generalize modal logic to a wide variety of modal-like systems. An interesting problem in this setting is to lift the usual relations between logic, definable classes of models and validity in classes of models to the coalgebraic level. The notion of a comonad and its (Eilenberg-Moore) coalgebras seems promising in this context.