Bisimulation and Bisimilarity

A bisimulation is a binary relation on the states of two LTSs, which establishes a tight semantic correspondence. More specifically, if two states s₁ and s₂ are related by a bisimulation, then s₁ can mimic all transitions of s₂ and vice versa. Furthermore, the derivatives reaches through these transitions remain related by the bisimulation.

Bisimilarity is the largest bisimulation: given an LTS, it relates any two states that are related by a bisimulation for that LTS.

Weak bisimulation (resp. bisimilarity) is the relaxed version of bisimulation (resp. bisimilarity) whereby internal actions performed by processes can be ignored.

For an introduction to theory of bisimulation, we refer to [Sangiorgi2011].

Main definitions

• lts.IsBisimulation r: the relation r is a bisimulation for the LTS lts.

• Bisimilarity lts is the binary relation on the states of lts that relates any two states related by some bisimulation on lts.

• lts.IsBisimulationUpTo r: the relation r is a bisimulation up to bisimilarity (this is known as one of the 'up to' techniques for bisimulation).

• lts.IsWeakBisimulation r: the relation r on the states of the LTS lts is a weak bisimulation.

• WeakBisimilarity lts is the binary relation on the states of lts that relates any two states related by some weak bisimulation on lts.

• lts.IsSWBisimulation is a more convenient definition for establishing weak bisimulations, which we prove to be sound and complete.

Notations

• s₁ ~[lts] s₂: the states s₁ and s₂ are bisimilar in the LTS lts.
• s₁ ≈[lts] s₂: the states s₁ and s₂ are weakly bisimilar in the LTS lts.

Main statements

• LTS.IsBisimulation.inv: the inverse of a bisimulation is a bisimulation.
• Bisimilarity.eqv: bisimilarity is an equivalence relation (see Equivalence).
• Bisimilarity.isBisimulation: bisimilarity is itself a bisimulation.
• Bisimilarity.largest_bisimulation: bisimilarity is the largest bisimulation.
• Bisimilarity.gfp: the union of bisimilarity and any bisimulation is equal to bisimilarity.
• LTS.IsBisimulationUpTo.isBisimulation: any bisimulation up to bisimilarity is a bisimulation.
• LTS.IsBisimulation.traceEq: any bisimulation that relates two states implies that they are trace equivalent (see TraceEq).
• Bisimilarity.deterministic_bisim_eq_traceEq: in a deterministic LTS, bisimilarity and trace equivalence coincide.
• Bisimilarity.symm_simulation: bisimilarity can be characterized through symmetric simulations.
• WeakBisimilarity.weakBisim_eq_swBisim: weak bisimulation and sw-bisimulation coincide.
• WeakBisimilarity.eqv: weak bisimilarity is an equivalence relation.

def Cslib.LTS.IsBisimulation {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop

A relation is a bisimulation if, whenever it relates two states, the transitions originating from these states mimic each other and the reached derivatives are themselves related.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cslib.LTS.IsHomBisimulation {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (r : State → State → Prop) : Prop

A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same.

Equations

• lts.IsHomBisimulation = lts.IsBisimulation lts

theorem Cslib.LTS.IsBisimulation.follow_fst {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} {s₁ : State✝} {s₂ : State✝¹} {μ : Label✝} {s₁' : State✝} (hb : lts₁.IsBisimulation lts₂ r) (hr : r s₁ s₂) (htr : lts₁.Tr s₁ μ s₁') : ∃ (s₂' : State✝¹), lts₂.Tr s₂ μ s₂' ∧ r s₁' s₂'

Helper for following a transition by the first state in a pair of a Bisimulation.

theorem Cslib.LTS.IsBisimulation.follow_snd {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} {s₁ : State✝} {s₂ : State✝¹} {μ : Label✝} {s₂' : State✝¹} (hb : lts₁.IsBisimulation lts₂ r) (hr : r s₁ s₂) (htr : lts₂.Tr s₂ μ s₂') : ∃ (s₁' : State✝), lts₁.Tr s₁ μ s₁' ∧ r s₁' s₂'

Helper for following a transition by the second state in a pair of a Bisimulation.

def Cslib.LTS.Bisimilarity {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop

Two states are bisimilar if they are related by some bisimulation.

Equations

• lts₁.Bisimilarity lts₂ s₁ s₂ = ∃ (r : State₁ → State₂ → Prop), r s₁ s₂ ∧ lts₁.IsBisimulation lts₂ r

def Cslib.LTS.«term_~[_,_]_» : Lean.TrailingParserDescr

Notation for bisimilarity.

Differently from standard pen-and-paper presentations, we require the LTSs to be mentioned explicitly.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cslib.LTS.HomBisimilarity {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : State → State → Prop

Homogeneous bisimilarity is bisimilarity where the underlying LTSs are the same.

Equations

• lts.HomBisimilarity = lts.Bisimilarity lts

def Cslib.LTS.«term_~[_]_» : Lean.TrailingParserDescr

Notation for homogeneous bisimilarity.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LTS.HomBisimilarity.refl {State : Type u_1} {Label✝ : Type u_2} {lts : LTS State Label✝} (s : State) : lts.HomBisimilarity s s

Homogeneous bisimilarity is reflexive.

theorem Cslib.LTS.IsBisimulation.inv {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} (h : lts₁.IsBisimulation lts₂ r) : lts₂.IsBisimulation lts₁ (flip r)

The inverse of a bisimulation is a bisimulation.

theorem Cslib.LTS.Bisimilarity.symm {State : Type u_1} {Label✝ : Type u_2} {lts₁ lts₂ : LTS State Label✝} {s₁ s₂ : State} (h : lts₁.Bisimilarity lts₂ s₁ s₂) : lts₂.Bisimilarity lts₁ s₂ s₁

Bisimilarity is symmetric.

theorem Cslib.LTS.IsBisimulation.comp {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r1 : State✝ → State✝¹ → Prop} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} {r2 : State✝¹ → State✝² → Prop} (h1 : lts₁.IsBisimulation lts₂ r1) (h2 : lts₂.IsBisimulation lts₃ r2) : lts₁.IsBisimulation lts₃ (Relation.Comp r1 r2)

The composition of two bisimulations is a bisimulation.

theorem Cslib.LTS.Bisimilarity.trans {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {s₁ : State✝} {s₂ : State✝¹} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} {s₃ : State✝²} (h1 : lts₁.Bisimilarity lts₂ s₁ s₂) (h2 : lts₂.Bisimilarity lts₃ s₂ s₃) : lts₁.Bisimilarity lts₃ s₁ s₃

Bisimilarity is transitive.

theorem Cslib.LTS.HomBisimilarity.eqv {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} : Equivalence lts.HomBisimilarity

Homogeneous bisimilarity is an equivalence relation.

instance Cslib.LTS.instIsEquivHomBisimilarity {State : Type u_1} {Label✝ : Type u_2} {lts : LTS State Label✝} : IsEquiv State lts.HomBisimilarity

theorem Cslib.LTS.IsBisimulation.sup {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r s : State✝ → State✝¹ → Prop} (hrb : lts₁.IsBisimulation lts₂ r) (hsb : lts₁.IsBisimulation lts₂ s) : lts₁.IsBisimulation lts₂ (r ⊔ s)

The union of two bisimulations is a bisimulation.

theorem Cslib.LTS.Bisimilarity.is_bisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : lts₁.IsBisimulation lts₂ (lts₁.Bisimilarity lts₂)

Bisimilarity is a bisimulation.

theorem Cslib.LTS.Bisimilarity.largest_bisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ lts₂ : LTS State✝ Label✝} {r : State✝ → State✝ → Prop} (h : lts₁.IsBisimulation lts₂ r) : Subrelation r (lts₁.Bisimilarity lts₂)

Bisimilarity is the largest bisimulation.

@[simp]

theorem Cslib.LTS.Bisimilarity.gfp {State₁ : Type u_1} {State₂ : Type u_2} {Label✝ : Type u_3} {lts₁ : LTS State₁ Label✝} {lts₂ : LTS State₂ Label✝} (r : State₁ → State₂ → Prop) (h : lts₁.IsBisimulation lts₂ r) : lts₁.Bisimilarity lts₂ ⊔ r = lts₁.Bisimilarity lts₂

The union of bisimilarity with any bisimulation is bisimilarity.

@[implicit_reducible]

instance Cslib.LTS.instTransBisimilarity {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} : Trans (lts₁.Bisimilarity lts₂) (lts₂.Bisimilarity lts₃) (lts₁.Bisimilarity lts₃)

calc support for bisimilarity.

Equations

• Cslib.LTS.instTransBisimilarity = { trans := ⋯ }

Order properties

@[implicit_reducible]

instance Cslib.LTS.instMaxSubtypeForallForallPropIsBisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : Max { r : State✝ → State✝¹ → Prop // lts₁.IsBisimulation lts₂ r }

Equations

• Cslib.LTS.instMaxSubtypeForallForallPropIsBisimulation = { max := fun (r s : { r : State✝¹ → State✝ → Prop // lts₁.IsBisimulation lts₂ r }) => ⟨↑r ⊔ ↑s, ⋯⟩ }

@[implicit_reducible]

instance Cslib.LTS.instSemilatticeSupSubtypeForallForallPropIsBisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : SemilatticeSup { r : State✝ → State✝¹ → Prop // lts₁.IsBisimulation lts₂ r }

Bisimulations equipped with union form a join-semilattice.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LTS.IsBisimulation.bot {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : lts₁.IsBisimulation lts₂ Relation.emptyHRelation

The empty (heterogeneous) relation is a bisimulation.

@[implicit_reducible]

instance Cslib.LTS.instBotSubtypeForallForallPropIsBisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : Bot { r : State✝ → State✝¹ → Prop // lts₁.IsBisimulation lts₂ r }

Equations

• Cslib.LTS.instBotSubtypeForallForallPropIsBisimulation = { bot := ⟨Relation.emptyHRelation, ⋯⟩ }

@[implicit_reducible]

instance Cslib.LTS.instTopSubtypeForallForallPropIsBisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : Top { r : State✝ → State✝¹ → Prop // lts₁.IsBisimulation lts₂ r }

Equations

• Cslib.LTS.instTopSubtypeForallForallPropIsBisimulation = { top := ⟨lts₁.Bisimilarity lts₂, ⋯⟩ }

@[implicit_reducible]

instance Cslib.LTS.instBoundedOrderSubtypeForallForallPropIsBisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : BoundedOrder { r : State✝ → State✝¹ → Prop // lts₁.IsBisimulation lts₂ r }

In the inclusion order on bisimulations:

• The empty relation is the bottom element.
• Bisimilarity is the top element.

Equations

• One or more equations did not get rendered due to their size.

Bisimulation up-to

def Cslib.LTS.UpToHomBisimilarity {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : State₁ → State₂ → Prop

Lifts a relation r to homogeneous bisimilarities on its types.

Equations

• lts₁.UpToHomBisimilarity lts₂ r = Relation.Comp lts₁.HomBisimilarity (Relation.Comp r lts₂.HomBisimilarity)

def Cslib.LTS.IsBisimulationUpTo {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop

A relation r is a bisimulation up to homogeneous bisimilarity if, whenever it relates two states in an lts, the transitions originating from these states mimic each other and the reached derivatives are themselves related by r up to bisimilarity.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LTS.IsBisimulationUpTo.is_bisimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} (h : lts₁.IsBisimulationUpTo lts₂ r) : lts₁.IsBisimulation lts₂ (lts₁.UpToHomBisimilarity lts₂ r)

Any bisimulation up to bisimilarity is a bisimulation.

theorem Cslib.LTS.IsBisimulation.bisim_trace {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} {s₁ : State✝} {s₂ : State✝¹} (hb : lts₁.IsBisimulation lts₂ r) (hr : r s₁ s₂) (μs : List Label✝) (s₁' : State✝) : lts₁.MTr s₁ μs s₁' → ∃ (s₂' : State✝¹), lts₂.MTr s₂ μs s₂' ∧ r s₁' s₂'

If two states are related by a bisimulation, they can mimic each other's multi-step transitions.

Relation to trace equivalence

theorem Cslib.LTS.IsBisimulation.traceEq {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} {s₁ : State✝} {s₂ : State✝¹} (hb : lts₁.IsBisimulation lts₂ r) (hr : r s₁ s₂) : lts₁.TraceEq lts₂ s₁ s₂

Any bisimulation implies trace equivalence.

theorem Cslib.LTS.Bisimilarity.le_traceEq {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} : lts₁.Bisimilarity lts₂ ≤ lts₁.TraceEq lts₂

Bisimilarity is included in trace equivalence.

theorem Cslib.LTS.IsBisimulation.traceEq_not_bisim : ∃ (State : Type) (Label : Type) (lts : LTS State Label), ¬lts.IsHomBisimulation lts.HomTraceEq

In general, trace equivalence is not a bisimulation (extra conditions are needed, see for example Bisimulation.deterministic_trace_eq_is_bisim).

theorem Cslib.LTS.Bisimilarity.bisimilarity_neq_traceEq : ∃ (State : Type) (Label : Type) (lts : LTS State Label), lts.HomBisimilarity ≠ lts.HomTraceEq

In general, bisimilarity and trace equivalence are distinct.

theorem Cslib.LTS.IsBisimulation.deterministic_traceEq_isBisimulation {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [lts₁.Deterministic] [lts₂.Deterministic] : lts₁.IsBisimulation lts₂ (lts₁.TraceEq lts₂)

In any deterministic LTS, trace equivalence is a bisimulation.

theorem Cslib.LTS.Bisimilarity.deterministic_traceEq_bisim {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {s₁ : State₁} {s₂ : State₂} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [lts₁.Deterministic] [lts₂.Deterministic] (h : lts₁.TraceEq lts₂ s₁ s₂) : lts₁.Bisimilarity lts₂ s₁ s₂

In deterministic LTSs, trace equivalence implies bisimilarity.

theorem Cslib.LTS.Bisimilarity.deterministic_bisim_eq_traceEq {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} [lts₁.Deterministic] [lts₂.Deterministic] : lts₁.Bisimilarity lts₂ = lts₁.TraceEq lts₂

In deterministic LTSs, bisimilarity and trace equivalence coincide.

Relation to simulation

theorem Cslib.LTS.IsBisimulation.isSimulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} : lts₁.IsBisimulation lts₂ r → lts₁.IsSimulation lts₂ r

Any bisimulation is also a simulation.

theorem Cslib.LTS.IsBisimulation.isSimulation_iff {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {r : State✝ → State✝¹ → Prop} : lts₁.IsBisimulation lts₂ r ↔ lts₁.IsSimulation lts₂ r ∧ lts₂.IsSimulation lts₁ (flip r)

A relation is a bisimulation iff both it and its inverse are simulations.

theorem Cslib.LTS.HomBisimilarity.symm_simulation {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} : lts.HomBisimilarity = fun (s₁ s₂ : State✝) => ∃ (r : State✝ → State✝ → Prop), r s₁ s₂ ∧ Std.Symm r ∧ lts.IsHomSimulation r

Homogeneous bisimilarity can also be characterized through symmetric simulations.

Weak bisimulation and weak bisimilarity

def Cslib.LTS.IsWeakBisimulation {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop

A weak bisimulation is similar to a Bisimulation, but allows for the related processes to do internal work. Technically, this is defined as a Bisimulation on the saturation of the LTSs.

Equations

• lts₁.IsWeakBisimulation lts₂ r = lts₁.saturate.IsBisimulation lts₂.saturate r

@[reducible, inline]

abbrev Cslib.LTS.IsHomWeakBisimulation {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) : Prop

A homogeneous bisimulation is a bisimulation where the underlying LTSs are the same.

Equations

• lts.IsHomWeakBisimulation = lts.IsWeakBisimulation lts

def Cslib.LTS.WeakBisimilarity {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop

Two states are weakly bisimilar if they are related by some weak bisimulation.

Equations

• lts₁.WeakBisimilarity lts₂ s₁ s₂ = ∃ (r : State₁ → State₂ → Prop), r s₁ s₂ ∧ lts₁.IsWeakBisimulation lts₂ r

def Cslib.LTS.«term_≈[_,_]_» : Lean.TrailingParserDescr

Notation for weak bisimilarity.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cslib.LTS.HomWeakBisimilarity {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : State → State → Prop

Homogeneous bisimilarity is bisimilarity where the underlying LTSs are the same.

Equations

• lts.HomWeakBisimilarity = lts.WeakBisimilarity lts

def Cslib.LTS.«term_≈[_]_» : Lean.TrailingParserDescr

Notation for homogeneous bisimilarity.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LTS.IsSWBisimulation {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop

An SWBisimulation is a more convenient definition of weak bisimulation, because the challenge is a single transition. We prove later that this technique is sound, following a strategy inspired by [Sangiorgi2011].

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LTS.IsSWBisimulation.follow_internal_fst {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} {r : State₁ → State₂ → Prop} {s₁ : State₁} {s₂ : State₂} {s₁' : State₁} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} (hswb : lts₁.IsSWBisimulation lts₂ r) (hr : r s₁ s₂) (hstr : lts₁.τSTr s₁ s₁') : ∃ (s₂' : State₂), lts₂.τSTr s₂ s₂' ∧ r s₁' s₂'

Utility theorem for 'following' internal transitions using an SWBisimulation (first component).

theorem Cslib.LTS.IsSWBisimulation.follow_internal_snd {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} {r : State₁ → State₂ → Prop} {s₁ : State₁} {s₂ s₂' : State₂} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} (hswb : lts₁.IsSWBisimulation lts₂ r) (hr : r s₁ s₂) (hstr : lts₂.τSTr s₂ s₂') : ∃ (s₁' : State₁), lts₁.τSTr s₁ s₁' ∧ r s₁' s₂'

Utility theorem for 'following' internal transitions using an SWBisimulation (second component).

theorem Cslib.LTS.isWeakBisimulation_iff_isSWBisimulation {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} {r : State₁ → State₂ → Prop} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} : lts₁.IsWeakBisimulation lts₂ r ↔ lts₁.IsSWBisimulation lts₂ r

We can now prove that any relation is a WeakBisimulation iff it is an SWBisimulation. This formalises lemma 4.2.10 in [Sangiorgi2011].

theorem Cslib.LTS.IsWeakBisimulation.isSwBisimulation {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {r : State₁ → State₂ → Prop} (h : lts₁.IsWeakBisimulation lts₂ r) : lts₁.IsSWBisimulation lts₂ r

theorem Cslib.LTS.IsSWBisimulation.isWeakBisimulation {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {r : State₁ → State₂ → Prop} (h : lts₁.IsSWBisimulation lts₂ r) : lts₁.IsWeakBisimulation lts₂ r

theorem Cslib.LTS.WeakBisimilarity.weakBisim_eq_swBisim {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} [HasTau Label] (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : lts₁.WeakBisimilarity lts₂ = fun (s₁ : State₁) (s₂ : State₂) => ∃ (r : State₁ → State₂ → Prop), r s₁ s₂ ∧ lts₁.IsSWBisimulation lts₂ r

Weak bisimilarity can also be characterized through sw-bisimulations.

theorem Cslib.LTS.HomWeakBisimilarity.refl {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} (s : State) : lts.HomWeakBisimilarity s s

Homogeneous weak bisimilarity is reflexive.

theorem Cslib.LTS.IsWeakBisimulation.inv {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} (r : State₁ → State₂ → Prop) (h : lts₁.IsWeakBisimulation lts₂ r) : lts₂.IsWeakBisimulation lts₁ (flip r)

The inverse of a weak bisimulation is a weak bisimulation.

theorem Cslib.LTS.WeakBisimilarity.symm {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} {s₁ : State₁} {s₂ : State₂} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} (h : lts₁.WeakBisimilarity lts₂ s₁ s₂) : lts₂.WeakBisimilarity lts₁ s₂ s₁

Weak bisimilarity is symmetric.

theorem Cslib.LTS.IsWeakBisimulation.comp {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} {State₃ : Type u_4} {r1 : State₁ → State₂ → Prop} {r2 : State₂ → State₃ → Prop} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} (h1 : lts₁.IsWeakBisimulation lts₂ r1) (h2 : lts₂.IsWeakBisimulation lts₃ r2) : lts₁.IsWeakBisimulation lts₃ (Relation.Comp r1 r2)

The composition of two weak bisimulations is a weak bisimulation.

theorem Cslib.LTS.IsSWBisimulation.comp {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} {State₃ : Type u_4} {r1 : State₁ → State₂ → Prop} {r2 : State₂ → State₃ → Prop} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} (h1 : lts₁.IsSWBisimulation lts₂ r1) (h2 : lts₂.IsSWBisimulation lts₃ r2) : lts₁.IsSWBisimulation lts₃ (Relation.Comp r1 r2)

The composition of two sw-bisimulations is an sw-bisimulation.

theorem Cslib.LTS.WeakBisimilarity.trans {Label : Type u_1} {State₁ : Type u_2} {State₂ : Type u_3} {State₃ : Type u_4} {s₁ : State₁} {s₂ : State₂} {s₃ : State₃} [HasTau Label] {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label} {lts₃ : LTS State₃ Label} (h1 : lts₁.WeakBisimilarity lts₂ s₁ s₂) (h2 : lts₂.WeakBisimilarity lts₃ s₂ s₃) : lts₁.WeakBisimilarity lts₃ s₁ s₃

Weak bisimilarity is transitive.

theorem Cslib.LTS.HomWeakBisimilarity.eqv {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} : Equivalence lts.HomWeakBisimilarity

Homogeneous weak bisimilarity is an equivalence relation.