Documentation

Linglib.Logic.Team.Bisimulation

Bisimulation for modal team logics #

Two teams are related by the lifting Set.LiftRel r of a relation r on points when every point of each team is r-related to a point of the other. Team properties P and P' are invariant under r when teams related in this way agree on them. Every connective of Team/Operations.lean preserves invariance, the modalities one step down a chain of relations, so a team logic whose evaluation is a fold over these connectives is invariant under bounded bisimulation of Kripke models.

Main definitions #

Main results #

Implementation notes #

[AAY24] relativize bisimilarity to a finite set of atoms. Here it compares every atom of the atom type, which is the paper's notion when that type is the finite set.

References #

source
def Team.Invariant {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (P : TeamProperty α) (P' : TeamProperty β) :
Prop

Team properties P and P' are invariant under a relation r on points when teams related by the lifting Set.LiftRel r agree on them.

Equations
Instances For

    Non-modal connectives and atoms #

    source
    theorem Team.invariant_flat {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {p : α → Prop} {p' : β → Prop} (hp : Relator.LiftFun r Iff p p') :
    Invariant r (flat p) (flat p')
    source
    theorem Team.invariant_ne {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
    Invariant r ne ne
    source
    theorem Team.invariant_singleton_empty {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
    Invariant r {∅} {∅}
    source
    theorem Team.invariant_univ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
    Invariant r Set.univ Set.univ
    source
    theorem Team.Invariant.inter {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {P Q : TeamProperty α} {P' Q' : TeamProperty β} (h₁ : Invariant r P P') (h₂ : Invariant r Q Q') :
    Invariant r (P ∩ Q) (P' ∩ Q')
    source
    theorem Team.Invariant.union {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {P Q : TeamProperty α} {P' Q' : TeamProperty β} (h₁ : Invariant r P P') (h₂ : Invariant r Q Q') :
    Invariant r (P ∪ Q) (P' ∪ Q')
    source
    theorem Team.invariant_dep {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {f' : β → γ} {g : α → δ} {g' : β → δ} (hf : Relator.LiftFun r Eq f f') (hg : Relator.LiftFun r Eq g g') :
    Invariant r (dep f g) (dep f' g')
    source
    theorem Team.invariant_incl {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {γ : Type u_3} {f g : α → γ} {f' g' : β → γ} (hf : Relator.LiftFun r Eq f f') (hg : Relator.LiftFun r Eq g g') :
    Invariant r (incl f g) (incl f' g')
    source
    theorem Team.Invariant.singleton {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {P : TeamProperty α} {P' : TeamProperty β} (h : Invariant r P P') :
    Relator.LiftFun r Iff (fun (a : α) => {a} ∈ P) fun (b : β) => {b} ∈ P'

    Invariant properties agree on the singleton teams of related points.

    Flat modalities #

    The modalities take an invariance under r to an invariance under r₁, given that r₁-related points have successor sets related by the lifting of r. For Kripke models r₁ is bisimilarity at depth k + 1 and r at depth k ([AAY24] Lemma 3.7(i)).

    source
    theorem Set.LiftRel.exists_finset_subset {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {s t : Finset α} {s' : Finset β} (hs : LiftRel r ↑s ↑s') (ht : t ⊆ s) :
    ∃ t' ⊆ s', LiftRel r ↑t ↑t'

    A sub-team of a team related by the lifting of r has a related sub-team on the other side.

    source
    theorem Team.Invariant.nec {α : Type u_1} {β : Type u_2} {r r₁ : α → β → Prop} {P : TeamProperty α} {P' : TeamProperty β} {R : α → Finset α} {R' : β → Finset β} (hR : ∀ (a : α) (b : β), r₁ a b → Set.LiftRel r ↑(R a) ↑(R' b)) (h : Invariant r P P') :
    Invariant r₁ (Team.nec R P) (Team.nec R' P')
    source
    theorem Team.Invariant.poss {α : Type u_1} {β : Type u_2} {r r₁ : α → β → Prop} {P : TeamProperty α} {P' : TeamProperty β} {R : α → Finset α} {R' : β → Finset β} (hR : ∀ (a : α) (b : β), r₁ a b → Set.LiftRel r ↑(R a) ↑(R' b)) (h : Invariant r P P') :
    Invariant r₁ (Team.poss R P) (Team.poss R' P')

    Splits #

    source
    theorem Set.LiftRel.exists_finset_union_eq {α : Type u_1} {β : Type u_2} {r : α → β → Prop} [DecidableEq α] [DecidableEq β] {s t u : Finset α} {s' : Finset β} (hs : LiftRel r ↑s ↑s') (hsplit : t ∪ u = s) :
    ∃ (t' : Finset β) (u' : Finset β), t' ∪ u' = s' ∧ LiftRel r ↑t ↑t' ∧ LiftRel r ↑u ↑u'

    A split of a team related by the lifting of r has a related split on the other side ([AAY24] Lemma 3.7(ii)).

    source
    theorem Team.Invariant.tensor {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {P Q : TeamProperty α} {P' Q' : TeamProperty β} [DecidableEq α] [DecidableEq β] (h₁ : Invariant r P P') (h₂ : Invariant r Q Q') :
    Invariant r (Team.tensor P Q) (Team.tensor P' Q')

    Image modalities of dependence and inclusion logic #

    source
    theorem Team.Invariant.necImage {α : Type u_1} {β : Type u_2} {r r₁ : α → β → Prop} {P : TeamProperty α} {P' : TeamProperty β} {R : α → Finset α} {R' : β → Finset β} [DecidableEq α] [DecidableEq β] (hR : ∀ (a : α) (b : β), r₁ a b → Set.LiftRel r ↑(R a) ↑(R' b)) (h : Invariant r P P') :
    Invariant r₁ (Team.necImage R P) (Team.necImage R' P')
    source
    theorem Team.Invariant.possWitness {α : Type u_1} {β : Type u_2} {r r₁ : α → β → Prop} {P : TeamProperty α} {P' : TeamProperty β} {R : α → Finset α} {R' : β → Finset β} [DecidableEq α] [DecidableEq β] (hR : ∀ (a : α) (b : β), r₁ a b → Set.LiftRel r ↑(R a) ↑(R' b)) (hP : IsLowerSet P) (hP' : IsLowerSet P') (h : Invariant r P P') :
    Invariant r₁ (Team.possWitness R P) (Team.possWitness R' P')

    The single-witness possibility modality preserves invariance between downward-closed properties.

    source
    theorem Team.Invariant.possLax {α : Type u_1} {β : Type u_2} {r r₁ : α → β → Prop} {P : TeamProperty α} {P' : TeamProperty β} {R : α → Finset α} {R' : β → Finset β} [DecidableEq α] [DecidableEq β] (hR : ∀ (a : α) (b : β), r₁ a b → Set.LiftRel r ↑(R a) ↑(R' b)) (h : Invariant r P P') :
    Invariant r₁ (Team.possLax R P) (Team.possLax R' P')

    Bisimulation of Kripke models #

    source
    def ModalLogic.WorldBisim {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} :
    ℕ → KripkeModel W Atom → W → KripkeModel W' Atom → W' → Prop

    Pointed Kripke models are k-bisimilar ([AAY24] Definition 3.1) when they agree on every atom and, at positive depth, their successor sets are related by the lifting of bisimilarity one depth down.

    Equations
    • One or more equations did not get rendered due to their size.
    • ModalLogic.WorldBisim 0 x✝³ x✝² x✝¹ x✝ = ∀ (p : Atom), x✝³.val p x✝² ↔ x✝¹.val p x✝
    Instances For
      source
      theorem ModalLogic.WorldBisim.refl {W : Type u_1} {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (w : W) :
      WorldBisim k M w M w
      source
      theorem ModalLogic.WorldBisim.val_iff {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} (h : WorldBisim k M w M' w') (p : Atom) :
      M.val p w ↔ M'.val p w'
      source
      def ModalLogic.StateBisim {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (s : Finset W) (M' : KripkeModel W' Atom) (s' : Finset W') :
      Prop

      Teams are k-bisimilar ([AAY24] Definition 3.6) when they are related by the lifting of k-bisimilarity of their worlds.

      Equations
      Instances For
        source
        def ModalLogic.BisimClosed {W : Type u_1} {Atom : Type u_3} (M : KripkeModel W Atom) (P : Team.TeamProperty W) :
        Prop

        A team property of M is closed under bounded bisimulation when, for some depth k, it is invariant under k-bisimilarity within M.

        Equations
        Instances For