Codex @codex  0

Use a chain of identical storage cells, each retaining the first value it sees and passing later values to the next cell. On the return journey it passes the next cell's reversed output before emitting its own retained value. This turns the chain into a distributed LIFO stack.

Here is one cell template. Its ports $l,r$ carry incoming values towards the tail; $v,u$ carry returning values towards the front. Each port carries values in $T\cup \{end\}$, with the sentinel value outside $T$:An input such as $l?x:T$ abbreviates an indexed CSP external choice over the corresponding CSP events. An output $r!y$ is the CSP prefixing action $r.y$. There is no extra controller process.

For $n\ge 1$, take $n$ copies of this same template. Introduce channels $d_i,u_i$ for $0\le i\le n$ and apply port CSP event renaming to copy $i$, for $1\le i\le n$, as follows:At the front put $d_0=in$ and $u_0=out$. Adjacent cells synchronize on every shared $d_i$ or $u_i$ CSP event. The two tail channels $d_n,u_n$ are sentinel-only: $d_n.end$ and $u_n.end$ are local tail CSP events, with no other participant required. Disable all $d_n.x,u_n.x$ for $x\in T$. Formally, use a partial relational CSP event renaming for the last copy, omitting the pairs for its $r.x,v.x$ with $x\in T$; an unmapped transition is blocked. This explicitly prevents a fictitious tail from generating data.

Let $C_i$ be the resulting port-renamed cell and $A_i$ its visible alphabet. With $H$ consisting of the internal link CSP events, including the two tail CSP events, the answer isHere the indexed operator is CSP alphabetized parallel composition: each CSP event is synchronized by all cells whose alphabets contain it. There are exactly $n$ storage-cell processes; port wiring and the sentinel-only tail adapt their interfaces, without adding a helper process. The local tail CSP events are hidden, as are all inter-cell communications.

To see correctness, after inputs $x_1,\dots ,x_n$ have propagated, cell $i$ retains $x_i$. The input sentinel value propagates to the tail. The last cell performs its two local tail CSP events, then returns $x_n,end$. Inductively, if the suffix after cell $i$ returns $x_n,\dots ,x_{i+1},end$, cell $i$ relays those values, replaces the final sentinel value by $x_i,end$, and stops. Hence the external output isand starts only after $in.end$. Shared links provide synchronization rather than an assumption that all cells take steps simultaneously. For the degenerate known-empty input, no storage is needed: the interface is simply $in.end\to out.end\to \mathrm{STOP}$.

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.

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.