I have a question for anyone who happens to know: are bisimulations more common in process calculi such as the π-calculus because of τ transitions?
Lately I've been proving some simulation theorems for λ calculi, and none of them is a bisimulation; there are too many "administrative" reductions in the implementation semantics, so it's not possible to guarantee that every one-step reduction in the implementation semantics corresponds to a reduction sequence in the specification semantics.
Now, it's been a while since I looked at the π-calculus, but I seem to recall that you can hide a sequence of reductions inside a "black box" and call them a single transition τ. I suspect this facility allows you to pretend a sequence of transitions is a single transition in order to hide the details of an implementation semantics, effectively producing a completely indistinguishable simulation.
(This is admittedly all a little vague since my knowledge of bisimulations is scant.)
Subscribe to:
Post Comments (Atom)
4 comments:
In the \pi-calculus, there is a notion of weak bisimulation where \tau-transtions are abstracted away. Weak bisimulation are bisimulations for the relation: -\tau->* -\alpha-> -\tau->*.
tau transitions can be seen as not observable internal transitions.
Barbed bisimulation might be the creature you are after.
Yes, I too think that you're looking for the weak bisimulation or the ground one..
As far as I remember the weak works like :
t standing for "tau" and "l" for any other label
t,t,...,t,l,t,t....
And the ground :
t,t,...,l
P!
+1
Post a Comment