Exercise 1

1. P and Q are neither bisimilar nor weakly bisimilar, because the state Q' can make both a b-transition and a c-transition and therefore it is not bisimilar neither to P1 nor to P2.
2. P and Q are weakly bisimilar (but not strongly bisimilar).
3. P and Q are strongly bisimilar. The bisimulation relation is showed by the dashed lines.
4. P and Q are neither bisimilar nor weakly bisimilar, because the state Q' can make both a tau-transition to Q and a tau-transition to 0, and therefore it is not bisimilar neither to P nor to 0.
5. P and Q are weakly bisimilar (but not strongly bisimilar). The weak bisimulation relation is showed by the dashed lines.

Exercise 2

• 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'.

Exercise 3

   Sem(k) =def= p.Sem(k-1)
   Sem(i) =def= p.Sem(i-1) + v.Sem(i+1)   for 0<i<k
   Sem(0) =def= v.Sem(1)

An alternative definition is:

   Sem(k) =def= S | S | ... | S   (k instances of S in parallel)

where

   S =def= p.v.S

Exercise 4

   (^a.0 | a.P | a.Q)\{a}