Logical Structures in Computation Seminar

Logics for Bisimulation-Invariance

Logics that precisely capture all the FO- or MSO-definable properties of "states" that are invariant under bisimulation can be seen as essentially "modal". Classical examples include basic modal logic (the modal fragment of FO: van Benthem) or the mu-calculus (the modal fragment of MSO: Janin-Walukiewicz). Variations concern extensions of the basic modalities w.r.t. richer notions of bisimulation and/or restricted classes of relevant models. Examples here include the modal fragment of FO over finite models (Rosen), of FO over (finite) epistemic models, of FO and MSO over finite transitive models, of FO over (finite) inquisitive epistemic models, as well as a new characterization of common knowledge logic over (finite) epistemic models. All of these require other than the classical model-theoretic techniques, and also go some little way towards exploring the modal spectrum between FO and MSO. The talk touches on older joint work with Anuj Dawar and on work in progress with Felix Canavoi and with Ivano Ciardelli.