Bisimulation invariance for BSML

[AAY24] [Ant25]

The carrier-level bisimulation substrate (WorldBisim, StateBisim, and the Lemma 3.7 transport lemmas) lives in Core/Logic/Modal/Bisimulation.lean, shared across the modal team logics. This file specialises it to BSML: the modal-depth measure on BSMLFormula and the headline invariance result (Theorem 3.8) for BSML's bilateral evaluation.

Main declarations

• BSMLFormula.modalDepth — modal depth (page 9): atoms/NE are 0, conj/disj take max, poss increments.
• bisim_invariant_eval — Theorem 3.8 for BSML: k-bisimilar states agree on eval for all formulas of modal depth ≤ k, for both polarities.

Implementation notes

The bisim-invariance proof inducts on the formula, handling both polarities (eval M b φ s) jointly at each step. The negation case flips polarity without changing depth; the modal case uses StateBisim.accessImage (Lemma 3.7(i)) to recurse at depth k; conjunction and disjunction use StateBisim.splitPreserve (Lemma 3.7(ii)) for the split-existential clauses (conj-antiSupport and disj-support).

Todo

• Hennessy-Milner direction (Theorem 3.3): k-equivalence implies k-bisimilarity, via Hintikka formulas. Requires a finite atom set hypothesis ([Fintype Atom]) for the characteristic-formula construction. Deferred — Theorem 3.8 alone is enough for the expressive-completeness side of [AAY24] §3.
• Bisim invariance for BSMLOr.eval and BSMLEmpty.eval. Same shape with one new case each (gdisj is structurally like support_conj at the team level; empt reduces to support of the inner formula or s = ∅, both bisim-preserved).

Modal depth

def Core.Logic.Modal.BSML.BSMLFormula.modalDepth {Atom : Type u_3} : BSMLFormula Atom → ℕ

Modal depth of a BSMLFormula (page 9 of [AAY24]). Atoms and NE are 0; neg preserves depth; conj and disj take the max; poss increments.

Equations

• (Core.Logic.Modal.BSML.BSMLFormula.atom a).modalDepth = 0
• Core.Logic.Modal.BSML.BSMLFormula.ne.modalDepth = 0
• ψ.neg.modalDepth = ψ.modalDepth
• (ψ₁.conj ψ₂).modalDepth = max ψ₁.modalDepth ψ₂.modalDepth
• (ψ₁.disj ψ₂).modalDepth = max ψ₁.modalDepth ψ₂.modalDepth
• ψ.poss.modalDepth = ψ.modalDepth + 1

Theorem 3.8: bisimulation invariance for BSML

theorem Core.Logic.Modal.BSML.bisim_invariant_eval {W : Type u_1} {W' : Type u_2} [DecidableEq W] [Fintype W] [DecidableEq W'] [Fintype W'] {Atom : Type u_3} (φ : BSMLFormula Atom) {k : ℕ} : φ.modalDepth ≤ k → ∀ {M : BSMLModel W Atom} {M' : BSMLModel W' Atom} {s : Finset W} {s' : Finset W'}, StateBisim k M s M' s' → ∀ (b : Bool), eval M b φ s ↔ eval M' b φ s'

Theorem 3.8 of [AAY24] specialised to BSML: if s ⇌_k s' and φ : BSMLFormula Atom has modal depth ≤ k, then eval M b φ s ↔ eval M' b φ s' for both polarities.

Proved by structural induction on φ, with both polarities handled jointly at each step. The neg case flips polarity without changing depth; the poss case uses Lemma 3.7(i) to recurse at depth k; conjunction and disjunction use Lemma 3.7(ii) for the split-existential clauses (conj-antiSupport and disj-support).