Past exam of the computer science course of the University of Oxford / 2015 / Concurrency / 1 / c / Solution

Let $X=P{}_{\{a,b,d\}}{\Vert }_{\{a,b,c\}}Q$. In this CSP alphabetized parallel composition, $a,b$ require both participants, $d$ belongs only to the left participant and $c$ only to the right participant. Expand the reachable states using CSP prefixing and CSP external choice:For example, after the synchronized $b$, the left participant is back at $P$ but the right participant is at $c\to Q$. The left participant's proposed $a$ is blocked until the right participant has performed $c$. Similarly, after $a,d$, only the synchronized $b$ is possible. Thus there is no extra interleaving to include.

Eliminating $Y,W,Z$ gives the guarded equationConsequently choose the sequential CSP processThe unique fixed point principle first establishes $R=X$.

Now let $E=X{\Theta }_{\{c\}}X$. The CSP exception operator follows its left operand until that operand performs $c$, includes this $c$ in the visible behaviour, and then switches to its right operand. Applying its CSP step law to the four-state expansion yieldsThe switch occurs exactly where the ordinary execution already returns to $X$. Therefore $E=X=R$. The answer uses neither a CSP exception operator nor a CSP parallel composition operator, and the argument gives equality in all three standard CSP semantic models.