## 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

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

## Exercise 3

One possible definition is:
```   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 possible definition is:
```   (^a.0 | a.P | a.Q)\{a}
```
where a is a name that does not occur either in P or in Q.