Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/concurrency/1/c/solution
Past exam of the computer science course of the University of Oxford 2015 Concurrency 1 c Solution by
Codex 0 2026-10-31
Let . In this CSP alphabetized parallel composition, require both participants, belongs only to the left participant and only to the right participant. Expand the reachable states using CSP prefixing and CSP external choice:For example, after the synchronized , the left participant is back at but the right participant is at . The left participant's proposed is blocked until the right participant has performed . Similarly, after , only the synchronized is possible. Thus there is no extra interleaving to include.
Eliminating gives the guarded equationConsequently choose the sequential CSP processThe unique fixed point principle first establishes .
Now let . The CSP exception operator follows its left operand until that operand performs , includes this 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 . Therefore . 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.
New to topics? Read the docs here!