Bisimulation

structure IsBisim {W W2 : Type} (M : KripkeModel W) (M2 : KripkeModel W2) (Z : W → W2 → Prop) (vo : Vocab) : Prop

A bisimulation between M and M2, for the given vocabulary.

• atoms (x : W) (y : W2) : Z x y → ∀ n ∈ vo.atomProps, M.val x n ↔ M2.val y n
• zig (x : W) (y : W2) : Z x y → ∀ c ∈ vo.atomProgs, ∀ (x' : W), M.Rel c x x' → ∃ (y' : W2), M2.Rel c y y' ∧ Z x' y'
• zag (x : W) (y : W2) : Z x y → ∀ c ∈ vo.atomProgs, ∀ (y' : W2), M2.Rel c y y' → ∃ (x' : W), M.Rel c x x' ∧ Z x' y'

theorem IsBisim.symm {W✝ : Type} {M : KripkeModel W✝} {W✝¹ : Type} {M2 : KripkeModel W✝¹} {Z : W✝ → W✝¹ → Prop} {vo : Vocab} (hZ : IsBisim M M2 Z vo) : IsBisim M2 M (flip Z) vo

theorem IsBisim.relate {W✝ : Type} {M : KripkeModel W✝} {W✝¹ : Type} {M2 : KripkeModel W✝¹} {Z : W✝ → W✝¹ → Prop} {vo : Vocab} (hZ : IsBisim M M2 Z vo) (α : Program) : α.voc ⊆ vo → ∀ (x : W✝) (y : W✝¹) (x' : W✝), Z x y → _root_.relate M α x x' → ∃ (y' : W✝¹), _root_.relate M2 α y y' ∧ Z x' y'

Extend IsBisim.zig from atomic programs to all programs.

theorem IsBisim.evaluate {W✝ : Type} {M : KripkeModel W✝} {W✝¹ : Type} {M2 : KripkeModel W✝¹} {Z : W✝ → W✝¹ → Prop} {vo : Vocab} (hZ : IsBisim M M2 Z vo) (φ : Formula) : φ.voc ⊆ vo → ∀ (x : W✝) (y : W✝¹), Z x y → (_root_.evaluate M x φ ↔ _root_.evaluate M2 y φ)

Bisimilar states agree on all formulas in the given vocabulary.