A meta-modal logic for bisimulations

TL;DR

This paper introduces a new modal logic with a bisimulation quantifier, providing a complete axiomatization and decidability results, all verified in Isabelle/HOL.

Contribution

It extends modal logic with a bisimulation quantifier, offers a complete axiomatisation, and proves decidability, verified in Isabelle/HOL.

Findings

Bisimulations are definable via frame correspondence in the new logic.

The logic's satisfiability problem is PSPACE-complete.

All results are encoded and verified in Isabelle/HOL.

Abstract

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.