Bisimulation

4 fully proved

Modal

StructureBisimulation#✓fully proved

Let \(M\) and \(N\) be Kripke models over the same atoms, with sets of worlds \(W\) and \(V\) and accessibility relations \(R_M\) and \(R_N\). A relation \(Z \subseteq W \times V\) is a bisimulation between \(M\) and \(N\) when, for all \(w \in W\) and \(v \in V\) with \(w \mathrel{Z} v\): each atom \(a\) is true at \(w\) in \(M\) if and only if \(a\) is true at \(v\) in \(N\); for every \(w'\) with \(w \mathrel{R_M} w'\) there is \(v'\) with \(v \mathrel{R_N} v'\) and \(w' \mathrel{Z} v'\) (forth); and for every \(v'\) with \(v \mathrel{R_N} v'\) there is \(w'\) with \(w \mathrel{R_M} w'\) and \(w' \mathrel{Z} v'\) (back).

structure Bisimulation (M : KripkeModel W Atom) (N : KripkeModel V Atom)
    (R : W → V → Prop) : Prop where
  /-- Related worlds agree on every atom. -/
  atom_iff : ∀ {w v}, R w v → ∀ a, M.valuation w a ↔ N.valuation v a
  /-- Every accessible world of the first model is matched by an accessible world of the
    second. -/
  forth : ∀ {w v w'}, R w v → M.rel w w' → ∃ v', N.rel v v' ∧ R w' v'
  /-- Every accessible world of the second model is matched by an accessible world of the
    first. -/
  back : ∀ {w v v'}, R w v → N.rel v v' → ∃ w', M.rel w w' ∧ R w' v'

Uses 1 · Used by 5

Statement usesKripke model

Used byBisimilar worlds · Bisimulations preserve modal formulas · Bisimilar worlds are modally equivalent · Bisimulation-invariant formulas · Modal formulas are bisimulation-invariant under the standard translation

Bisimulation

TheoremBisimulations preserve modal formulas#✓fully proved

Let \(Z\) be a bisimulation between Kripke models \(M\) and \(N\) over the same atoms. If \(Z\) relates a world \(w\) of \(M\) to a world \(v\) of \(N\), then every modal formula \(\varphi\) is satisfied at \(w\) in \(M\) if and only if \(\varphi\) is satisfied at \(v\) in \(N\).

theorem satisfies_iff (h : Bisimulation M N R) (φ : Formula Atom) (w : W) (v : V)
    (hr : R w v) : M.Satisfies w φ ↔ N.Satisfies v φ

Uses 4 · Used by 2

Statement usesBisimulation · Modal formulas · Kripke model · Satisfaction in a Kripke model

Used byBisimilar worlds are modally equivalent · Modal formulas are bisimulation-invariant under the standard translation

DefinitionBisimilar worlds#✓fully proved

Let \(M\) and \(N\) be Kripke models over the same atoms. A world \(w\) of \(M\) and a world \(v\) of \(N\) are bisimilar if some bisimulation between \(M\) and \(N\) relates \(w\) to \(v\).

def Bisimilar (M : KripkeModel W Atom) (N : KripkeModel V Atom) (w : W) (v : V) : Prop :=
  ∃ R : W → V → Prop, Bisimulation M N R ∧ R w v

Uses 2 · Used by 1

Statement usesBisimulation · Kripke model

Used byBisimilar worlds are modally equivalent

TheoremBisimilar worlds are modally equivalent#✓fully proved

If a world \(w\) of a Kripke model \(M\) and a world \(v\) of a Kripke model \(N\) over the same atoms are bisimilar, then every modal formula \(\varphi\) is satisfied at \(w\) in \(M\) if and only if \(\varphi\) is satisfied at \(v\) in \(N\).

theorem Bisimilar.satisfies_iff {M : KripkeModel W Atom} {N : KripkeModel V Atom}
    {w : W} {v : V} (h : Bisimilar M N w v) (φ : Formula Atom) :
    M.Satisfies w φ ↔ N.Satisfies v φ

Uses 6

Statement usesBisimilar worlds · Modal formulas · Kripke model · Satisfaction in a Kripke model

Proof usesBisimulation · Bisimulations preserve modal formulas

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.