From: Tobias Nipkow <nipkow@in.tum.de>
A meta-modal logic for bisimulations
Alfredo Burrieza, Fernando Soler-Toscano and Antonio Yuste-Ginel
Bisimulations are a fundamental formal tool in the model theory of standard
modal logic. Roughly speaking, bisimulations provide a clear answer to a
foundational model-theoretical question: Given two (Kripke-style) models, what
conditions are sufficient and necessary for them to satisfy the same modal
formulas? We propose a modal study of the notion of bisimulation. We extend the
basic modal language with a new modality
, whose intended meaning is universal quantification over all states that are
bisimilar to the current one. We provide a sound and complete axiomatisation of
the class of all pairs of Kripke models linked by bisimulations.
https://www.isa-afp.org/entries/Bisimulation_Logic.html
Enjoy!
Last updated: Jul 26 2025 at 12:43 UTC