From 3c14b03b3112baf2484847799ebaadc49b4c9c12 Mon Sep 17 00:00:00 2001 From: "Cuijpers, Pieter" Date: Sat, 11 Oct 2025 21:41:51 +0200 Subject: [PATCH 1/4] Introduction of left-saturation of an LTS and branching bisimulation definitions --- .../Semantics/LTS/Bisimulation.lean | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index bcf40bae..ebbaadac 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -1090,3 +1090,43 @@ theorem SWBisimilarity.eqv [HasTau Label] {lts : LTS State Label} : } end WeakBisimulation + +section BranchingBisimulation + +/-! ## Branching bisimulation and branching bisimilarity -/ + +/- This definition should be moved to LTS Basic eventually.-/ +/-- Left-Saturated transition relation. -/ +inductive LTS.LSTr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where +| refl : lts.LSTr s HasTau.τ s +| tr : lts.LSTr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.LSTr s1 μ s3 + +/-- A branching bisimulation is similar to a `WeakBisimulation` in that it allows for a saturation +of internal transitions, but it is a stronger equivalence in that it is able to distinguish +when internal work constitutes a choice. -/ +def LTS.IsBranchingBisimulation [HasTau Label] (lts : LTS State Label) + (r : State → State → Prop) := + ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, + /- In case of a transition on the left -/ + (∀ s1', lts.Tr s1 μ s1' → + /- A single tau transition can be mimicked by doing nothing. -/ + (μ = HasTau.τ ∧ ∃ s2', lts.LSTr s2 HasTau.τ s2' ∧ r s1 s2' ∧ r s1' s2') ∨ + /- Any transition (including tau's) can be mimicked by first doing a number of + tau's while relating to the original state (i.e. not making a choice yet), and + upon mimicking the label also relating to the new state. -/ + ∃ s2' s2'', lts.LSTr s2 HasTau.τ s2' ∧ r s1 s2' ∧ lts.Tr s2' μ s2'' ∧ r s1' s2'') + ∧ + /- The symmetric case of a transition on the right -/ + (∀ s2', lts.Tr s2 μ s2' → + (μ = HasTau.τ ∧ ∃ s1', lts.LSTr s1 HasTau.τ s1' ∧ r s1' s2 ∧ r s1' s2') ∨ + ∃ s1' s1'', lts.LSTr s1 HasTau.τ s1' ∧ r s1' s2 ∧ lts.Tr s1' μ s1'' ∧ r s1'' s2') + +/-- Two states are branching bisimilar if they are related by some branching bisimulation. -/ +def BranchingBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop := + fun s1 s2 => + ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsWeakBisimulation r + +/-- Notation for branching bisimilarity. -/ +notation s:max " ≈br[" lts "] " s':max => BranchingBisimilarity lts s s' + +end BranchingBisimulation From 17389e23dfdf009d6bd33e9fd720e5638c5ee723 Mon Sep 17 00:00:00 2001 From: "Cuijpers, Pieter" Date: Sat, 11 Oct 2025 21:59:19 +0200 Subject: [PATCH 2/4] Moved left-saturation to LTS.Basic, updated doc file --- Cslib/Foundations/Semantics/LTS/Basic.lean | 9 +++++++++ Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 13 +++++++------ 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 2176a77d..a7fd5a60 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -576,6 +576,15 @@ def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set S end Weak +section Branching + +/-- Left-Saturated transition relation. -/ +inductive LTS.LSTr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where +| refl : lts.LSTr s HasTau.τ s +| tr : lts.LSTr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.LSTr s1 μ s3 + +end Branching + /-! ## Divergence -/ section Divergence diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index ebbaadac..99b0d761 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -42,11 +42,18 @@ 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`. +- `lts.IsBranchingBisimulation r`: the relation `r` on the states of the LTS `lts` is a branching +bisimulation. +- `BranchingBisimilarity lts` is the binary relation on the states of `lts` that relates any two +states related by some branching 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`. +- `s1 ≈br[lts] s2`: the states `s1` and `s2` are branching bisimilar in the LTS `lts`. ## Main statements @@ -1095,12 +1102,6 @@ section BranchingBisimulation /-! ## Branching bisimulation and branching bisimilarity -/ -/- This definition should be moved to LTS Basic eventually.-/ -/-- Left-Saturated transition relation. -/ -inductive LTS.LSTr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where -| refl : lts.LSTr s HasTau.τ s -| tr : lts.LSTr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.LSTr s1 μ s3 - /-- A branching bisimulation is similar to a `WeakBisimulation` in that it allows for a saturation of internal transitions, but it is a stronger equivalence in that it is able to distinguish when internal work constitutes a choice. -/ From 15685df248a8a50213a4367ac97e6e0369edb65e Mon Sep 17 00:00:00 2001 From: "Cuijpers, Pieter" Date: Sun, 12 Oct 2025 22:29:13 +0200 Subject: [PATCH 3/4] Removed definition of LSTr since it is equivalent to STr for tau. Updated definition of Branching Bisimulation to match [DeNicolaVaandrager-Three Logics for Branching Bisimulation] --- Cslib/Foundations/Semantics/LTS/Basic.lean | 9 --------- Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 12 ++++++------ 2 files changed, 6 insertions(+), 15 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index a7fd5a60..2176a77d 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -576,15 +576,6 @@ def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set S end Weak -section Branching - -/-- Left-Saturated transition relation. -/ -inductive LTS.LSTr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where -| refl : lts.LSTr s HasTau.τ s -| tr : lts.LSTr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.LSTr s1 μ s3 - -end Branching - /-! ## Divergence -/ section Divergence diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 99b0d761..116d3505 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -1111,21 +1111,21 @@ def LTS.IsBranchingBisimulation [HasTau Label] (lts : LTS State Label) /- In case of a transition on the left -/ (∀ s1', lts.Tr s1 μ s1' → /- A single tau transition can be mimicked by doing nothing. -/ - (μ = HasTau.τ ∧ ∃ s2', lts.LSTr s2 HasTau.τ s2' ∧ r s1 s2' ∧ r s1' s2') ∨ - /- Any transition (including tau's) can be mimicked by first doing a number of + (μ = HasTau.τ ∧ r s1' s2) ∨ + /- And transition (including tau's) can be mimicked by first doing a number of tau's while relating to the original state (i.e. not making a choice yet), and upon mimicking the label also relating to the new state. -/ - ∃ s2' s2'', lts.LSTr s2 HasTau.τ s2' ∧ r s1 s2' ∧ lts.Tr s2' μ s2'' ∧ r s1' s2'') + ∃ s2' s2'', lts.STr s2 HasTau.τ s2' ∧ lts.Tr s2' μ s2'' ∧ r s1 s2' ∧ r s1' s2'') ∧ /- The symmetric case of a transition on the right -/ (∀ s2', lts.Tr s2 μ s2' → - (μ = HasTau.τ ∧ ∃ s1', lts.LSTr s1 HasTau.τ s1' ∧ r s1' s2 ∧ r s1' s2') ∨ - ∃ s1' s1'', lts.LSTr s1 HasTau.τ s1' ∧ r s1' s2 ∧ lts.Tr s1' μ s1'' ∧ r s1'' s2') + (μ = HasTau.τ ∧ r s1 s2') ∨ + ∃ s1' s1'', lts.STr s1 HasTau.τ s1' ∧ lts.Tr s1' μ s1'' ∧ r s1' s2 ∧ r s1'' s2') /-- Two states are branching bisimilar if they are related by some branching bisimulation. -/ def BranchingBisimilarity [HasTau Label] (lts : LTS State Label) : State → State → Prop := fun s1 s2 => - ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsWeakBisimulation r + ∃ r : State → State → Prop, r s1 s2 ∧ lts.IsBranchingBisimulation r /-- Notation for branching bisimilarity. -/ notation s:max " ≈br[" lts "] " s':max => BranchingBisimilarity lts s s' From aec7f125601e1980d897a20320d7caa7a222fde5 Mon Sep 17 00:00:00 2001 From: "Cuijpers, Pieter" Date: Mon, 13 Oct 2025 17:15:24 +0200 Subject: [PATCH 4/4] Updated comment with reference to original definition. --- Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index 116d3505..d4dd5faf 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -1104,7 +1104,11 @@ section BranchingBisimulation /-- A branching bisimulation is similar to a `WeakBisimulation` in that it allows for a saturation of internal transitions, but it is a stronger equivalence in that it is able to distinguish -when internal work constitutes a choice. -/ +when internal work constitutes a choice. There are several (equivalent) definitions used in +literature. The original one can be found in [R.J. van Glabbeek and W.P. Weijland, +"Branching Time and Abstraction in Bisimulation Semantics", 1990]. But we follow the slightly +more popular definition of [de Nicola and Vaandrager, 1995, https://doi.org/10.1145/201019.201032]. +-/ def LTS.IsBranchingBisimulation [HasTau Label] (lts : LTS State Label) (r : State → State → Prop) := ∀ ⦃s1 s2⦄, r s1 s2 → ∀ μ, @@ -1112,9 +1116,9 @@ def LTS.IsBranchingBisimulation [HasTau Label] (lts : LTS State Label) (∀ s1', lts.Tr s1 μ s1' → /- A single tau transition can be mimicked by doing nothing. -/ (μ = HasTau.τ ∧ r s1' s2) ∨ - /- And transition (including tau's) can be mimicked by first doing a number of - tau's while relating to the original state (i.e. not making a choice yet), and - upon mimicking the label also relating to the new state. -/ + /- Any transition can be mimicked by first performing a number of + τ transitions while relating to the original state, and then mimicking + the intended transition. -/ ∃ s2' s2'', lts.STr s2 HasTau.τ s2' ∧ lts.Tr s2' μ s2'' ∧ r s1 s2' ∧ r s1' s2'') ∧ /- The symmetric case of a transition on the right -/