Fall 98, CSE 520: Solution of Assignment 4

Exercise 1

  1. neither strongly nor weakly bisimilar
  2. weakly bisimilar, not strongly bisimilar
  3. strongly (and weakly) bisimilar
  4. neither strongly nor weakly bisimilar
  5. 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

  1. In CCS, one possible definition is:
    [[ tau.P + tau.Q ]] = ( a^.0 | a.[[P]] | a.[[Q]] )\{a}
  2. 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]] ))