Fall 98, CSE 520: Solution of Assignment 4
Exercise 1
- neither strongly nor weakly bisimilar
- weakly bisimilar, not strongly bisimilar
- strongly (and weakly) bisimilar
- neither strongly nor weakly bisimilar
- neither strongly nor weakly bisimilar. This last exercise was a bit
misleading, because P =def= a.R | a^.0 is strongly bisimilar to
the process Q' =def= a.((a^.0)|R) + a^.a.R + tau.R.
For this reason, I gave only a penalty of 1 point to those who
gave the answer "strongly bisimilar" here.
Exercise 2
The new system is weakly bisimilar to a 2-cell (ordered) buffer.
Exercise 3
- In CCS, one possible definition is:
[[ tau.P + tau.Q ]] = ( a^.0 | a.[[P]] | a.[[Q]] )\{a}
- In the pi-calculus, one possible definition is:
[[ tau.P + tau.Q ]] = (a)( a^x.0 | a(x).[[P]] | a(x).[[Q]] )
We assume the names "a" and "x" not to occur free in P and Q.
Exercise 4
A possible solution is:
[[ x^y.P ]] = (a)(x^a | a(w).(w^y | [[P]] ))
[[ x(z).Q ]] = (b)(x(v).(v^b | b(z).[[P]] ))