Please write your solutions as clearly and concisely as possible.

1. (40 pts) For each of the following definitions of the CCS process P, draw the transition graph of the process (the nodes of the graph are the processes and the arcs are the labeled transitions).

   1. P =def= a.b.P + a.c.P
   2. P =def= a.(b.P + c.P)
   3. P =def= Q | R        where  Q =def= a.Q  and  R = b.R
   4. P =def= Q | R        where  Q =def= a.Q  and  R =def= ^a.R
   5. P =def= (Q | R)\{a}  where  Q =def= a.Q  and  R =def= ^a.R
   6. P =def= (Q | R)\{a}  where  Q =def= a.Q + b.Q  and  R =def= ^a.R + c.R
   7. P =def= Q [a|->c]    where  Q =def= a.b.Q
   

   Give a finite representation of the transition graph whenever possible. For instance, if the process is P =def= a.Q and Q =def= b.P, then the graph should be:
   

2. (40 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).

3. (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.