A meta-modal logic for bisimulations
This work offers a novel logical perspective on bisimulations, but its impact is limited to the modal logic community.
The paper introduces a new modal operator for universal quantification over bisimilar states, shows bisimulations are definable via frame correspondence, provides a sound and complete axiomatization, and proves the satisfiability problem is PSPACE-complete. All results are verified in Isabelle/HOL.
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.