Sunday, March 25, 2007

Bisimulation bleg

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


Anonymous said...

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.

Anonymous said...

Barbed bisimulation might be the creature you are after.

Anonymous said...

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

And the ground :


Anonymous said...