as well as $\tau \notin H_2 \cup N_2 \cup B_2$. The other part of the non-interference, from Def. 11(1), does not provide any extra information.

We claim that $\ell \in H_2$. By contradiction, if $\ell \notin H_2$ then, since $\sigma \notin H_1$, the two c-actions $\ell:H_1[F_1]$ and $\sigma:H_2[0]$ of $Q$ would be interference-free according to Def. 11. But then, since $\{\ell, \sigma\} \cap C \neq \{\}$, coherence Def. 12 applied to $Q$ would imply $\sigma \in iA(F_1)$ and $\ell \in iA(0)$. The latter, however, is impossible. Thus, as claimed, $\ell \in H_2$. Likewise, from $\sigma \notin N_1$ we derive $\bar{\ell} \in N_2$ in the same fashion.

Now we invoke the fact that $\tau \notin B_2$, i.e. $H_2 \cap \overline{iA}(R) \subseteq \{\sigma\}$ and $N_2 \cap \overline{iA}(Q) \subseteq \{\sigma\}$. But $\bar{\ell} \in iA(R)$ and $\ell \in iA(Q)$, whence we must have $\ell \notin H_2$ and $\bar{\ell} \notin N_2$. This is a contradiction. Hence, transitions obtained by rules $(Com_a)$ and $(Com_\sigma)$ are never interference-free.

■ $\{(Par_1), (Par_2)\} \diamond (Com_\sigma)$: As the representative case, we assume $P = Q|R$ and the non-interfering, diverging reductions are

$$Q|R \xrightarrow{\frac{\alpha_1}{F_1|R}} H_1 Q_1 | R \text{ and } Q|R \xrightarrow{\frac{\sigma}{0}} H_2 \cup N_2 \cup B_2 Q_2 | R_2$$

with $\alpha_1 \in \mathcal{R} \cup \{\tau\}$ so that $P_1 \equiv Q_1|R$ and $P_2 \equiv Q_2|R_2$ are generated by the rule $(Par_1)$ and $(Com_\sigma)$, respectively, from transitions

$$Q \xrightarrow{\frac{\alpha_1}{F_1}} H_1 Q_1 \text{ and } Q \xrightarrow{\frac{\sigma}{0}} H_2 Q_2 \text{ and } R \xrightarrow{\frac{\sigma}{0}} N_2 R_2.$$

where $\alpha_1 \neq \sigma$ and the c-actions $\alpha_1:H_1[F_1|R]$ and $\sigma:(H_2 \cup N_2 \cup B_2)[0]$ are interference-free. First, Def. 11(1) implies $\alpha_1 \notin H_2 \cup N_2 \cup B_2$ and $\sigma \notin H_1$. Further, if $\alpha_1 = \tau$ then $(H_2 \cup N_2 \cup B_2) \cap (iA^*(0) \cup \{\tau\}) = \{\}$, which in particular means $H_2 \cap (iA^*(0) \cup \{\tau\}) = \{\}$. Therefore, the c-actions $\alpha_1:H_1[F_1]$ and $\sigma:H_2[0]$ are interference-free. Note that $\{\alpha_1, \sigma\} \cap C \neq \{\}$. Hence we can exploit coherence Def. 12 for $Q$, obtaining the stronger form of environment shift. But this would imply $\alpha_1 \in iA(0)$ which is impossible. So we find that transitions obtained by rules $(Par_i)$ and $(Com_\sigma)$ are never interference-free in the sense of coherence.

■ $(Com_\sigma) \diamond (Com_\sigma)$: We assume $P = Q|R$ and the non-interfering, diverging reductions

$$Q|R \xrightarrow{\frac{\sigma_1}{0}} H_1 \cup N_1 \cup B_1 Q_1 | R_1 \text{ and } Q|R \xrightarrow{\frac{\sigma_2}{0}} H_2 \cup N_2 \cup B_2 Q_2 | R_2$$

with $P_i = Q_i|R_i$ and $E_i = F_i|G_i$ are generated by the communication rules $(Com_\sigma)$. Observing that $\{\sigma_1, \sigma_2\} \subseteq \mathcal{R}$ is impossible, here, we may assume $\sigma_1 \neq \sigma_2$ or $Q_1|R_1 \neq Q_2|R_2$. This can only hold true if $Q_1 \neq Q_2$ or $R_1 \neq R_2$. Furthermore, the two clock transitions of $Q_1|Q_2$ can be assumed to be interference-free. From this it follows that the two underlying clock transitions $Q \xrightarrow{\sigma_1} H_1 Q_1$ and $Q \xrightarrow{\sigma_2} H_2 Q_2$ and the likewise the transitions $R \xrightarrow{\sigma_0} N_1 R_1$ and $R \xrightarrow{\sigma_0} N_2 R_2$ are interference-free. If $Q_1 \neq Q_2$ then we could apply coherence of $Q$ and obtain $\sigma \in iA(0)$, if $R_1 \neq R_2$ the same follows from coherence of $R$. This is impossible, whence the case can be excluded. ◀

## D.4 Hiding

► **Proposition 65.** If $Q$ is coherent for $\pi$ and $\sigma \dashrightarrow \ell \notin \pi$ for all $\sigma \in L$ and $\ell \in \pi$, then $Q/L$ is coherent for $\pi$.

**Proof.** It suffices to prove the proposition for the special case $Q/\sigma$ of a single clock. We recall the semantic rule for this case:

$$\frac{P \xrightarrow{\frac{\alpha}{E}} H Q \quad H' = H - \{\sigma\}}{P/\sigma \xrightarrow{\frac{\alpha/\sigma}{E/\sigma}} H' Q/\sigma} \quad (\text{Hide})$$
where $\sigma/\sigma = \tau$ and $\alpha/\sigma = \alpha$ if $\alpha \neq \sigma$. Let $P = Q/\sigma$ and the two non-interfering and diverging transitions

$$P \xrightarrow[\overline{E_1}]{\alpha_1/\sigma} H_1 P_1 \text{ and } P \xrightarrow[\overline{E_2}]{\alpha_2/\sigma} H_2 P_2$$

arise by (Hide) from transitions

$$Q \xrightarrow[\overline{F_1}]{\alpha_1} N_1 Q_1 \text{ and } Q \xrightarrow[\overline{F_2}]{\alpha_2} N_2 Q_2$$

with $E_i = F_i/\sigma$, $P_i = Q_i/\sigma$ and $H_i = N_i - \{\sigma\}$. For coherence Def. 12 we assume that $\alpha_1/\sigma \neq \alpha_2/\sigma$ or $P_1 \neq P_2$, or $\{\alpha_1/\sigma, \alpha_2/\sigma\} \subseteq \mathcal{R}$ and $\alpha_i/\sigma \notin H_{3-i}$. Further, let the c-actions $\alpha_i:H_i[E_i]$ be interference-free. Observe that the first case implies $\alpha_1 \neq \alpha_2$ and the second case means $Q_1 \neq Q_2$. Moreover, because of the assumption that $\sigma \dashv\vdash \alpha_i \notin \pi$ we must have $\sigma \notin N_1 \cup N_2$. But this means $H_i = N_i$.

First, suppose that $\alpha_1 = \alpha_2 = \sigma$. But then the assumption $Q_1 \neq Q_2$ contradicts strong determinacy of clocks (Proposition 15). Thus, the actions $\alpha_i$ cannot both be the clock $\sigma$ that is hidden. The case $\alpha_i = \sigma$ and $\alpha_{3-i} \in Act - \{\sigma\}$, for some fixed $i \in \{1, 2\}$ can also be excluded as follows: By Prop. 54 the clock transition and the non-clock transition must interfere in $Q$, i.e., $\alpha_i \in N_{3-i}$ or $\alpha_{3-i} \in N_i$. The former $\sigma = \alpha_i \in N_{3-i}$ is impossible because of the above. The latter is outright impossible since then $\alpha_{3-i}/\sigma = \alpha_{3-i} \in N_i = H_i$ which contradicts the non-interference assumption on the transitions of $P$.

The only remaining case to handle is that both of the diverging transitions are by labels $\alpha_1, \alpha_2 \in Act - \{\sigma\}$ and $\alpha_i/\sigma = \alpha_i$ for both $i \in \{1, 2\}$. We claim that the c-actions $\alpha_i:N_i[F_i]$ are interference-free. If $\alpha_1 \neq \alpha_2$ then non-interference assumption directly gives $\alpha_i \notin H_i = N_i$. Next, if for some $i \in \{1, 2\}$, $\alpha_i = \alpha_i/\sigma = \tau$, then the assumptions on $P$ not only give $\tau \notin H_{3-i} = N_{3-i}$ but also

$$N_{3-i} \cap \overline{\mathbb{A}}^*(F_{3-i}/\sigma) = H_{3-i} \cap \overline{\mathbb{A}}^*(E_{3-i}) = \{\}.$$

Since by assumption on policy conformance $\sigma \notin N_{3-i}$ the latter implies $N_{3-i} \cap \overline{\mathbb{A}}^*(F_{3-i}) = \{\}$. Now we have shown that the diverging transitions of $Q$ are non-interfering we can use the coherence Def. 12 for $Q$ by induction hypothesis and get $F'_1, F'_2, Q'$ such that

$$Q_1 \xrightarrow[\overline{F_2}]{\alpha_2} N'_2 Q' \text{ and } Q_2 \xrightarrow[\overline{F_1}]{\alpha_1} N'_1 Q' \text{ with } F_1 \xrightarrow{\alpha_2} F'_1 \text{ and } F_2 \xrightarrow{\alpha_1} F'_2$$

such that $N'_i \subseteq N_i$. By applying (Hide) to these transitions, we obtain

$$P_1 \xrightarrow[\overline{F'_2}/\sigma]{\alpha_2/\sigma} H''_2 Q'/\sigma \text{ and } P_2 \xrightarrow[\overline{F'_1}/\sigma]{\alpha_1/\sigma} H''_1 Q'/\sigma$$

where $H''_i = N'_i - \{\sigma\} \subseteq N_i - \{\sigma\} = H_i$. Note, by rule (Hide) we also have

$$F_1/\sigma \xrightarrow{\alpha_2/\sigma} F'_1/\sigma \text{ and } F_2/\sigma \xrightarrow{\alpha_1/\sigma} F'_2/\sigma.$$

In the special case that $\{\alpha_1/\sigma, \alpha_2/\sigma\} = \{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_1 \neq \alpha_2$ or $Q_1/\sigma \neq Q_2/\sigma$, or $\{\alpha_1/\sigma, \alpha_2/\sigma\} \cap \mathcal{C} = \{\alpha_1, \alpha_2\} \cap \mathcal{C} \neq \{\}$ we obtain the stronger context shifts $F_1 \xrightarrow{\alpha_2} F'_1$ and $F_2 \xrightarrow{\alpha_1} F'_2$ from which we infer

$$F_1/\sigma \xrightarrow{\alpha_2/\sigma} F'_1/\sigma \text{ and } F_2/\sigma \xrightarrow{\alpha_1/\sigma} F'_2/\sigma.$$

This completes the proof.
1697 D.5 Restriction

Let us next look at the restriction operator. The following definition is relevant for creating coherent processes under action restriction (App. D.5).

The fact that $P$ is locally coherent does not imply that $P \setminus L$ is locally coherent. Consider the process $Q = (s + a:s | b.\bar{s}) \setminus s$ which is conformant and pivotable. The signal $s$ blocks the action $a$ by priority in the thread $s + a:s$. For the communication partner $\bar{s}$ to become active, however, it needs the synchronisation with an external action $\bar{b}$. The transition

$$Q \xrightarrow[ (1 | b.\bar{s}) \setminus s ]{ a } (b.\bar{s}) \setminus s$$

generated by (Restr) does not provide enough information in the blocking set $H$ and environment $E$ for us to be able to characterise the environments in which the action $a$ is blocked. For instance, the parallel composition $Q | \bar{b}$ will internally set the sender $\bar{s}$ free and thus block the $a$-transition. From the above transition the (Com) rule permits $Q | \bar{b}$ to offer the $a$-step. This is not right as it is internally blocked and does not commute with the $b | \bar{b}$ reduction. A simple solution to avoid such problems and preserve confluence is to force restricted signals so they do not block any visible actions. This restriction suffices in many cases. Another, more general solution is to use the extended rule Restr\* discussed above after Example 34.

1709 ▶ **Proposition 66.** If $Q \models \pi$ and $\pi$ is precedence-closed for $L \cup \bar{L}$, then $(Q \setminus L) \models \pi \setminus L$.

**Proof.** It suffices to prove the proposition for the special case $P = Q \setminus a$ for a single channel name $a \in A$. Recall the rule (Restr) for this case:

$$ \frac{Q \xrightarrow[E]{\alpha} H \quad \alpha \notin \{a, \bar{a}\} \quad H' = H - \{a, \bar{a}\}}{Q \setminus a \xrightarrow[E\setminus a]{\alpha} H' \setminus a} \text{(Restr)} $$

Consider a transition

$$Q \setminus a \xrightarrow[E\setminus a]{\ell} H' \setminus Q' \setminus a \text{ derived from } Q \xrightarrow[E]{\ell} H \setminus Q'$$

with $H' = H - \{a, \bar{a}\}$, $\ell \notin \{a, \bar{a}\}$ and $\ell' \in H'$. Then $\ell' \notin \{a, \bar{a}\}$ and $\ell' \in H$. Conformance Def. 17 applied to $Q$ implies $\ell' \dashv\vdash \ell \in \pi$. But then $\ell' \dashv\vdash \ell \in \pi - a$, too, as both $\ell$ and $\ell'$ a distinct from $a$ and $\bar{a}$. This ensures conformance.

If $P = Q \setminus a$ and the two non-interfering and diverging transitions

$$P_2 \leftarrow_{E_2}^{\alpha_2} H_2 P \xrightarrow[E_1]{\alpha_1} H_1 P_1$$

arise from rule (Restr) then we have diverging transitions

$$Q_2 \leftarrow_{F_2}^{\alpha_2} N_2 Q \xrightarrow[F_1]{\alpha_1} N_1 Q_1$$

with $H_i = N_i - \{a, \bar{a}\}$, $\alpha_i \notin \{a, \bar{a}\}$, where $E_i \equiv F_i \setminus a$ and $P_i \equiv Q_i \setminus a$. We assume $\alpha_1 \neq \alpha_2$ or $P_1 \neq P_2$ or $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_i \notin H_{3-i}$. Further, suppose non-interference of $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$. Note that in case $P_1 \neq P_2$ we immediately have $Q_1 \neq Q_2$. Next, notice that the premise of the (Restr) rule ensures $\alpha_i \notin \{a, \bar{a}\}$. It is easy to see that this means $\{a, \bar{a}\} \cap N_i = \{\}$, i.e., $H_i = N_i$. By contraposition, suppose $\ell \in \{a, \bar{a}\}$ and $\ell \in N_i$. Then $\ell \dashv\vdash \alpha_i \in \pi$. But $\pi$ is precedence-closed for $\{a, \bar{a}\}$, so we would have $\alpha_i \in \{a, \bar{a}\}$ which is a contradiction. So, $H_i = N_i$.
All this means that to invoke coherence Def. 12 of the above $Q$ is sufficient to show that the c-actions $\alpha_1:N_1[F_1]$ and $\alpha_2:N_2[F_2]$ do not interfere. Now, if $\alpha_1 \neq \alpha_2$ then from the non-interference assumption on the transitions out of $P$ we get $\alpha_i \notin H_{3-i} = N_{3-i}$. This is what we need for Def. 11(1) to show that the c-actions $\alpha_i:N_i[F_i]$ are interference-free. For the second part Def. 11(2) suppose $\alpha_{3-i} = \tau$ for some $i \in \{1, 2\}$. Then the assumed non-interference of the transitions out of $P$ means $H_i \cap (i\overline{A}^*(E_i) \cup \{\tau\}) = \{\}$, which is the same as $\tau \notin H_i$ and the following set condition

$$ (N_i - \{a, \bar{a}\}) \cap i\overline{A}^*(F_i \setminus a) = \{\}. $$

Since $\{a, \bar{a}\} \cap N_{3-i} = \{\}$ we have $N_i \cap i\overline{A}^*(F_i) \subseteq \mathcal{L} - \{a, \bar{a}\}$. We claim that the $\alpha_i$-transitions of $Q$ is enabled, specifically $N_i \cap i\overline{A}^*(F_i) = \{\}$ observing that $\tau \notin H_i = N_i$. By contraposition, suppose $\beta \in N_i \cap i\overline{A}^*(F_i) \subseteq \mathcal{L} - \{a, \bar{a}\}$. Hence, $\beta \notin \{a, \bar{a}\}$ and so $\beta \in N_i - \{a, \bar{a}\}$ and also $\beta \in i\overline{A}^*(F_i \setminus a)$, but this contradicts the above set-condition. Thus, we have shown that for all $i \in \{1, 2\}$, $\alpha_{3-i} = \tau$ implies $N_i \cap i\overline{A}^*(F_i) = \{\}$. This proves the c-actions $\alpha_i:N_i[F_i]$ out of $Q$ are interference-free. Hence, we can use coherence of $Q$ for the diverging transition and get $F'_1, F'_2, Q'$ such that

$$ Q_1 \xrightarrow{\alpha_2} N'_2 Q' \text{ and } Q_2 \xrightarrow{\alpha_1} N'_1 Q' \text{ with } F_1 \xrightarrow{\alpha_2} F'_1 \text{ and } F_2 \xrightarrow{\alpha_1} F'_2 $$

such that $N'_i \subseteq N_i$. We construct the required reconvergence by application of rule (Restr):

$$ P_1 \xrightarrow{\alpha_2} H_2'' Q' \setminus a \text{ and } P_2 \xrightarrow{\alpha_1} H_1'' Q' \setminus a \text{ with } F_1 \setminus a \xrightarrow{\alpha_2} F_1' \setminus a \text{ and } F_2 \setminus a \xrightarrow{\alpha_1} F_2' \setminus a $$

<footnote n="1720">1720 with $E'_i = F'_i \setminus a$ and $H''_i = N'_i - \{a, \bar{a}\} \subseteq N_i - \{a, \bar{a}\} = H_i$. In the special case that</footnote>

<footnote n="1721">1721 $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_1 \neq \alpha_2$ or $P_1 \notin P_2$ or $\{\alpha_1, \alpha_2\} \cap \mathcal{C} \neq \{\}$ we can rely on the stronger</footnote>

<footnote n="1722">1722 context shifts $F_1 \xrightarrow{\alpha_2} F'_1$ and $F_2 \xrightarrow{\alpha_1} F'_2$ to conclude $F_1 \setminus a \xrightarrow{\alpha_2} F'_1 \setminus a$ and $F_2 \setminus a \xrightarrow{\alpha_1} F'_2 \setminus a$.</footnote>

<footnote n="1723">1723 This completes the proof. ◀</footnote>