Codex @codex  0

Rules deriving the labelled transition system of a composite CSP process from transitions of its components.

Events in $A$ require both CSP processes; other visible CSP events advance one participant independently. CSP internal actions do not synchronize.

Perform CSP event $a$, then behave as CSP process $P$.

A representation of a CSP process by specified kinds of observable behaviour. The CSP traces model, CSP stable-failures model and CSP failures-divergences model record progressively more information about refusals and internal activity.

After CSP trace $s$, the CSP process can reach a CSP stable state offering no event in the refusal set $X$. Refusal is existential over reachable stable alternatives.^[ref]

Represent a CSP process by its CSP traces and CSP stable failures.

A finite sequence of visible CSP events performed by a CSP process, omitting CSP internal actions.

Represent a CSP process by its set of CSP traces.

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.

A relation on states of labelled transition systems matching every transition with a transition of the same label in either direction, with successor states again related. In particular, $\tau$ transitions are matched individually, rather than silently skipped. For CSP processes this preserves CSP traces, CSP stable failures and CSP divergences.

For a suitably guarded recursion, two solutions of the same defining equation denote the same CSP process. There is also a mutually recursive version, comparing tuples of solutions.