Skip to content

feat: definition branching bisimulation #94

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

feat: definition branching bisimulation #94

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3c14b03
Introduction of left-saturation of an LTS and branching bisimulation …
PieterCuijpers Oct 11, 2025
17389e2
Moved left-saturation to LTS.Basic, updated doc file
PieterCuijpers Oct 11, 2025
15685df
Removed definition of LSTr since it is equivalent to STr for tau. Upd…
PieterCuijpers Oct 12, 2025
aec7f12
Updated comment with reference to original definition.
PieterCuijpers Oct 13, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions Cslib/Foundations/Semantics/LTS/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
41 changes: 41 additions & 0 deletions Cslib/Foundations/Semantics/LTS/Bisimulation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -1090,3 +1097,37 @@ theorem SWBisimilarity.eqv [HasTau Label] {lts : LTS State Label} :
}

end WeakBisimulation

section BranchingBisimulation

/-! ## Branching bisimulation and branching bisimilarity -/

/-- 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') ∨
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you have a reference for this? The one I've found uses Tr, not LStr here: https://ir.cwi.nl/pub/1370/1370D.pdf

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, that's interesting. I know there are several different definitions going around.
But looking at it better, since the only use of LSTr is on tau, it is equivalent to STr.
So I think the LSTr definition is indeed not needed.

I'll do a bit of digging to see which is the most appropriate.
I think I'll just mail Rob van Glabbeek for advice :-)

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I took mine from: https://evink.win.tue.nl/education/2it70/PDF2016/2it70-chap5.pdf
But your reference is better, I think. And the definition is also a bit shorter.

I have a doubt though.
While the use of STr is "nice" in the sence that it matches what you've used for weak bisimulation,
the condition of having tau's "before and after" may lead to a lot of case distinctions in proofs that are essentially unnecessary. Will we have to resolve those simply by introducing appropriate theorems? Or can we avoid that by making the right choices now?

I think that question is also at the heart of different - essentially equivalent - definitions of branching bisimulation popping up in different places. The proofs go smoother if you take one instead of the other, but I don't know which is which.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've tried a few more sources:

[R.J.van Glabbeek and W.P.Weijland, "Branching Time and Abstraction in Bisimulation Semantics", 1990]
If R(r, s) and r --a--> r’, then either a = τ and R(r’, s), or there exists a
path s => s1 --a--> s2 => s’ such that R(r, s1), R(r’, s2) and R(r’, s’).

[R.J. van Glabbeek, "The Linear Time - Branching Time Spectrum II", CONCUR 1993]
if pRq and p -a-> p' then there exists q", q' s.t. q=>q" and ((a = τ and q" = q') V q" -a-> q')
and pRq" and p'Rq'

[R.de Nicola and F. Vaandrager, "Three Logics for Branching Bisimulation", 1995]
If R(r, s) and r --a--> r’, then either a = τ and R(r’, s), or there exists a
path s => s1 --a--> s’ such that R(r, s1) and R(r’, s’).

The one in [deVink]'s lecture notes - which I used in my first commit - is, arguably, unnecessarily complicated.
It is also not popular in other works I've encountered during my scan.
Most seem to go for the Nicola Vaandrager variant, which you also found.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the overview!
I'd define a relation for that s => s1, since it can be made very simple (refl and stepL cases). I don't have a good name to suggest right now though, as I'm not aware of people normally giving this relation a name in papers... :-) Ideas?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed. I started out reusing what is there, but I also felt that it was overcomplicating things.
I noticed there is a \tauClosure already, which then also can be cleaned up.
Maybe just LTS.\tauSteps or LTS.\tauSTr?

Should we discuss the naming on Zulip?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In order to introduce that properly, I'm tempted to also change the definition of LTS.STr... but that has implications downstream everywhere on the weak definitions. I'm willing to make the change, but that needs backup...

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Moved this to Zulip...

/- 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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be IsBranchingBisimulation


/-- Notation for branching bisimilarity. -/
notation s:max " ≈br[" lts "] " s':max => BranchingBisimilarity lts s s'

end BranchingBisimulation