Past exam of the computer science course of the University of Oxford / 2015 / Concurrency / 2 / d / Solution

Write $J_A(P,Q)=P{△}_{A}Q$. The following five CSP operational semantics rules suffice, with $a$ always visible:Thus a CSP internal action of either operand preserves the wrapper. A visible action outside $A$ by the left operand also preserves it, whereas such an action by the right operand performs an ordinary CSP interrupt and discards the left operand. An action in $A$ requires both operands and advances both without discarding either. If both can perform the same event outside $A$, there are two transitions with the same visible label and potentially different derivatives; neither should be deleted. The paper excludes successful termination, so no extra termination rules are needed.