Bisimulation and Bisimilarity

A bisimulation is a binary relation on the states of an LTS, which establishes a tight semantic correspondence. More specifically, if two states s1 and s2 are related by a bisimulation, then s1 can mimic all transitions of s2 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 [San].

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.

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

Notations

• s1 ~[lts] s2: the states s1 and s2 are bisimilar in the LTS lts.
• s1 ≈[lts] s2: the states s1 and s2 are weakly bisimilar in the LTS lts.
• s1 ≈sw[lts] s2: the states s1 and s2 are sw 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.
• WeakBisimilarity.weakBisim_eq_swBisim: weak bisimilarity and sw-bisimilarity coincide in all LTSs.
• WeakBisimilarity.eqv: weak bisimilarity is an equivalence relation.
• SWBisimilarity.eqv: sw-bisimilarity is an equivalence relation.

def Cslib.LTS.IsBisimulation {State : Type u} {Label : Type v} (lts : LTS State Label) (r : State → State → Prop) : Prop

A relation is a bisimulation 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.

Equations

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

theorem Cslib.LTS.IsBisimulation.follow_fst {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} {s1 s2 : State} {μ : Label} {s1' : State} (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s1 μ s1') : ∃ (s2' : State), lts.Tr s2 μ s2' ∧ r s1' s2'

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

theorem Cslib.LTS.IsBisimulation.follow_snd {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} {s1 s2 : State} {μ : Label} {s2' : State} (hb : lts.IsBisimulation r) (hr : r s1 s2) (htr : lts.Tr s2 μ s2') : ∃ (s1' : State), lts.Tr s1 μ s1' ∧ r s1' s2'

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

def Cslib.Bisimilarity {State : Type u} {Label : Type v} (lts : LTS State Label) : State → State → Prop

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

Equations

• s1 ~[lts] s2 = ∃ (r : State → State → Prop), r s1 s2 ∧ lts.IsBisimulation r

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

Notation for bisimilarity.

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

Equations

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

theorem Cslib.Bisimilarity.refl {State : Type u} {Label : Type v} {lts : LTS State Label} (s : State) : s ~[lts] s

Bisimilarity is reflexive.

theorem Cslib.LTS.IsBisimulation.inv {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsBisimulation r) : lts.IsBisimulation (flip r)

The inverse of a bisimulation is a bisimulation.

theorem Cslib.Bisimilarity.symm {State : Type u} {Label : Type v} {lts : LTS State Label} {s1 s2 : State} (h : s1 ~[lts] s2) : s2 ~[lts] s1

Bisimilarity is symmetric.

theorem Cslib.LTS.IsBisimulation.comp {State : Type u} {Label : Type v} {lts : LTS State Label} {r1 r2 : State → State → Prop} (h1 : lts.IsBisimulation r1) (h2 : lts.IsBisimulation r2) : lts.IsBisimulation (Relation.Comp r1 r2)

The composition of two bisimulations is a bisimulation.

theorem Cslib.Bisimilarity.trans {State : Type u} {Label : Type v} {lts : LTS State Label} {s1 s2 s3 : State} (h1 : s1 ~[lts] s2) (h2 : s2 ~[lts] s3) : s1 ~[lts] s3

Bisimilarity is transitive.

theorem Cslib.Bisimilarity.eqv {State : Type u} {Label : Type v} {lts : LTS State Label} : Equivalence (Bisimilarity lts)

Bisimilarity is an equivalence relation.

theorem Cslib.Bisimulation.union {State : Type u} {Label : Type v} {lts : LTS State Label} {r s : State → State → Prop} (hrb : lts.IsBisimulation r) (hsb : lts.IsBisimulation s) : lts.IsBisimulation (r ⊔ s)

The union of two bisimulations is a bisimulation.

theorem Cslib.Bisimilarity.is_bisimulation {State : Type u} {Label : Type v} {lts : LTS State Label} : lts.IsBisimulation (Bisimilarity lts)

Bisimilarity is a bisimulation.

theorem Cslib.Bisimilarity.largest_bisimulation {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsBisimulation r) : Subrelation r (Bisimilarity lts)

Bisimilarity is the largest bisimulation.

@[simp]

theorem Cslib.Bisimilarity.gfp {State : Type u} {Label : Type v} {lts : LTS State Label} (r : State → State → Prop) (h : lts.IsBisimulation r) : Bisimilarity lts ⊔ r = Bisimilarity lts

The union of bisimilarity with any bisimulation is bisimilarity.

instance Cslib.instTransBisimilarity {State : Type u} {Label : Type v} {lts : LTS State Label} : Trans (Bisimilarity lts) (Bisimilarity lts) (Bisimilarity lts)

calc support for bisimilarity.

Equations

• Cslib.instTransBisimilarity = { trans := ⋯ }

Order properties

instance Cslib.instMaxSubtypeForallForallPropIsBisimulation {State : Type u} {Label : Type v} {lts : LTS State Label} : Max { r : State → State → Prop // lts.IsBisimulation r }

Equations

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

instance Cslib.instSemilatticeSupSubtypeForallForallPropIsBisimulation {State : Type u} {Label : Type v} {lts : LTS State Label} : SemilatticeSup { r : State → State → Prop // lts.IsBisimulation r }

Bisimulations equipped with union form a join-semilattice.

Equations

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

theorem Cslib.Bisimulation.emptyRelation_bisimulation {State : Type u} {Label : Type v} {lts : LTS State Label} : lts.IsBisimulation emptyRelation

The empty relation is a bisimulation.

instance Cslib.instBoundedOrderSubtypeForallForallPropIsBisimulation {State : Type u} {Label : Type v} {lts : LTS State Label} : BoundedOrder { r : State → State → Prop // lts.IsBisimulation r }

In the inclusion order on bisimulations:

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

Equations

• Cslib.instBoundedOrderSubtypeForallForallPropIsBisimulation = { top := ⟨Cslib.Bisimilarity lts, ⋯⟩, le_top := ⋯, bot := ⟨emptyRelation, ⋯⟩, bot_le := ⋯ }

Bisimulation up-to

def Cslib.LTS.IsBisimulationUpTo {State : Type u} {Label : Type v} (lts : LTS State Label) (r : State → State → Prop) : Prop

A relation r is a bisimulation up to 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.isBisimulation {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} (h : lts.IsBisimulationUpTo r) : lts.IsBisimulation (Relation.UpTo r (Bisimilarity lts))

Any bisimulation up to bisimilarity is a bisimulation.

theorem Cslib.Bisimulation.bisim_trace {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} {s1 s2 : State} (hb : lts.IsBisimulation r) (hr : r s1 s2) (μs : List Label) (s1' : State) : lts.MTr s1 μs s1' → ∃ (s2' : State), lts.MTr s2 μs s2' ∧ r s1' s2'

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} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} {s1 s2 : State} (hb : lts.IsBisimulation r) (hr : r s1 s2) : s1 ~tr[lts] s2

Any bisimulation implies trace equivalence.

theorem Cslib.Bisimilarity.le_traceEq {State : Type u} {Label : Type v} {lts : LTS State Label} : Bisimilarity lts ≤ TraceEq lts

Bisimilarity is included in trace equivalence.

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

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

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

In general, bisimilarity and trace equivalence are distinct.

theorem Cslib.Bisimulation.deterministic_traceEq_is_bisim {State : Type u} {Label : Type v} {lts : LTS State Label} [lts.Deterministic] : lts.IsBisimulation (TraceEq lts)

In any deterministic LTS, trace equivalence is a bisimulation.

theorem Cslib.Bisimilarity.deterministic_traceEq_bisim {State : Type u} {Label : Type v} {lts : LTS State Label} {s1 s2 : State} [lts.Deterministic] (h : s1 ~tr[lts] s2) : s1 ~[lts] s2

In any deterministic LTS, trace equivalence implies bisimilarity.

theorem Cslib.Bisimilarity.deterministic_bisim_eq_traceEq {State : Type u} {Label : Type v} {lts : LTS State Label} [lts.Deterministic] : Bisimilarity lts = TraceEq lts

In any deterministic LTS, bisimilarity and trace equivalence coincide.

Relation to simulation

theorem Cslib.Bisimulation.is_simulation {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} : lts.IsBisimulation r → Simulation lts r

Any bisimulation is also a simulation.

theorem Cslib.Bisimulation.simulation_iff {State : Type u} {Label : Type v} {lts : LTS State Label} {r : State → State → Prop} : lts.IsBisimulation r ↔ Simulation lts r ∧ Simulation lts (flip r)

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

Weak bisimulation and weak bisimilarity

def Cslib.LTS.IsWeakBisimulation {Label : Type u_1} {State : Type u_2} [HasTau 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 LTS.

Equations

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

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

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

Equations

• s1 ≈[lts] s2 = ∃ (r : State → State → Prop), r s1 s2 ∧ lts.IsWeakBisimulation r

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

Notation for weak 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} [HasTau 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 [San].

Equations

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

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

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

Equations

• s1 ≈sw[lts] s2 = ∃ (r : State → State → Prop), r s1 s2 ∧ lts.IsSWBisimulation r

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

Notation for swbisimilarity.

Equations

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

@[irreducible]

theorem Cslib.SWBisimulation.follow_internal_fst_n {Label : Type u_1} {State : Type u_2} {r : State → State → Prop} {s1 s2 : State} {n : ℕ} {s1' : State} [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s1 HasTau.τ s1') : ∃ (s2' : State), lts.STr s2 HasTau.τ s2' ∧ r s1' s2'

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

@[irreducible]

theorem Cslib.SWBisimulation.follow_internal_snd_n {Label : Type u_1} {State : Type u_2} {r : State → State → Prop} {s1 s2 : State} {n : ℕ} {s2' : State} [HasTau Label] {lts : LTS State Label} (hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s2 HasTau.τ s2') : ∃ (s1' : State), lts.STr s1 HasTau.τ s1' ∧ r s1' s2'

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

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

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

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

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} {r : State → State → Prop} [HasTau Label] {lts : LTS State Label} : lts.IsWeakBisimulation r ↔ lts.IsSWBisimulation r

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

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

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

theorem Cslib.WeakBisimilarity.by_swBisimulation {Label : Type u_1} {State : Type u_2} {s1 s2 : State} [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) (hb : lts.IsSWBisimulation r) (hr : r s1 s2) : s1 ≈[lts] s2

If two states are related by an SWBisimulation, then they are weakly bisimilar.

theorem Cslib.WeakBisimilarity.weakBisim_eq_swBisim {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : WeakBisimilarity lts = SWBisimilarity lts

Weak bisimilarity and sw-bisimilarity coincide for all LTSs.

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

sw-bisimilarity is reflexive.

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

Weak bisimilarity is reflexive.

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

The inverse of an sw-bisimulation is an sw-bisimulation.

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

The inverse of a weak bisimulation is a weak bisimulation.

theorem Cslib.SWBisimilarity.symm {Label : Type u_1} {State : Type u_2} {s1 s2 : State} [HasTau Label] (lts : LTS State Label) (h : s1 ≈sw[lts] s2) : s2 ≈sw[lts] s1

sw-bisimilarity is symmetric.

theorem Cslib.WeakBisimilarity.symm {Label : Type u_1} {State : Type u_2} {s1 s2 : State} [HasTau Label] (lts : LTS State Label) (h : s1 ≈[lts] s2) : s2 ≈[lts] s1

Weak bisimilarity is symmetric.

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

The composition of two weak bisimulations is a weak bisimulation.

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

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

theorem Cslib.WeakBisimilarity.trans {Label : Type u_1} {State : Type u_2} [HasTau Label] {s1 s2 s3 : State} (lts : LTS State Label) (h1 : s1 ≈[lts] s2) (h2 : s2 ≈[lts] s3) : s1 ≈[lts] s3

Weak bisimilarity is transitive.

theorem Cslib.SWBisimilarity.trans {Label : Type u_1} {State : Type u_2} [HasTau Label] {s1 s2 s3 : State} (lts : LTS State Label) (h1 : s1 ≈sw[lts] s2) (h2 : s2 ≈sw[lts] s3) : s1 ≈sw[lts] s3

sw-bisimilarity is transitive.

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

Weak bisimilarity is an equivalence relation.

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

SW-bisimilarity is an equivalence relation.