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

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

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

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

• WeakBisimulation lts 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.

• SWBisimulation lts 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

• Bisimulation.inv: the inverse of a bisimulation is a bisimulation.
• Bisimilarity.eqv: bisimilarity is an equivalence relation (see Equivalence).
• Bisimilarity.is_bisimulation: 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.
• Bisimulation.upTo_bisimulation: any bisimulation up to bisimilarity is a bisimulation.
• Bisimulation.bisim_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 Bisimulation {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) : 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.

def Bisimulation.follow_fst {State : Type u} {Label : Type v} {s1 s2 s1' : State} {lts : LTS State Label} {r : Rel State State} (hb : Bisimulation lts r) (hr : r s1 s2) (μ : Label) (htr : lts.tr s1 μ s1') : ∃ (s2' : State), lts.tr s2 μ s2' ∧ r s1' s2'

Helper for following a transition using the first component of a Bisimulation.

Equations

• ⋯ = ⋯

def Bisimulation.follow_snd {State : Type u} {Label : Type v} {s1 s2 s2' : State} {lts : LTS State Label} {r : Rel State State} (hb : Bisimulation lts r) (hr : r s1 s2) (μ : Label) (htr : lts.tr s2 μ s2') : ∃ (s1' : State), lts.tr s1 μ s1' ∧ r s1' s2'

Helper for following a transition using the second component of a Bisimulation.

Equations

• ⋯ = ⋯

def Bisimilarity {State : Type u} {Label : Type v} (lts : LTS State Label) : Rel State State

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

Equations

• s1 ~[lts] s2 = ∃ (r : Rel State State), r s1 s2 ∧ Bisimulation lts r

def «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 Bisimilarity.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : s ~[lts] s

Bisimilarity is reflexive.

theorem Bisimulation.inv {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) (h : Bisimulation lts r) : Bisimulation lts r.inv

The inverse of a bisimulation is a bisimulation.

theorem 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 Bisimulation.comp {State : Type u} {Label : Type v} (lts : LTS State Label) (r1 r2 : Rel State State) (h1 : Bisimulation lts r1) (h2 : Bisimulation lts r2) : Bisimulation lts (r1.comp r2)

The composition of two bisimulations is a bisimulation.

theorem 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 Bisimilarity.eqv {State : Type u} {Label : Type v} (lts : LTS State Label) : Equivalence (Bisimilarity lts)

Bisimilarity is an equivalence relation.

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

Bisimilarity is a bisimulation.

theorem Bisimilarity.largest_bisimulation {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) (h : Bisimulation lts r) (s1 s2 : State) : r s1 s2 → s1 ~[lts] s2

Bisimilarity is the largest bisimulation.

theorem Bisimilarity.gfp {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) (h : Bisimulation lts r) : (Bisimilarity lts).union r = Bisimilarity lts

The union of bisimilarity with any bisimulation is bisimilarity.

def BisimulationUpTo {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) : 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 Bisimulation.upTo_bisimulation {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) (h : BisimulationUpTo lts r) : Bisimulation lts (r.upTo (Bisimilarity lts))

Any bisimulation up to bisimilarity is a bisimulation.

theorem Bisimulation.bisim_trace {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 s2 : State) (r : Rel State State) (hb : Bisimulation lts 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 Bisimulation.bisim_traceEq {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 s2 : State) (r : Rel State State) (hb : Bisimulation lts r) (hr : r s1 s2) : s1 ~tr[lts] s2

Any bisimulation implies trace equivalence.

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

Bisimilarity implies trace equivalence.

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

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

theorem 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 Bisimulation.deterministic_traceEq_is_bisim {State : Type u} {Label : Type v} (lts : LTS State Label) (hdet : lts.Deterministic) : Bisimulation lts (TraceEq lts)

In any deterministic LTS, trace equivalence is a bisimulation.

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

In any deterministic LTS, trace equivalence implies bisimilarity.

theorem Bisimilarity.deterministic_bisim_eq_traceEq {State : Type u} {Label : Type v} (lts : LTS State Label) (hdet : lts.Deterministic) : Bisimilarity lts = TraceEq lts

In any deterministic LTS, bisimilarity and trace equivalence coincide.

Relation to simulation

theorem Bisimulation.is_simulation {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) : Bisimulation lts r → Simulation lts r

Any bisimulation is also a simulation.

theorem Bisimulation.simulation_iff {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) : Bisimulation lts r ↔ Simulation lts r ∧ Simulation lts r.inv

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

Weak bisimulation and weak bisimilarity

def WeakBisimulation {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r : Rel State State) : 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

• WeakBisimulation lts r = Bisimulation lts.saturate r

def WeakBisimilarity {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : Rel State State

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

Equations

• s1 ≈[lts] s2 = ∃ (r : Rel State State), r s1 s2 ∧ WeakBisimulation lts r

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

Notation for weak bisimilarity.

Equations

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

def SWBisimulation {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r : Rel State State) : 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 SWBisimilarity {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : Rel State State

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

Equations

• s1 ≈sw[lts] s2 = ∃ (r : Rel State State), r s1 s2 ∧ SWBisimulation lts r

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

Notation for swbisimilarity.

Equations

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

@[irreducible]

theorem SWBisimulation.follow_internal_fst_n {Label : Type u_1} {State : Type u_2} {s1 s2 : State} {n : ℕ} {s1' : State} [HasTau Label] (lts : LTS State Label) (r : Rel State State) (hswb : SWBisimulation lts 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 SWBisimulation.follow_internal_snd_n {Label : Type u_1} {State : Type u_2} {s1 s2 : State} {n : ℕ} {s2' : State} [HasTau Label] (lts : LTS State Label) (r : Rel State State) (hswb : SWBisimulation lts 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 SWBisimulation.follow_internal_fst {Label : Type u_1} {State : Type u_2} {s1 s2 s1' : State} [HasTau Label] (lts : LTS State Label) (r : Rel State State) (hswb : SWBisimulation lts 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 SWBisimulation.follow_internal_snd {Label : Type u_1} {State : Type u_2} {s1 s2 s2' : State} [HasTau Label] (lts : LTS State Label) (r : Rel State State) (hswb : SWBisimulation lts 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 WeakBisimulation.iff_swBisimulation {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r : Rel State State) : WeakBisimulation lts r ↔ SWBisimulation lts 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 WeakBisimulation.toSwBisimulation {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {r : Rel State State} (h : WeakBisimulation lts r) : SWBisimulation lts r

theorem SWBisimulation.toWeakBisimulation {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {r : Rel State State} (h : SWBisimulation lts r) : WeakBisimulation lts r

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

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

theorem 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 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 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 SWBisimulation.inv {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r : Rel State State) (h : SWBisimulation lts r) : SWBisimulation lts r.inv

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

theorem WeakBisimulation.inv {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r : Rel State State) (h : WeakBisimulation lts r) : WeakBisimulation lts r.inv

The inverse of a weak bisimulation is a weak bisimulation.

theorem 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 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 WeakBisimulation.comp {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r1 r2 : Rel State State) (h1 : WeakBisimulation lts r1) (h2 : WeakBisimulation lts r2) : WeakBisimulation lts (r1.comp r2)

The composition of two weak bisimulations is a weak bisimulation.

theorem SWBisimulation.comp {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (r1 r2 : Rel State State) (h1 : SWBisimulation lts r1) (h2 : SWBisimulation lts r2) : SWBisimulation lts (r1.comp r2)

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

theorem 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 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 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 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.