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), & (slides)
effective separation & interpolation
A separator for pair of logical formulae φ and φ′ is a formula ψ such that φ entails ψ and ψ entails ¬φ′. Separation is particularly interesting when the intermediate formula ψ is expressed in a weaker logic than φ and φ′. The notion generalizes definitions (separator for φ and ¬φ is equivalent to ψ) and interpolation (when ψ only uses the common part of the vocabularies of φ and φ′). I am interested in effective aspects of separation: given φ,φ′, can we decide if there is a separator of a certain kind? And if so, can we compute it?
-
A STACS 2025 paper (full version) written with Jean Christoph Jung where we investigated the case of separation of modal fixpoint formulae by a modal formula with no fixpoints. We solved the problem over multiple classes of models, and found a surprising difference in complexity between binary and ternary trees.
"Modal Separation of Fixpoint Formulae (full version)" & (slides)