A meta-modal logic for bisimulations

We propose a modal study of the notion of bisimulation. Our contribution is threefold. First, we extend the basic modal language with a new modality $\nbi$, whose intended meaning is universal quantification over all states that are bisimilar to the current one. We show that bisimulations are definable in this object language via frame correspondence. Second, we provide a sound and complete axiomatisation of the class of all pairs of Kripke models that are bisimulation-related. Third, we show that the satisfiability problem of our logic is decidable and PSPACE-complete via a translation to standard modal logic $K$ under a simple frame condition. All our results are encoded and verified by Isabelle/HOL.