Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: A meta-modal logic for bisimul...


view this post on Zulip Email Gateway (Jul 24 2025 at 21:57):

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!

smime.p7s


Last updated: Jul 26 2025 at 12:43 UTC