Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A meta-modal logic for bisimulations

Alfredo Burrieza, Fernando Soler-Toscano, Antonio Yuste-Ginel

TL;DR

This work develops meta-modal logic for bisimulations by introducing a single object-level modality $[\, b\,]$ that uniformly quantifies over all states bisimilar to the current one. It shows that the key bisimulation conditions—atomic harmony, forth, and back—are definable in this language and provides a sound and complete axiomatisation for the class of bi-models, with the completeness proof encoded and verified in Isabelle/HOL. The approach clarifies expressivity advantages over standard modal logic and situates the results in a broader context of modal definability, filtration, and bisimulation theory, while outlining future research directions in decidability and extensions to more general morphisms. The work thus advances a coherent meta-modal perspective on bisimulation, with potential applications to automated reasoning about model equivalences and meta-theoretic properties in modal logic.

Abstract

We propose a modal study of the notion of bisimulation. Our contribution is twofold. First, we extend the basic modal language with a new modality [b], 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. Second, we provide a sound and complete axiomatisation of the class of all pairs of Kripke models linked by bisimulations.

A meta-modal logic for bisimulations

TL;DR

This work develops meta-modal logic for bisimulations by introducing a single object-level modality that uniformly quantifies over all states bisimilar to the current one. It shows that the key bisimulation conditions—atomic harmony, forth, and back—are definable in this language and provides a sound and complete axiomatisation for the class of bi-models, with the completeness proof encoded and verified in Isabelle/HOL. The approach clarifies expressivity advantages over standard modal logic and situates the results in a broader context of modal definability, filtration, and bisimulation theory, while outlining future research directions in decidability and extensions to more general morphisms. The work thus advances a coherent meta-modal perspective on bisimulation, with potential applications to automated reasoning about model equivalences and meta-theoretic properties in modal logic.

Abstract

We propose a modal study of the notion of bisimulation. Our contribution is twofold. First, we extend the basic modal language with a new modality [b], 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. Second, we provide a sound and complete axiomatisation of the class of all pairs of Kripke models linked by bisimulations.

Paper Structure

This paper contains 13 sections, 14 theorems, 20 equations.

Table of Contents

  1. Introduction
  2. Background
  3. A simple modal logic for bisimulations
  4. Syntax
  5. Semantics
  6. Expressivity
  7. (Un)definability
  8. Axiom system
  9. Soundness and completeness
  10. Discussion and related work
  11. Conclusion
  12. Recap.
  13. Open challenges.

Key Result

Theorem 1

Given two Kripke pointed models $({\cal M},w)$ and $(\mathcal{M'},w')$ which are image-finitary, then ${\cal M}, w\, \underline{\leftrightarrow}\, {\cal M'}, w'$ iff $({\cal M},w)$ and $(\mathcal{M'},w')$ satisfy the exact same $\mathcal{L}_{\square}$-formulas.

Theorems & Definitions (39)

  • Definition 1: Basic modal language
  • Definition 2: Basic frames, models and truth
  • Definition 3: Bisimulation for $\mathcal{L}_{\square}$
  • Theorem 1: hennessy1985algebraic
  • Definition 4
  • Definition 5: Frames for ${\cal L}_{{\square [\,b\,]}}$
  • Definition 6: Models for ${\cal L}_{{\square [\,b\,]}}$
  • Definition 7: Truth for ${\cal L}_{{\square [\,b\,]}}$
  • Remark 1
  • Example 1: A bi-model
  • ...and 29 more