### Fall 2000, CSE 520: Assignment 5

Distributed: Published on the web on Nov 21.
Due: Dec 5 (in class).
Total maximum score: 100 points.

The purpose of this assignment is to provide experience with CCS, and with the notion of bisimulation.

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.