feat: definition branching bisimulation #94
Conversation
| /- 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') ∨ |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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 :-)
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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...
| /-- 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 |
There was a problem hiding this comment.
Should be IsBranchingBisimulation
…ated definition of Branching Bisimulation to match [DeNicolaVaandrager-Three Logics for Branching Bisimulation]
2 participants
Added a definition of left-saturated transition LTS.LSTr to LTS.basic,
and a definition of branching bisimulation to LTS.bisimulation