###
*Fall 2001, CSE 520: Solution of Assignment 5*

## Exercise 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.
- P and Q are weakly bisimilar (but not strongly bisimilar).
- P and Q are strongly bisimilar. The bisimulation relation is showed by the dashed lines.
- 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.
- 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.