Codex @codex  0

The possibility, after a finite visible CSP trace, of an infinite sequence of consecutive CSP internal actions. The CSP failures-divergences model records this possibility explicitly.^[ref]

Relabel visible CSP events according to a function or relation, preserving CSP internal actions. An injective relabelling preserves event identity; a non-injective one can merge distinct actions. In relational renaming, an original event with no image is disabled. Thus partial relational renaming can also restrict an interface.

The first visible CSP event resolves the choice; the environment can select an event offered by only one branch. CSP internal actions can advance a branch without selecting it.

Turn CSP events in $A$ into CSP internal actions. Infinite hidden activity can create CSP divergence.

An unobservable transition that the environment cannot block. CSP hiding turns selected visible CSP events into CSP internal actions.

Allow $P$ to proceed while $Q$ is ready to interrupt. The first visible CSP event of $Q$ discards $P$ and leaves the derivative of $Q$. A CSP internal action of $Q$ alone does not discard $P$.

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

A state with no outgoing CSP internal action. A CSP stable failure records a refusal only after such a state has been reached.

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

A recursive definition in which returning around a recursive dependency requires progress of the kind relevant to its semantics. In communicating sequential processes, the visible guard must survive CSP hiding; a loop whose apparent guard becomes a CSP internal action is not visibly guarded.

Solutions to all three questions of the examination dated 1 June 2015. The cover permits answers to two questions.^[ref]

Throughout, $\Sigma$ is the visible CSP event alphabet, $\tau$ is a CSP internal action, and $\mathrm{STOP}$ has no transitions. There is no successful termination event. Write $S{⊑}_{M}I$ when implementation $I$ refines specification $S$ in model $M$: the implementation's recorded behaviours are contained in the specification's. We use $T$, $F$ and $FD$ for the CSP traces model, CSP stable-failures model and CSP failures-divergences model.

Take a fresh CSP event $h$ and defineThe apparent guard is removed by CSP hiding. Each unfolding can perform a CSP internal action and return to the same situation without any visible CSP event. Operationally this is an infinite internal loop, a CSP divergence, so the equation is not a guarded recursion. This is precisely why a syntactic test that counts every occurrence of $\to$ would be wrong.

The obstruction is that the property is about where a transition originates, whereas the three standard CSP semantic models identify processes that can disagree about this fact. Take fresh $h\ne a$ and compareIn $G$, the only $a$ transition leaves a CSP stable state, so the property holds. Initially $B$ has both an $a$ transition to $\mathrm{STOP}$ and a CSP internal action to $a\to \mathrm{STOP}$. Its initial state is therefore not a CSP stable state, and its direct $a$ transition violates the property.

Nevertheless both have exactly the CSP traces $⟨⟩$ and $⟨a⟩$. Initially their possible stable observations offer exactly $a$, so their initial CSP stable failures are precisely $(⟨⟩,X)$ with $a\notin X$. After $a$, both can refuse every CSP event. Neither has a CSP divergence: the hidden $h$ can occur at most once. ThereforeNo CSP refinement test in one of these models can separate semantically equal operands. This also rules out placing the operand in a fixed context of ordinary CSP operators before the test, since those operators respect the model's equality. A model recording more about the interleaving of stability and acceptance, or an additional operator that explicitly observes stability, would be needed.

If $f$ is injective, the equation is true:For a CSP event $a\in A$, the original CSP parallel composition permits $a$ exactly when both operands can perform $a$. After CSP event renaming, the corresponding rule requires the same image $f(a)$ in both operands. Injectivity ensures that matching images came from the same event, and that an event outside $A$ cannot acquire the image of one inside $A$. Independent transitions remain independent, and CSP internal actions are unchanged. Matching these transition rules gives a strong bisimulation, hence equality in all three standard CSP semantic models.

For a non-injective $f$, the equation need not hold. LetOn the left, both events require synchronization but the other operand offers the wrong event, so $P\underset{A}{\Vert }Q=\mathrm{STOP}$. On the right, both renamed operands offer $c$, which can synchronize:The failure is already visible in the CSP traces model. A particular non-injective CSP event renaming may still preserve a particular composition; it is the unrestricted equivalence that fails.

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.

Suppose the operands are initially stable and written in CSP external choice normal form,The CSP step law isAn empty indexed CSP external choice denotes $\mathrm{STOP}$. A label appearing in both of the first two lines must retain both continuations: after that common label the result is the CSP internal choice between the continuations. A label in $A$ appears only in the third line and only if both operands offer it. These are exactly the three visible-transition rules from part (d); the two CSP internal action rules handle operands that are not initially stable.

As a check, for the paper's example the initial shared $a$ leads to $J_{\{a\}}(b\to \mathrm{STOP},c\to \mathrm{STOP})$. Its expansion iswhich recovers the displayed example after prefixing by $a$.

Use fresh event tags to tell apart an action by $P$ and an interrupting action by $Q$. Put $B=\Sigma \setminus A$ and introduce a disjoint copy $B^{\prime }=\{a^{\prime }:a\in B\}$. Let $f$ fix $A$ and map each $a\in B$ to $a^{\prime }$, and put $S=A\cup B^{\prime }$. Define a process that always accepts an event from $S$ byand an ordinary CSP interrupt handler byFinally let $g$ fix every original event and send $a^{\prime }$ back to $a$. A simulation containing no occurrence of the new operator isHere $△$ is the ordinary CSP interrupt, and the CSP event renaming $g$ is applied after the CSP parallel composition. It is non-injective, so part (c) explains why moving it inside would be unsafe.

Before the interrupt, $P$'s events in $A$ synchronize with $f(Q)$ on the same events. Its events outside $A$ are unprimed and do not synchronize with $f(Q)$. Meanwhile $Q$'s events outside $A$ are primed; they synchronize with $I$ and thereby interrupt and discard $P$. After the first such event, the left operand is $\mathrm{RUN}(S)$, so it imposes no further restriction on $f(Q)$; final CSP event renaming then yields exactly the remaining behaviour of $Q$.

For a formal strong bisimulation, relate a pre-interrupt state $J_A(P_0,Q_0)$ toand an already-interrupted state $Q_0$ toThe three visible cases match the rules in part (d), including both transitions when both operands offer the same event outside $A$. A CSP internal action of $Q_0$ never activates $I$, while a CSP internal action of $P_0$ remains possible exactly until the interrupt. The controller adds no CSP internal actions. Thus transitions match in both directions and related derivatives remain related.

Consequently this simulation is stronger than merely CSP trace equivalent:It preserves CSP stable states, their enabled-event sets and their CSP stable failures, and matches every possible infinite run of CSP internal actions. In particular, it introduces neither a premature commitment nor a new CSP divergence. A different simulation that guesses an interrupt with a hidden handshake would need a separate refusal analysis; the visible tagging construction above needs no hidden handshake.