pith. sign in

arxiv: 2507.15117 · v3 · submitted 2025-07-20 · 💻 cs.LO · math.LO

A meta-modal logic for bisimulations

Alfredo Burrieza , Fernando Soler-Toscano , Antonio Yuste-Ginel This is my paper

Pith reviewed 2026-05-19 03:41 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords bisimulationmodal logicKripke modelsframe correspondenceaxiomatizationsatisfiabilitydecidability
0
0 comments X

The pith

Bisimulation relations between Kripke models become expressible inside an extended modal logic via a new modality.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends the basic modal language with a modality that asserts a property holds at every state bisimilar to the current one. It shows that this addition makes bisimulations definable through first-order frame correspondence conditions. A sound and complete axiomatization is given for the logic over all pairs of models related by bisimulation. Satisfiability is shown to be PSPACE-complete by a direct translation to standard modal logic K that works once an equivalence condition is imposed on the accessibility relation.

Core claim

By adjoining a modality whose semantics range over all bisimilar worlds, bisimulations between Kripke models become definable in the object language by frame correspondence; the resulting logic over bisimulation-related model pairs admits a sound and complete axiomatization; and satisfiability remains decidable and PSPACE-complete after translation to modal logic K under a simple frame condition.

What carries the argument

The new bisimulation modality that universally quantifies over all states bisimilar to the current world.

If this is right

  • Bisimulations can be expressed directly by object-language formulas via frame correspondence.
  • The class of bisimulation-related model pairs has a sound and complete axiomatization.
  • Satisfiability of the new logic reduces to that of modal logic K and inherits PSPACE-completeness under the stated frame condition.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Existing decision procedures for modal logic K could be reused to check bisimulation properties once the frame condition is ensured.
  • The same internalization technique might apply to other structural relations such as simulation or trace equivalence.

Load-bearing premise

Imposing an equivalence condition on the accessibility relation preserves the intended semantics when translating to standard modal logic K.

What would settle it

A concrete pair of Kripke models related by bisimulation together with a formula whose truth value differs between the extended logic and its translation to K without the equivalence condition.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper extends the basic modal language with a new modality nbi whose intended semantics is universal quantification over states bisimilar to the current one. It shows that bisimulations are definable in the object language via frame correspondence, supplies a sound and complete axiomatization for the class of all pairs of Kripke models that are bisimulation-related, and establishes that satisfiability is PSPACE-complete by a translation to standard modal logic K that holds under a stated frame condition (accessibility as equivalence). All results—including the language definition, frame correspondence, axiomatization, and complexity proof—are encoded and verified in Isabelle/HOL.

Significance. If the results hold, the work supplies a modal-logic treatment of bisimulations that makes them definable in the object language and yields a decidable, completely axiomatized logic for bisimulation-related model pairs. The machine-checked proofs in Isabelle/HOL constitute a clear strength: they directly verify the frame correspondence for definability, the soundness and completeness of the axiomatization, and the satisfiability-preservation lemma under the precise frame condition used in the translation. This verification removes any unverified gap in the argument and renders the development self-contained against external benchmarks such as modal logic K.

minor comments (2)
  1. [Abstract] The abstract refers to 'a simple frame condition' without stating it explicitly; adding the precise condition (accessibility as equivalence on the meta-model) already in the abstract would improve immediate readability.
  2. [Introduction] The notation nbi is introduced without an early illustrative formula; including a short example of a formula using the new modality in the introduction would help readers grasp its intended use before the technical development.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept the manuscript. The review accurately captures the contributions, including the extension with the nbi modality, frame correspondence for definability, the sound and complete axiomatization, the PSPACE-completeness result via translation to K, and the Isabelle/HOL verification of all components.

Circularity Check

0 steps flagged

No significant circularity; results are self-contained via Isabelle/HOL formalization

full rationale

The paper defines a new modality □bi for universal quantification over bisimilar states, proves definability of bisimulations via frame correspondence, supplies a sound and complete axiomatization for bisimulation-related model pairs, and establishes PSPACE-completeness of satisfiability by reduction to modal logic K under an explicit frame condition (accessibility as equivalence). All steps are encoded and machine-checked in Isabelle/HOL, which constitutes an external, verifiable benchmark independent of any self-citation chain or parameter fitting. The translation lemma is verified directly under the stated condition rather than assumed without proof, so no derivation reduces to its inputs by construction. This is the standard case of a formally verified logic paper with no load-bearing circular steps.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The paper relies on standard modal logic axioms (K, necessitation) plus the new bisimulation modality axioms. No free parameters are fitted to data. The new modality is an invented syntactic entity whose semantics are given by the bisimulation relation.

axioms (2)
  • standard math Standard K axiom and necessitation rule for the new modality
    Invoked in the soundness and completeness proofs for the axiomatization of bisimulation-related pairs.
  • domain assumption Frame correspondence for bisimulation definability
    The correspondence between the new modality and the bisimulation relation is taken as the semantic foundation.
invented entities (1)
  • nbi modality (bisimulation quantifier) no independent evidence
    purpose: To express universal quantification over bisimilar states inside the object language
    Introduced as the central syntactic extension; its semantics are defined via the bisimulation relation on Kripke models.

pith-pipeline@v0.9.0 · 5649 in / 1548 out tokens · 32939 ms · 2026-05-19T03:41:55.464708+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

22 extracted references · 22 canonical work pages

  1. [1]

    Quotient dynamics: The logic of abstraction

    Alexandru Baltag, Nick Bezhanishvili, Julia Ilin, and Ayb¨ uke ¨Ozg¨ un. Quotient dynamics: The logic of abstraction. In Logic, Rationality, and Interaction: 6th International Workshop (LORI 2017) , pages 181–194. Springer, 2017

    work page 2017

  2. [2]

    Local and symbolic bisimulation using tabled constraint logic programming

    Samik Basu, Madhavan Mukund, CR Ramakrishnan, IV Ramakrish- nan, and Rakesh Verma. Local and symbolic bisimulation using tabled constraint logic programming. In International Conference on Logic Programming, pages 166–180. Springer, 2001

    work page 2001

  3. [3]

    Modal logic

    Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal logic. Cambridge University Press, 2010

    work page 2010

  4. [4]

    Symbolic model checking: 1020 states and be- yond

    Jerry R Burch, Edmund M Clarke, Kenneth L McMillan, David L Dill, and Lain-Jinn Hwang. Symbolic model checking: 1020 states and be- yond. Information and computation , 98(2):142–170, 1992

    work page 1992

  5. [5]

    Modal logic: an introduction

    Brian F Chellas. Modal logic: an introduction . Cambridge university press, 1980

    work page 1980

  6. [6]

    Modal logic for philosophers

    James W Garson. Modal logic for philosophers . Cambridge University Press, 2013. 22

    work page 2013

  7. [7]

    Using the universal modality: gains and questions

    Valentin Goranko and Solomon Passy. Using the universal modality: gains and questions. Journal of Logic and Computation, 2(1):5–30, 1992

    work page 1992

  8. [8]

    Algebraic laws for nondeter- minism and concurrency

    Matthew Hennessy and Robin Milner. Algebraic laws for nondeter- minism and concurrency. Journal of the ACM (JACM) , 32(1):137–161, 1985

    work page 1985

  9. [9]

    Knowledge and belief: An introduction to the logic of the two notions

    Kaarlo Jaakko Juhani Hintikka. Knowledge and belief: An introduction to the logic of the two notions . Cornell University Press, 1962

    work page 1962

  10. [10]

    Psychology Press, 1996

    George Edward Hughes and Maxwell John Cresswell.A new introduction to modal logic. Psychology Press, 1996

    work page 1996

  11. [11]

    Filtration revisited: Lattices of stable non-classical logics

    Julia Ilin. Filtration revisited: Lattices of stable non-classical logics . PhD thesis, University of Amsterdam, 2018

    work page 2018

  12. [12]

    The algebra of topology

    John Charles Chenoweth McKinsey and Alfred Tarski. The algebra of topology. Annals of mathematics , 45(1):141–191, 1944

    work page 1944

  13. [13]

    Is- abelle/HOL: a proof assistant for higher-order logic , volume 2283

    Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Is- abelle/HOL: a proof assistant for higher-order logic , volume 2283. Springer, 2002

    work page 2002

  14. [14]

    Time and modality

    Arthur N Prior. Time and modality . Oxford University Press, 1957

    work page 1957

  15. [15]

    On the origins of bisimulation and coinduction

    Davide Sangiorgi. On the origins of bisimulation and coinduction. ACM Transactions on Programming Languages and Systems (TOPLAS) , 31(4):1–41, 2009

    work page 2009

  16. [16]

    Modal correspondence theory

    Johan van Benthem. Modal correspondence theory. PhD thesis, Univer- sity of Amsterdam, 1976

    work page 1976

  17. [17]

    Modal logic for open minds

    Johan van Benthem. Modal logic for open minds . Center for the Study of Language and Information Stanford, 2010

    work page 2010

  18. [18]

    Vistas from a drop of water

    Johan van Benthem. Vistas from a drop of water. In Ensayos en Honor a Mar´ ıa Manzano. College Publications, 2019

    work page 2019

  19. [19]

    Modern faces of filtration

    Johan van Benthem and Nick Bezhanishvili. Modern faces of filtration. In Kit Fine on Truthmakers, Relevance, and Non-classical Logic , pages 23–61. Springer, 2023. 23

    work page 2023

  20. [20]

    Lindstrom theorems for fragments of first-order logic

    Johan Van Benthem, Balder Ten Cate, and Jouko Vaananen. Lindstrom theorems for fragments of first-order logic. Logical Methods in Computer Science, 5, 2009

    work page 2009

  21. [21]

    Deontic logic

    Georg Henrik Von Wright. Deontic logic. Mind, 60(237):1–15, 1951

    work page 1951

  22. [22]

    Basic concepts in modal logic

    Edward N Zalta. Basic concepts in modal logic. Center for the Study of Language and Information , 1995. 24

    work page 1995