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:
-
my master thesis "Bisimulational Categoricity" written under supervision of dr Bartosz Wcisło and (unofficially) dr Mateusz Łełyk
"Bisimulational Categoricity" (master thesis)
-
an AiML paper extending previous results to: (i) two-way modal logic and two-way bisimulation and (ii) transitive modal logic (EF-logic) and transitive bisimulation (EF-bisimulation)
"Bisimulational Categoricity" (paper) & (slides)
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:
-
a poster, awarded during the online conference WKNKO-1, containing counterexamples to some possible exsentions of our previous characterisations
"Modal logic over the class of well-founded models is highly non-compact" (poster)
expressive extensions of the modal fixpoint calculus μ-ML
I investigate an extension of the modal μ-calculus with countdown operators, being bounded variants of the μ and ν operators. This logic, called countdown μ-calculus, 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).
-
a paper written with Bartek Klin and recently accepted for MFCS 2022 contains some of the established facts about the logic
"Countdown μ-calculus" (full version), (conference version) & (slides)
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.