Please write your solutions as clearly and concisely as possible.

1. (30 pts) For each of the following pairs of processes P and Q, say whether they are strongly / weakly bisimilar or not. Justify your answer.

   1. P =def= a.0 + a.P , Q =def= a.(0 + Q)
   2. P =def= a.0 + tau.P , Q =def= a.0
   3. P =def= a.(P | P) , Q =def= a.a.Q
   4. P =def= a.tau.c.0 + a.tau.d.0 , Q =def= a.(tau.c.0 + tau.d.0)
   5. P =def= a.R | ^a.0 , Q =def= a.^a.R + ^a.a.R + tau.R
   

   In the last pair, ^a represents the action complementary to a. (according to our convension, a is input and ^a is output).

2. (20 pts) Consider the following specification of a two-position buffer:

      B2 =def= in.B1
      B1 =def= in.B0 + ^out.B2
      B0 =def= ^out.B1
   

   Consider now the implementation of a two-position FIFO buffer by using two one-position buffers, serialized, and communicating via the adjacent ports:

      C =def= (B[out|->a] | B[in|->a])\{a}
   

   where B is defined as follows:

      B =def= in.^out.B
   

   Say whether B2 and C are strongly / weakly bisimilar or not. Justify your answer.

3. (50 pts) Prove that strong bisimulation is closed wrt the operators of CCS (i.e. it's a congruence). Namely, prove that, if P is strongly bisimilar to Q, then
   1. a.P is strongly bisimilar to a.Q
   2. P + R is strongly bisimilar to Q + R
   3. P | R is strongly bisimilar to Q | R
   4. P\L is strongly bisimilar to Q\L
   5. P[f] is strongly bisimilar to Q[f]

   Note: for the fixpoint operator, the property of preserving bisimulation has a more complicated formulation. We will not consider it here.