Exercise 1

1. P and Q are neither strongly bisimilar, nor weakly bisimilar. In fact P -a-> 0 while the only a-transition from Q brings to 0 + Q which is not bisimilar to 0 (because 0 + Q can make an a-transition while 0 cannot make any transition).

2. P and Q are not strongly bisimilar because P can make a tau transition and Q cannot. However P and Q are weakly bisimilar. A weak bisimulation between them is R = { (P,Q) , (0,0) }

3. P and Q are strongly bisimilar and therefore also weakly bisimilar. A bisimulation between them is R = { (P,Q) , (P|P, a.Q), (P|P|P, Q), (P|P|P|P, a.Q) ,... }

4. P and Q are neither strongly bisimilar nor weakly bisimilar. In fact, Q -a-> tau.c.0 + tau.d.0, while the only a-transitions that P can make commit either to a process that offers only a c-transition or to a process that offers only a d-transtion (after a tau-transition).

5. In general P and Q are neither strongly bisimilar nor weakly bisimilar. In fact, is R is, say, b.0, then P is able to make a b-transition after an a-transition, while Q does not have this possibility. Only if Q is equivalent to 0 then the two processes are strongly (and weakly) bisimilar.

Exercise 2

Exercise 3

1. Let R be the bisimulation between P and Q. Then define R' = { (a.P,a.Q) } union R. We need to show that R' is a bisimulation. The only transition from a.P is a.P -a-> P. This transition can be simulated by by a.Q. In fact a.Q -a-> Q, and we have that (P,Q) in R, hence (P,Q) in R'. Analogously for the transition from Q.

2. Let R be the bisimulation between P and Q. Then define R'= { (P+R,Q+R) } union R union Id, where Id is the identity relation. We need to show that R' is a bisimulation. Consider a transition from P+R, say P+R -a-> P'. If the transition is due to P, then we have also P -a-> P'. Then we know that we also have Q -a-> Q' and hence Q+R -a-> Q' for some Q'. Furthermore (P',Q') in R and therefore (P',Q') in R'. If the transition is due to R, then we have also R -a-> P' and we can simulate the same transition from Q+R, i.e. we have Q+R -a-> P'. Furthermore (P',P') in Id and therefore (P',Q') in R'. Similarly for the transitions from Q+R.

3. Let R be the bisimulation between P and Q. Then define R'= { (P'|R',Q'|R') | R' in Proc, (P',Q') in R }. Clearly (P|R,Q|R) in R'. We need to show now that R' is a bisimulation. Consider a transition from P'|R'. This can be either:
   • a transition from P', say P' -a-> P''. Namely we have P'|R' -a-> P''|R'. In this case we know that we can simulate it with a transition from Q'. In fact Q' -a-> Q'' with (P'',Q'') in R. Hence Q'|R' -a-> Q''|R' and (P''|R',Q''|R') in R'.
   • a transition from R', say R' -a-> R''. Namely we have P'|R' -a-> P'|R''. In this case we have also Q'|R' -a-> Q'|R'' and (P'|R'',Q'|R'') in R'.
   • a tau transition due to a synchronization between P' and R'. In this case we have transitions of the form P' -a-> P'' , R' -^a-> R'', and P'|R' -tau-> P''|R''. We know that we can simulate the transition from P' with a transition from Q'. In fact Q' -a-> Q'' with (P'',Q'') in R. Hence Q'|R' -tau-> Q''|R'' and (P''|R'',Q''|R'') in R'.
   Similarly for the transitions from Q|R.

4. Let R be the bisimulation between P and Q. Then define R'= { (P'\L,Q'\L) | (P',Q') in R }. Clearly (P\L,Q\L) in R'. We need to show now that R' is a bisimulation. Consider a transition from P'\L, say P'\L -a-> P''\L. This means that a is not in L or ^L, and that P' -a-> P''. Hence we have also Q' -a-> Q'' with (P'',Q'') in R. Therefore Q'\L -a-> Q''\L with (P''\L,Q''\L) in R'. Similarly for transitions from Q'\L.

5. Let R be the bisimulation between P and Q. Then define R'= { (P'[f],Q'[f]) | (P',Q') in R }. Clearly (P[f],Q[f]) in R'. We need to show now that R' is a bisimulation. Consider a transition from P'[f], say P'[f] -a-> P''[f]. This means that that P' -b-> P'' with a = f(b). Hence we have also Q' -b-> Q'' with (P'',Q'') in R. Therefore Q'[f] -a-> Q''[f] with (P''[f],Q''[f]) in R'. Similarly for transitions from Q'[f].