Coherence and Determinacy
with Priorities and Clocks

Luigi Liquori¹, Michael Mendler², and Claude Stolze¹

¹ Centre Inria de l'Université Côte d'Azur

² University of Bamberg

**Abstract.** Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called *constructive reduction* which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinacy-by-construction for multi-cast concurrent communication with shared memory. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of *coherent* processes a *confluence* property for constructive reductions. We show that under some restrictions, such as *pivotability*, coherence is preserved by the operators of prefix, summation, parallel composition, restriction and hiding. Since this permits memory and sharing, we are able to cover a strictly larger class of processes compared to those in Milner's classical confluence theory for CCS without priorities.

**Keywords:** Timed process algebras · Synchronous programming.

# 1 Introduction

Concurrency, by expression or by implementation, is both a convenient and unavoidable feature of modern software systems. However, this does not mean that we must necessarily give up the requirement of functional determinism which is crucial for maintaining predictability and to manage design complexity by simple mathematical models [31, 10, 18]. While the pure $\lambda$-calculus is naturally deterministic by design, it cannot model shared memory. Process algebras can naturally model shared objects, but do not guarantee determinism out of the box. In this paper we use the standard mathematical formalism CCS [36] to study methods for reconciling concurrency and determinism.

*Determinacy in Process Algebra.* Process algebras, like CCS [36], CSP [26], or $\Pi$-calculus [38, 39], just to mention a few, have been devised as a model of concurrency where a system and its environment continuously interact to mutually control each other’s behaviour through synchronisation and communication actions. In CCS, the interaction of concurrent processes $P|Q$ arises from the rendezvous synchronisation of an *action* $\alpha$ of P and an associated *co-action* $\bar{\alpha}$ from Q, generating a *silent action* $\tau$, also called a *reduction*. A process is in *normal form* if cannot reduce any more and *determinate* if it reduces to at most
one normal form, up to some notion of structural congruence. As a simplified example for the scenarios that we are interested in, consider a triple of concurrent processes $R|S|W$, where $S \stackrel{\text{def}}{=} r.S + w.\bar{r}.0$ acts as a shared resource, such as a (write-once) store, while $R \stackrel{\text{def}}{=} \bar{r}.0, W \stackrel{\text{def}}{=} \bar{w}.0$ are read and write processes, respectively, sharing $S$ with each other. The store $S$ offers a read action $r$ (rendezvous) leaving the state unchanged, or a write action $w$ upon which it changes its state to $\bar{r}.0$. At this point, the store only permits a single read and then becomes the inactive process $0$. The synchronisation between the actions $r, w$ and co-actions $\bar{r}, \bar{w}$ generates two sequences of reductions from $R|S|W$, namely $0|\bar{r}.0|0 \stackrel{\tau}{\leftrightarrow} 0|S|W \stackrel{\tau}{\leftrightarrow} R|S|W \stackrel{\tau}{\rightarrow} R|\bar{r}.0|0 \stackrel{\tau}{\rightarrow} 0|0|0$. Obviously, $R|S|W$ is not determinate. It reduces to two distinct normal forms $0|\bar{r}.0|0$ and $0|0|0$. The final store $\bar{r}.0$ on the left permits one more read, while $0$ on the right does not.

According to Milner [36], the notion of determinacy is tied up with predictability: "if we perform the same experiment twice on a determinate system, starting each time in its initial state, then we expect to get the same result, or behaviour, each time." A sufficient condition for determinacy is determinism. A process $P$ is (structurally) deterministic if for all its derivatives $Q$ and action $\alpha \in \text{Act}$, if $Q \xrightarrow{\alpha} Q_1$ and $Q \xrightarrow{\alpha} Q_2$ then $Q_1 \equiv Q_2$, where $\equiv$ is a suitable structural congruence. Structural determinism disallows processes such as $(a.A + a.B)|\bar{a}$ for $A \not\equiv B$ or parallel compositions such as or $a.A|a.B|\bar{a}$ where $A \not\equiv B$ which reduce to structurally distinct normal forms. However, determinism is too strong. For instance, the store $P \stackrel{\text{def}}{=} R_1|S|R_2$ with two readers $R_i \stackrel{\text{def}}{=} \bar{r}.R'_i$ ($i=1,2$), for a completely different $R'_i$, is determinate but not deterministic, when the $R_i$ may reach structurally distinct states after reading, say, $P \xrightarrow{\tau} R'_1|S|R_2$ and $P \xrightarrow{\tau} R_1|S|R'_2$ where $R'_1|S|R_2 \not\equiv R_1|S|R'_2$. Moreover, determinism is not closed under parallel composition. In the above example, all process $R_1, R_2, S$ are deterministic, but their composition $P$ is not. An insightful solution, proposed by Milner [36] (Chap. 11), is to replace determinism by the notion of *confluence* which still implies determinacy but turns out to be closed under parallel composition, and under natural restrictions. If predictability is taken as scheduling independence, then a sufficiently strong property for unique normal forms is the *Church-Rosser property* or *structural confluence*.

**Definition 1.** $P$ is (structurally) confluent<fnref n="3" /> if for every derivative $Q$ of $P$ and transitions $Q \xrightarrow{\alpha_1} Q_1$ and $Q \xrightarrow{\alpha_2} Q_2$ with $\alpha_1 \neq \alpha_2$ or $Q_1 \neq Q_2$, there exist $Q'_1 \equiv Q'_2$ such that $Q_1 \xrightarrow{\alpha_2} Q'_1$ and $Q_2 \xrightarrow{\alpha_1} Q'_2$.

It is intuitive to see that structural determinism implies structural confluence, which in turn implies determinacy, and that that all normal forms of a structurally confluent process must be structurally equivalent.

Milner shows that confluence is preserved by *"confluent composition"* $P|_L Q \stackrel{\text{def}}{=} (P|Q) \setminus L$, where $L$ is a set of "hidden" actions, combining the parallel and restriction operators, subject to the conditions that $\mathcal{L}(P) \cap \mathcal{L}(Q) = \{\}$ and

<footnote n="3">³ A variation of Milner’s “strong confluence” that includes $\tau$-actions and uses $\equiv$, and not bisimulation $\sim$.</footnote>
$\overline{\mathcal{L}(P)} \cap \mathcal{L}(Q) = L \cup \overline{L}$, where $\mathcal{L}(\underline{\phantom{}})$ is the function calculating the sort of a process. The former condition says that $P$ and $Q$ operate on disjoint actions and the latter says that every possible communication between $P$ and $Q$ is restricted by $L$. This is a form of sort separation, ensuring that every action $\alpha$ has at most one synchronisation partner $\bar{\alpha}$ either inside or outside of $(P|Q) \setminus L$.

Many practical examples of determinate systems can be understood as sort-separated compositions of confluent processes. However, this still covers only a rather limited class of applications. For example, memory processes such as $S$ above are firstly not confluent and, secondly, Milner's confluent composition forbids direct multi-cast communication, because labels such as $r$ in $S$ could not be shared by two readers $R_1, R_2$ due to sort-separation. This means that concurrent programming languages that support shared memory and yet have determinate reduction semantics, cannot be handled.

*Determinacy in Synchronous Programming.* The most prominent class of programming languages that manage to reconcile shared-memory concurrency and determinacy, is known as *Synchronous Programming (SP)*. In SP, processes interact with each other asynchronously at a *micro-step* level, yet synchronise in lock-step to advance jointly in iterative cycles of synchronous *macro-steps*. The micro-step interactions taking place during a macro-step determine the final outcome of the macro-step. This outcome is defined at the point where all subsystems pause to wait for a global logical *clock*. When this clock arrives, all subsystems proceed into the next computation cycle. Under the so-called *synchrony hypothesis*^4, the final outcome of a macro-step for each subsystem is fully determined from the stimulus provided by the environment of that component during the micro-step interactions. As such, the interactions inside each subsystem at macro-step level can be abstracted into a global Mealy automaton with deterministic I/O. SP started with Statecharts [24] and has generated languages such as Signal [20], Lustre [22], Esterel [7], Quartz [46], Zelus [11], SCCharts [23], Lingua Franca [32], just to mention a few.

When it comes to mathematical modelling it is natural to think of a clock as a broadcast action in the spirit of Hoare's CSP [26] that acts as a synchronisation barrier for a set of concurrent processes. Used with some scheduling control, it can bundle each process' actions into a sequence of macro-steps that are aligned with each other in a lock-step fashion. During each macro-step, a process executes only a temporal slice of its total behaviour, at the end of which it waits for all other processes in the same *clock scope* to reach the end of the current phase. When all processes have reached the barrier, they are released into the next round of computation. This suggests a priority-based scheduling mechanism, i.e., that the clock should fire only if the system has stabilised and no other admissible data actions are possible. This principle, called *maximal progress*, is built into timed process algebras, see e.g. [40, 15].

<footnote>^4 The “synchrony hypothesis” assumes that the reaction of a subsystem to input happens faster than the environment is able to produce new stimulus: the time needed to compute the reaction is unobservable by the environment. Also known as the “zero-time” assumption [28] or “fundamental mode operation” [47].</footnote>
*Contribution.* We introduce an extension of CCS, denoted CCS<sup>sp</sup>, that brings together the concepts of *priorities* [13, 45, 42] and *clocks* [21, 15, 41] that have previously been studied independently. We thus obtain an adequate compositional setting for SP exploiting standard techniques from process algebra. This is novel since many different customised semantics (e.g., [33, 12, 7, 1]) have been developed for SP over the years, few of which fit into the frameworks of classical process algebra. In the other direction, none of the extensions of CCS by priorities [13, 45, 42] or clocks [21, 15, 41] have systematically investigated determinacy for shared memory scenarios. By looking at this problem, our work identifies gaps in these classical theories and thus opens up new ground for research into general studies of Church-Rosser confluence in process algebra. We choose CCS here, but similar ideas might be possible for other process algebras like ATP [40], CSP or some synchronous variants of Milner's Π-calculus [2], just to mention a few. We find CCS most plausible as a point of departure since the concept of priorities is already well established and the combination of asynchronous scheduling and communication via local rendezvous synchronisation makes the problem of ensuring determinacy more prominent. At the technical level, we make the following specific contributions in this paper:

* We use broadcast actions (clocks) as global synchronisation barriers to schedule processes using priorities in a more flexible way than any of the earlier approaches. To achieve this, we must strengthen Phillips' notion of *weak enabling* (Def. 2) by *constructive enabling* (Def. 3). While all classical extensions of CCS by priorities [13, 45, 42] schedule the processes by their immediate initial actions, constructive enabling takes into account all actions potentially executable up to the next clock barrier. It was suprising for us to discover that such a natural modification suffices to obtain a process-algebraic model for shared-memory multi-threading, such as required for the constructive semantics of Esterel [7].

* We identify a strictly larger class of processes that enjoy the Church Rosser (CR) property (and thus reduce to unique normal forms) than the “confluence class” discussed by Milner [36] (Chap. 11). Since priorities are not part of Milner’s classical confluence theory, it cannot model deterministic shared objects with conflicting choice. In this paper, exploiting priorities and clocks, we enrich Milner’s notion of confluence to “confluence up-to priorities” that we call *coherence* (Def. 5). We show that coherent processes are CR for constructive enabling (Thm. 1).

* We show that coherence is preserved by parallel composition under reasonable restrictions that permit sharing and memory (Thm. 2). Specifically, we construct coherent processes in a type-directed compositional fashion using the notion of *precedence policies* (Def. 6). The policy for a conformant process specifies an upper bound for its precedence-blocking behaviour (Def. 7). A policy enriches the classical sort of a process by priority information. We define the special class of *pivot policies* and call coherent processes conforming to them *pivotable processes* (Def. 10). These are not only coherent (and thus CR) but preserved by parallel composition and other operators of the language (Thm. 2). In this fashion, we are able to extend Milner’s classical results for confluent processes
to cover significantly more applications, specifically Esterel-style multi-cast SP with shared objects.

• We show that each coherent process is *clock-deterministic* (Prop. 1) and that pivotable processes satisfy *maximal progress* (Prop. 2). No matter in which order we execute constructively enabled reductions, when a normal form is reached, and only then, a clock can tick. Since the normal form is uniquely determined, each pivotable process represents a “synchronous stream”. As such, our work extends the classical non-deterministic theory of timed (multi-clocked) process algebras [21, 40, 15] for applications in deterministic synchronous programming.

# 2 A Process Algebra with Clocks and Priorities

The syntax and operational semantics of our process algebra ‘SynPaTick’, denoted CCS<sup>spt</sup>, is defined in this section.

## 2.1 CCS<sup>spt</sup> Syntax

The terms in CCS<sup>spt</sup> form a set *P* of processes. We use *P*, *Q*, *R*, *S*... to range over *P*. Let *I* be a set of process names and let *A*, *B*... range over *I*. Let *A* be a countably infinite set of channel names with *a*, *b*... ranging over *A*. As in CCS, the set $\bar{A}$ is a disjoint set of co-names with elements denoted by $\bar{a}, \bar{b}, \bar{c}...$ in bijection with *A*; The overbar operator switches between *A* and $\bar{A}$, i.e., $\bar{a} = a$ for all $\bar{a} \in \bar{A}$. We will refer to the names $a \in A$ as input (or receiver) labels while the co-names $\bar{a} \in \bar{A}$ denote output (or sender) labels. Let *C* be a countably infinite set of broadcasted clock names, disjoint from both *A* and $\bar{A}$ and let $\sigma$ range over *C*. Every clock acts as its own co-name, $\bar{\sigma} = \sigma$ and so each $\sigma \in C$ is also considered as a clock label. Let $\mathcal{L} = A \cup \bar{A} \cup C$ be the set of input, output and clock labels and let $\ell$ range over $\mathcal{L}$, while *L*, *H* range over subsets of $\mathcal{L}$. We write $\overline{L}$ for the set $\{\ell | \ell \in L\}$. Let *Act* = *L* ∪ {τ} be the set of all actions obtained by adjoining the silent action $\tau \notin \mathcal{L}$ and let $\alpha$ range over *Act*. Viewed as actions, the input and output labels $\ell \in \mathcal{R}^{\text{def}} = A \cup \bar{A} \subseteq \text{Act}$ are referred to as rendezvous actions to distinguish them from the clock actions $\sigma \in C \subseteq \text{Act}$. All symbols can appear indexed. The process terms *P* are defined thus:

$$ P, Q, R, S ::= 0 \qquad \begin{array}{ll} \text{stop (inaction)} & \\ A & \text{name, } A \in \mathcal{I} \\ \alpha:H.P & \text{action, } \alpha \in \mathcal{L}, H \subseteq \mathcal{L} \\ P+Q & \text{choice} \end{array} \qquad \begin{array}{l|l} P|Q & \text{parallel} \\ P\setminus L & \text{restriction} \\ P/L & \text{hiding.} \end{array} $$

Intuitively, 0 denotes the *inactive* process which does nothing. The *action prefix* α:H.P denotes a process that offers to engage in the action α and then behaves as *P* while the *blocking* set *H* ⊆ *L* lists all actions taking precedence over α. A prefix with α ∈ *R* denotes a CCS-style rendezvous action. In case α ∈ *C*, it denotes a CSP-style broadcast action that can communicate with all the surrounding processes sharing on the same clock only when the clock is consumed. This correspond *de facto* to a broadcast synchronisation on a common clock σ. We
<figure><img src="image_1.png" /><figcaption>Fig. 1. Structural Congruence, where $\star \in \{|, +\}$ and $\lozenge \in \{\setminus, /\}$.</figcaption></figure>

assume that in every restriction $P \setminus L$ the set $L \subseteq \mathcal{R}$ consists of rendezvous actions, and in every hiding $P/L$ we have $L \subseteq \mathcal{C}$. These *scoping* operators act as name binders that introduce local scopes. The acute reader will notice the absence of the relabelling operator $P[f]$, useful in CCS to define the well-known “standard concurrent form” $(P_1[f_1] | \cdots | P_n[f_n]) \setminus L$. Because all of our examples are captured without need of relabelling, and for the sake of simplicity, relabelling will be treated in the full version of this work. A useful abbreviation is to drop the blocking sets if they are empty or drop the continuation process if it is inactive. For instance, we will typically write $a.P$ instead of $a:\{\}.P$ and $a:H$ rather than $a:H.0$. Also, it is useful to drop the braces for the blocking set if it is a singleton, writing $a:b.P$ instead of $a:\{b\}.P$. In our concrete notation using the abstract syntax of processes, we assume that the binary operator $+$ is right associative and taking higher binding strength than the binary operator $|$, i.e., writing $P+Q+R|S$ instead of $(P+(Q+R))|S$. Also, we assume that the unary operators of prefix, restriction and hiding have higher binding strength than the binary operators. Hence, we write $P\setminus c + a.b.c.Q|R/\sigma$ instead of $((P\setminus c) + (a.(b.(c.Q))))|(R/\sigma)$. The *sub-processes* of a $P$ are all sub-expressions of $P$ and (recursively) all sub-processes of $Q$ for *definitions* $A \stackrel{\text{def}}{=} Q$ where $A$ is a sub-expression of $P$. Sometimes it is useful to consider fragments of $\mathcal{P}$. As usual, we denote by $\mathcal{L}(P) \subseteq \mathcal{L}$ the free labels, called (*syntactic*) *sort* of $P$, identify processes that differ only in the choice of bound labels.

Following Milner’s presentation of the Π-calculus in [37], we define a structural congruence over processes. Specifically, structural congruence $\equiv$ is the smallest congruence over $\mathcal{P}$ that satisfies the equations in Fig. 1. The idea of the structural congruence is to split interaction rules between agents from rules governing the “left-to-right” representation of expressions. It allows to use those equations in the reduction rules making the latter simpler and easy to use, and it allows to set up formal equivalence of processes increasing for each program the number of legal transitions that, otherwise, would be blocked. Milner divides CCS equations in static, dynamic and expressions laws. We choose an approach inspired by the work of Berry and Boudol [9] by adding an explicit structural rule in the operational semantics. Note that we do not include in our structural rules all of Milner’s τ-laws, i.e. the ones related to the presence of τ-actions, like
$$ \overline{\alpha:H.P \xrightarrow[0]{\alpha} H P} \quad (\text{Act}) \qquad \frac{P \equiv P' \quad P' \xrightarrow{\alpha/R} H Q' \quad Q' \equiv Q \quad R' \equiv R}{P \xrightarrow{\alpha/R} H Q} \quad (\text{Struct}) $$

$$ \frac{P \xrightarrow{\alpha/R} H Q \quad L'=L \cup \bar{L} \quad \alpha \notin L' \quad H'=H-L'}{P \setminus L \xrightarrow{\alpha/R \setminus L} H' \setminus Q \setminus L} \quad (\text{Restr}) \qquad \frac{P \xrightarrow{\alpha/R} H Q \quad H'=H-L}{P/L \xrightarrow{\alpha/L/R/L} H' \setminus Q/L} \quad (\text{Hide}) $$

$$ \frac{P \xrightarrow{\alpha/R} H P' \quad \alpha \notin C}{P | Q \xrightarrow{\alpha/R} H P' | Q} \quad (\text{Par}) \qquad \frac{P \xrightarrow{\alpha/R} H P'}{P + Q \xrightarrow{\alpha/R} H P'} \quad (\text{Sum}) $$

$$ \frac{P \xrightarrow{\ell/R_1} H_1 P' \quad Q \xrightarrow{\bar{\ell}/R_2} H_2 Q' \quad H = \text{race}(P, Q)}{P | Q \xrightarrow{\ell | \bar{\ell}/R_1 | R_2} H_1 \cup H_2 \cup H P' | Q'} \quad (\text{Com}) \qquad \frac{A \stackrel{\text{def}}{=} P \quad P \xrightarrow{\alpha/R} H P'}{A \xrightarrow{\alpha/R} H P'} \quad (\text{Con}) $$

$$ \text{where} \quad \alpha/L \stackrel{\text{def}}{=} \begin{cases} \tau & \text{if } \alpha \in L \\ \alpha & \text{otherwise} \end{cases} \quad \ell | \bar{\ell} \stackrel{\text{def}}{=} \begin{cases} \tau & \text{if } \ell \in \mathcal{R} \\ \ell & \text{if } \ell \in \mathcal{C} \end{cases} \\ \text{race}(P, Q) \stackrel{\text{def}}{=} \begin{cases} \{\tau\} & \text{if } H_1 \cap \overline{i\mathcal{A}}(Q) \notin \{\ell\} \\ \{\ell\} & \text{or } H_2 \cap \overline{i\mathcal{A}}(P) \notin \{\bar{\ell}\} \\ \{\ell\} & \text{otherwise} \end{cases} $$

<caption>**Fig. 2.** The admissible transitions of CCS$^{spt}$. See Def. 2 for initial actions $i\mathcal{A}(P)$.</caption>

e.g. $\alpha.\tau.P \equiv \alpha.P$, or $P + \tau.P \equiv \tau.P$, and we have also dropped the congruence equations related to the uniqueness of solution of recursive equations and the expansion laws related to the standard concurrent form (cf. Chap. 3, Props. 2, 4(2) and 5 of [36]). Since we do not propose notions of behavioural equivalence in this paper, we prefer to take a conservative approach and only consider a minimum set of purely structural rules that do not impinge on the dynamics of expression behaviour.

## 2.2 Operational Semantics

The operational semantics for CCS$^{spt}$ is given using a labelled transition relation $P \xrightarrow{\alpha} Q$ in the style of Plotkin's Structured Operational Semantics (SOS) [44, 43], where $\alpha \in \mathcal{A}$ is the action that labels the SOS transition. When $\alpha \in \mathcal{L}$, the transition corresponds to a communication step, namely a rendezvous action or a broadcasted clock action. When $\alpha = \tau$ is silent, then the transition corresponds to a reduction or an evaluation step. When there is no more reduction possible, i.e., there is no $P'$ with $P \xrightarrow{\tau} P'$, then $P$ is a normal form.

We decorate the nondeterministic SOS with annotations that provides sufficient information to express a uniform and confluent reduction strategy based on scheduling precedences. Including these annotations, our SOS judgment takes the form $P \xrightarrow{\alpha/R} H Q$, read as “P reduces to Q with an action $\alpha$, a blocking set $H$ and a surrounding concurrent environment $R$”. The action decorated with these annotations, noted $\alpha:H[R]$, is called the complete action (or c-action). The semantics is defined inductively as the smallest relation closed under the rules in Fig. 2. We call each transition derivable by Fig. 2 an admissible transition. The
information provided by a c-action is sufficient to define our constructive reduction strategy for CCS<sup>sp</sup>t that satisfies a refined confluence property. Sometimes, we write $P \xrightarrow{\alpha} Q$ to state that there is a transition for some R and H.

The intuition behind the annotations of admissible transitions is as follows: $\alpha$ is the usual action labeling SOS transitions. The blocking set $H$ is the set of actions that take precedence over $\alpha$, and $R$, called the concurrent context, is a process that represents the behaviour of all threads in $P$ that execute concurrently with the transition, i.e., all actions in $R$ are potentially in competition with $\alpha$. Think of $H$ as the resources that are required by the action and of $R$ as the concurrent context that potentially competes for $H$. In a parallel composition $P|Q$ of $P$ with another process $Q$, the context $R$ might interact with the environment $Q$ to generate actions in the blocking set $H$. If this happens, the reduction in $P$ with blocking set $H$ will be considered blocked in our scheduled semantics.

In the rules of Fig. 2, the reader can observe how the annotation for the concurrent context and the blocking sets are inductively built. In a nutshell: Rule (Act) is the axiom annotating in the transition the action and the (empty) environment. Rules (Restr) and (Hide) deal with “local restriction” of rendezvous actions and “local hiding” of broadcasted clocks. Rules (Par) and (Sum) are almost standard and deal with parallelism and choice. Rule (Struct) internalises in the transition the above presented structural equivalence of processes. Rule (Com) constitutes the core of our SOS. It captures, in an elegant way, both the classical CCS rendezvous communication rule and the classical CSP broadcasting communication; it has an extra race test, enriching the blocking set of the conclusion by $\tau$, in case $P$ and $Q$ interfere. Finally, rule (Con) deals with process names and refers to a process whose behaviour is specified by a definitional equation $A \stackrel{def}{=} P$.

## 2.3 Constructive Scheduling

The operational semantics of Fig. 2 for rendezvous actions coincides with that of CCS and the rules for clock actions coincide with the semantics of CSP broadcast actions. The scheduling annotations $H$ and $R$ of a c-action $\alpha:H[R]$ expose extra information about blocking and concurrent context, respectively, of the underlying action $\alpha$. We can use them to implement different scheduling strategies. Prioritised process algebras [13, 45, 42] block an admissible transition $\alpha:H[R]$ when $H$ contains the silent action $\tau$ or an action that synchronises with some initial action of the concurrent context $R$. Otherwise, it is (weakly) enabled.

**Definition 2 (Initial actions and weakly-enabled transition).**

- The initial actions of a process $R$ are $iA(R) = \{\alpha \mid \exists Q. R \xrightarrow{\alpha} Q\} \subseteq Act$.

- A c-action $\alpha:H[R]$ is called weakly enabled if $H \cap (iA(R) \cup \{\tau\}) = \{\}$.

We call $P$ discrete if all its c-actions $\alpha:H[R]$ are self-blocking, i.e. $H = \{\alpha\}$. Let us call a process $P$ free if all its c-actions $\alpha:H[R]$ have an empty blocking set
$H = \{\}$. The weakly enabled transitions of (unclocked) free processes coincide with the semantics of CCS [36]. A process $P$ is *irreflexive* if none of its c-actions $\alpha:H.Q$ blocks itself, i.e., $\alpha \notin H$. For (unclocked) irreflexive processes, a transition is weakly enabled iff it is derivable in the operational semantics of CCS$^{Ph}$ [42]$^5$.

Ex. 1 and Ex. 2 in Sec. 3 below demonstrate how prioritised scheduling by weak enabling (Def. 2) can indeed help to ensure determinacy in special cases. For the general case, however, weak enabling is not sufficient. In order to prevent non-determinacy (a global property) from priorities (a purely local property), we must be able to block a c-action $\alpha:H[R]$ not just if the initial actions $iA(R)$ of the concurrent context $R$ can synchronise with $H$, as in weak enabling, but look at the set $iA^*(R)$ of all actions that $R$ can potentially engage in, before it reaches a clock; Ex. 4 in Sec. 3 illustrates this.

**Definition 3 (Potential actions and constructive enabling).**

- The set $iA^*(P) \subseteq \mathcal{L}$ of potential actions is the smallest extension $iA(P) \cap \mathcal{L} \subseteq iA^*(P)$ such that if $\ell \in iA^*(Q)$ and $P \xrightarrow{\alpha} Q$ for $\alpha \in \mathcal{R} \cup \{\tau\}$, then $\ell \in iA^*(P)$.

- A transition with c-action $\alpha:H[R]$ is called constructively enabled, or c-enabled for short, if $H \cap (iA^*(R) \cup \{\tau\}) = \{\}$.

- We write $P \Downarrow Q$ if there is a sequence of c-enabled reductions $P \xrightarrow{\tau} P_1 \xrightarrow{\tau} \dots P_n \xrightarrow{\tau} Q$ such that $Q$ is a normal form.

The next Sec. 3 presents some motivating examples, while Sec. 4 focuses on the mathematical theory underlying CCS$^{spt}$.

**3 Examples**

The first example shows the basic mechanism of how priorities can be used to schedule processes under weak enabling.

*Example 1 (Read Before Write).* Consider a “store” $S \stackrel{def}{=} w.r+r:w$ that offers a write action $w$ followed by a read $r$, or a read action $r:w$ that prefers the write over the read. If we put $S$ in parallel with a reader $R \stackrel{def}{=} \bar{r}$, the read actions $r$ and $\bar{r}$ synchronise in a reduction $S|R \xrightarrow{\tau_0} \{w\} \bar{0}$. The fact that $w$ takes priority over $r$ is recorded in the blocking set $\{w\}$. This will block $R$'s transition when a parallel writer $W \stackrel{def}{=} \bar{w}$ is added. Then the reading reduction would be $S|R|W \xrightarrow{\tau_W} \{w\} W$, but the c-action $\tau:\{w\}[W]$ is not weakly enabled (see Def. 2).

Processes can block each other from making progress. This happens under weak enabling if processes offer two-way rendezvous synchronisation with contradicting precedences, as the following examples illustrate.

<footnote>$^5$ In CCS$^{Ph}$ the blocking sets are written before the action, $H:\alpha.P$, where we write $\alpha:H.P$ in CCS$^{spt}$.</footnote>
**Example 2 (Binary Blocking).** Take processes $P \stackrel{\text{def}}{=} a:b.A+b$ and $Q \stackrel{\text{def}}{=} \bar{b}:\bar{a}.B+\bar{a}$. Their composition $P|Q$ has two admissible reductions, through $a:b|\bar{a}$ to A or through $b|\bar{b}:\bar{a}$ to B. So, disregarding the precedences, it is non-deterministic if $A \not\equiv B$. Under weak enabling transitions, however, $P|Q$ creates a circular deadlock: P offers a unless synchronisation with $\bar{b}$ is possible, while Q offers $\bar{b}$ provided there is no synchronisation with a. None of the reductions is enabled.

**Example 3 (Reflexive Blocking).** In the free process $s|\bar{s}.A|\bar{s}.B$ action s can be consumed by $\bar{s}.A$ or by $\bar{s}.B$, generating non-deterministic $\tau$-transitions to $A|\bar{s}.B$ or to $\bar{s}.A|B$. However, by adding self-blocking, as in $s:s|\bar{s}.A|\bar{s}.B$, weak enabling protects the prefix s from being consumed when both $\bar{s}.A$ and by $\bar{s}.B$ compete for it. If only one is present, as in $s:s|\bar{s}.A$ and $s:s|\bar{s}.B$, no blocking occurs.

Blocking under weak enabling, as implemented in the classical prioritised algebras [13, 45, 42] ensures determinism in the special case where the dependencies involve only initial actions. However, parallel threads can create dependency chains through sequences of actions, e.g., when accessing a shared process that is acting as a resource. This is the general case handled by our c-enabling.

**Example 4 (Transitive Blocking).** The process $S \stackrel{\text{def}}{=} w_0+r_0:w_0|w_1+r_1:w_1$ offers receiver actions $w_i$ and $r_i$ for $i \in \{0, 1\}$ such that $w_i$ has precedence over $r_i$. Now take processes $P_0 \stackrel{\text{def}}{=} \overline{r_0.w_1}$ and $P_1 \stackrel{\text{def}}{=} \overline{r_1.w_0}$ which first aim to synchronise with $r_i$ and then sequentially afterwards with $w_{1-i}$. The parallel composition $P_0|S|P_1$ has two initial $\tau$-reductions

$$P_0|w_0+r_0:w_0|\overline{w_0} \leftarrow_{P_0|(w_0+r_0:w_0)}^{\tau} \{w_1\} P_0|S|P_1 \xrightarrow{w_1+r_1:w_1|P_1} \{w_0\} \overline{w_1}|w_1+r_1:w_1|P_1$$

These reductions are both weakly enabled but not c-enabled. This is good for determinacy, because if we continued under weak enabling then the residual process $\overline{w_1}|w_1+r_1:w_1|P_1$ in its first reduction must execute the synchronisation on $w_1$ and thus proceed as $\overline{w_1}|w_1+r_1:w_1|P_1 \xrightarrow{\tau} P_1$ while the residual process $P_0|w_0+r_0:w_0|\overline{w_0}$ can only reduce to $P_0$. Hence, the resulting final outcome of executing $P_0|S|P_1$ is not determinate. Observe that none of the two reductions displayed above is actually c-enabled.

**Example 5 (Read/Write Memory).** Let $w_0, w_1, r_0, r_1$ the labels of writing/reading a boolean value 0 or 1, respectively. A memory would be modelled by two mutually recursive processes

$$w\text{AND}_0 \stackrel{\text{def}}{=} w_1.w\text{AND}_1 + w_0:w_1.w\text{AND}_0 + r_0:\{w_0, w_1\}.w\text{AND}_0$$

$$w\text{AND}_1 \stackrel{\text{def}}{=} w_1.w\text{AND}_1 + w_0:w_1.w\text{AND}_0 + r_1:\{w_0, w_1\}.w\text{AND}_1$$

The process $w\text{AND}_v$ represents the memory cell in a state where it has stored the value $v \in \{0, 1\}$. In either state, it offers to synchronise with a write action $w_u$ to change its state to $w\text{AND}_u$, and also with a read action $r_v$ to transmit its stored value $v$ to a reader.
$$ \mathbf{ABRO} \stackrel{\text{def}}{=} (A | B | R | O) \setminus s $$

$$ A \stackrel{\text{def}}{=} k:k.0 + a:\{k, a\}.\bar{s}:\bar{s}.0 + \sigma:\{k, a\}.A $$

$$ B \stackrel{\text{def}}{=} k:k.0 + b:\{k, b\}.\bar{s}:\bar{s}.0 + \sigma:\{k, b\}.B $$

$$ R \stackrel{\text{def}}{=} r:r.R' + \sigma:r.R $$

$$ R' \stackrel{\text{def}}{=} \bar{k}.R' + \sigma:\bar{k}.(A | B | R | O) $$

$$ O \stackrel{\text{def}}{=} k:k.0 + s:k.O' + \sigma:\{k, s\}.O $$

$$ O' \stackrel{\text{def}}{=} k:k.0 + s:k.\bar{o}:\bar{o}.0 + \sigma:\{k, s\}.O' $$

<figure><img src="image_2.png" /><figcaption>Fig. 3. ABRO as a CCS<sup>spt</sup> process, a Mealy machine, and a SyncChart.</figcaption></figure>

The write actions $w_u$ do not only change the state of the memory, they also block the read actions since they appear in their blocking sets $r_v:\{w_0, w_1\}$. Between the write actions, the blocking sets implement a precedence of $w_1$ over $w_0$. In the picture on the right, the process state transitions are visualised with the blocking sets as red dashed arrows.

<figure><img src="image_3.png" /></figure>

**Example 6 (Esterel Signals).** Concurrent Esterel threads communicate via signals [8, 19]. A (pure, temporary) signal can have two statuses, present and absent. At the beginning of a synchronous macro-step, each signal is initialised to be absent, by default. The signal becomes present as soon as some thread emits it. It remains present thereafter for throughout the current macro-step, i.e., until the next clock cycle is started. The clock is a global synchronisation, taken by all threads simultaneously. The value of the signal is broadcast to all concurrent threads which can test it and branch their control-flow according to the signal's status. To maintain coherency of data-flow and deterministic behaviour, the signal status can only be read when no writing is possible any more. Esterel compilers conduct a causality analysis on the program and obtain a suitable static schedule when they generate imperative code. In Esterel hardware compilers, the scheduling is achieved dynamically by propagating signal statuses. Programs that cannot be scheduled to satisfy the emit-before-test protocol, or hardware that does not stabilise are called non-constructive and rejected by the compiler. A pure, temporary signal is modelled by the following behaviour:

$$ S_0 \stackrel{\text{def}}{=} \text{abs:emit}.S_0 + \text{emit}.S_1 + \sigma:\{\text{abs, emit}\}.S_0 $$

$$ S_1 \stackrel{\text{def}}{=} \text{pres}.S_1 + \text{emit}.S_1 + \sigma:\{\text{pres, emit}\}.S_0 $$

which is depicted on the right.

<figure><img src="image_4.png" /></figure>
Example 7 (ABRO). The ‘hello world’ in the Esterel synchronous language [8], ABRO has the following behaviour: “Emit the output *o* as soon as both inputs *a* and *b* have been received. Reset this behaviour each time the input *r* occurs, without emitting *o* in the reset cycle” [19]. The behaviour of ABRO is expressed as a Mealy machine and a SyncChart, as displayed in Fig. 3 on the right. The synchronous behaviour of Esterel lies in the assumption that each transition of the Mealy machine summarises a single *macro-step* interaction of the machine with its environment. The transitions of parallel machines synchronise so that state changes proceed in lock-step. The simultaneous execution of these transitions that make up a macro-step consists of the sending and receiving of signals. The propagation of individual signals between machines is modeled in the *micro-step* operational semantics of Esterel. In CCS<sup>spt</sup> we represent the micro-steps as sequences of τ-transitions, i.e., reductions, whereas the macro-step is captured as a global clock synchronisation. Unfortunately, the Mealy machine formalism is *not scalable* because the number of states can grow exponentially as the number of signals grow, while in Esterel can be expressed in a linear number of code lines as seen on the right. The loop *P* each *R* construct of Esterel executes the behaviour of program *P* for an unbounded number of clock cycles, but restarts its body *P* when the signal *R* becomes present.

The reset *R* takes priority over the behaviour of *P* which is preempted at the moment that the reset occurs. Note that in Esterel each signal appears *exactly once*, as in the specification and unlike in the Mealy machine. Other parts of Esterel also naturally arise from precedence-based scheduling. Esterel's loop *P* each *R* mechanism, for instance, can be coded using the static parallel composition operator that combines the process *P* to be aborted and reset with a “watchdog” process *R*. The latter waits for the reset signal from the environment in each clock cycle. The choice between the reset and continuing inside *P* is resolved by giving *R* higher priority. When the reset occurs, the watchdog sends “kill” signals to all threads running in *P* and waits for these to terminate. Only then the watchdog *R* restarts *P* from scratch. This is a form of precedence that can be naturally expressed in the blocking sets of CCS<sup>spt</sup>. As such, Fig. 3 on the left translates the Esterel code of ABRO compositionally in CCS<sup>spt</sup>.

For the sake of simplicity, we don't use the channel encoding of Ex. 6, and we assume that the channels *a*, *b*, *r*, *o* model the signals *A*, *B*, *R*, *O*, and all have a unique sender and receiver. The main process ABRO creates a local channel *s* and executes *A|B|R|O*. Hence, *A|B* encodes `await A || await B`. The channel *s* is used to signal the normal ending of processes *A* and *B* to *O*: in other words, it ensures `await A || await B` is executed *before* `emit O`. Once *s* has been received twice by *O* (which encodes `emit O`), it emits `¯o` and ends, unless it is killed at some moment by the action *k*. Finally, *R* controls the Esterel loop: it kills all the remaining processes among *A|B|O* when it receives *r* using the action ¯*k* which has priority over everything else, and once it cannot send ¯*k* anymore, it waits for *σ* and restart *A|B|R|O*. Every action that is supposed to synchronise
with a unique process is reflexive (i.e. it belongs to its own blocking set). It is the case for every action except $\bar{k}$, $s$, and $\sigma$. Having as many reflexive actions as possible helps ensuring the coherence of the process, as shown in Thm. 2.

**Example 8 (Processes with different clocks).** Consider the process $P \stackrel{\text{def}}{=} (\rho:\{m,\sigma\}.P + m:m.\rho.P + \sigma:m.P)/\rho$. The process' internal clock $\rho$ has a lower priority than $\sigma$ so it does not block any outside action $\sigma$. The action $m$ still blocks $\sigma$ to ensure maximal progress. For instance, in $P|Q$ where $Q \stackrel{\text{def}}{=} \sigma.m:\bar{m}.\sigma.\bar{m}:\bar{m}.0$, process $Q$ can send all the messages $\bar{m}$ on the tempo of $\sigma$, while $P$ receives them on the unrelated tempo of $\rho$.

**Example 9 (Changing the frequency of a clock).** Consider the following processes:

$$ 
\begin{align*}
P &\stackrel{\text{def}}{=} P_1 / \rho \\
P_1 &\stackrel{\text{def}}{=} \rho:x.(\sigma:x.P_1 + x:x.\sigma P_2) + x:x.\sigma P_2 \\
P_2 &\stackrel{\text{def}}{=} \rho:x.(\rho:x.(\sigma:x.P_2 + x:x.\sigma P_1) + x:x.\sigma P_1) + x:x.\sigma P_1
\end{align*}
$$

If we consider that the action $\bar{x}$ is never offered, then $P_1/\rho$ triggers the internal clock $\rho$ once between each clock $\sigma$, whereas $P_2/\rho$ triggers $\rho$ twice between each $\sigma$. The action $x$ allows the process $P$ to switch between $P_1/\rho$ and $P_2/\rho$.

# 4 Coherence and Determinacy for CCS<sup>spt</sup>

This section presents the core elements of our scheduling theory under constructive enabling: coherence, policies, and policy-conformant processes. Coherence (Def. 5) corresponds to Milner's notion of confluence, but refined “up-to” priorities. It requires structural confluence for c-enabled and diverging c-actions only if they do not interfere with each other considering their blocking sets and concurrent environments.

**Definition 4 (Transition Interference).** Two c-enabled transitions with c-actions $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are interference-free if $\alpha_1 = \alpha_2$ or $\alpha_i \notin H_{3-i}$ for all $i \in \{1,2\}$.

Confluence of interference-free c-actions is formulated using an auxiliary form of residual transition $P \stackrel{\alpha}{\rightsquigarrow} Q$. This is a transition from $P$ to $Q$ with an action that is a “factor” of $\alpha$. Formally, we define $P \stackrel{\alpha}{\rightsquigarrow} Q$ if $(i) \alpha \in \mathcal{L}$ with $P \stackrel{\alpha}{\to} Q$ or $P \equiv Q$, or $(ii) \alpha = \tau$ with $P \stackrel{\tau}{\to} Q$ or $P \stackrel{\ell}{\to} Q$ or $P \stackrel{\bar{\ell}}{\to} Q$ for some $\ell \in \mathcal{R}$.

**Definition 5 (Process Coherence).** A process $P$ is (structurally) coherent if for all its derivatives $Q$ the following holds: given two c-enabled and interference-free transitions $Q \xrightarrow{\alpha_1} H_1$ and $Q \xrightarrow{\alpha_2} H_2$ such that $\alpha_1 \neq \alpha_2$ or $Q_1 \notin Q_2$ or both $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_i \notin H_{3-i}$; there exist transitions $Q_1 \xrightarrow{\alpha_2} H'_2$ and $Q_2 \xrightarrow{\alpha_1} H'_1$ with $H'_i \subseteq H_i$ and $E_1 \rightsquigarrow E'_1$ and $E_2 \rightsquigarrow E'_2$. Moreover, if $\alpha_1 = \alpha_2 \in \mathcal{C}$ are clocks, then $E_1 \stackrel{\alpha_2}{\to} E'_1$ and $E_2 \stackrel{\alpha_1}{\to} E'_2$.
Def. 5 expresses a Church-Rosser Property that extends the notion of confluence (Def. 1) for general, non-discrete processes. One shows that for discrete processes, coherence is identical with confluence.

**Example 10.** For instance, $Q \stackrel{\text{def}}{=} a:\{\}$.0 is confluent but not coherent. Since the prefix is not self-blocking, coherence ensures that the label must be *consumable* by arbitrarily many concurrent processes. Technically, since $Q \xrightarrow{a} Q_1$ and $Q \xrightarrow{a} Q_2$ for $Q_1 \equiv 0 \equiv Q_2$, there should be a transition $Q_i \xrightarrow{a} Q'$ which is not the case. However, for discrete processes, coherence is identical with confluence: With self-blocking, $Q \stackrel{\text{def}}{=} a:a.0$ is both confluent and coherent. It is important to note that all examples in Sec. 3 are coherent but not confluent.

**Theorem 1 (Coherence implies Determinacy).** *Coherent processes are de-terminate under c-enabled reductions, i.e., $P \Downarrow Q_1$ and $P \Downarrow Q_2$ implies $Q_1 \equiv Q_2$.*

Thm. 1 concerns the reductions, i.e., the $\tau$-transitions, of a coherent process. For clock transitions we have an even stronger result.

**Proposition 1 (Clock Determinism).** *Coherent processes $P$ are structurally clock deterministic, i.e., if $P \xrightarrow{\sigma} P_1$ and $P \xrightarrow{\sigma} P_2$ are c-enabled, then $P_1 \equiv P_2$.*

The question is now how we can obtain coherent processes by composition. In view of Milner’s classical result for confluence, we expect to have to impose some form of “sort-separation” for parallel processes. It turns out that we can express such a condition and even avoid the restriction operator (thereby permit sharing) if we enrich the sorts $\mathcal{L}(P)$, $\mathcal{L}(Q)$ by priority information. We call the resulting enriched sorts $\pi(P)$, $\pi(Q)$ *precedence policies*.

**Definition 6 (Precedence Policy).** *A precedence policy is a pair $\pi = (L, \dashrightarrow)$ where $L \subseteq \mathcal{L}$ is a subset of visible actions, called the alphabet of $\pi$ and $\dashrightarrow \subseteq L \times L$ a binary relation on $L$, called the precedence relation.*

We will write $\ell \in \pi$ to state that $\ell$ is in the alphabet of $\pi$ and we write $\ell_1 \dashrightarrow \ell_2 \in \pi$ to express that the pair $(\ell_1, \ell_2) \in \dashrightarrow$, i.e. $\ell_1$ has precedence over $\ell_2$. Further, if $\ell_1, \ell_2 \in \pi$ and both $\ell_1 \dashrightarrow \ell_2 \notin \pi$ as well as $\ell_2 \dashrightarrow \ell_1 \notin \pi$, we say that $\ell_1$ and $\ell_2$ are *concurrently independent* under $\pi$, written (by abuse of the set-notation) $\ell_1 \diamond \ell_2 \in \pi$. For any policy $\pi = (L, \dashrightarrow)$ and set of labels $K \subseteq \mathcal{L}$ we denote by $\pi \setminus K$ the policy $\pi$ restricted to the alphabet $L - (K \cup \bar{K})$ in the standard way. There is also the normal inclusion ordering $\pi_1 \subseteq \pi_2$ between policies defined by $L_1 \subseteq L_2$ and $\dashrightarrow_1 \subseteq \dashrightarrow_2$. The next Def. 7 on conformance captures how policies statically specify the externally observable scheduling behaviour of a process.

**Definition 7 (Conformance).** *P conforms to a policy $\pi$ if for each derivative $Q$ of $P$: If $Q \xrightarrow{\ell} H$ $Q'$ with $\ell \in \mathcal{L}$, then $\ell \in \pi$ and for all $\ell' \in H \cap \mathcal{L}$, we have $\ell' \dashrightarrow \ell \in \pi$.*

For a process $P$ and policy $\pi$, let us write$^6$ $P \Vdash \pi$ to express that $P$ is *coherent* for $\pi$, i.e., $P$ is coherent and conforms to policy $\pi$. If $P \Vdash \pi$ then the alphabet

<footnote>$^6$ In Milner’s notation we would write $P : \pi$, but we already use the colon ‘:’ for blocking sets as in CCS$^\text{Ph}$.</footnote>
of $\pi$ corresponds to the sort $\mathcal{L}(P)$ in CCS. It gives an upper bound on the labels that can be used by the process, and the precedence relation in $\pi$ provides a static over-approximation of the blocking, i.e., which labels can be in a choice conflict with each other. As a notational shortcut we will write $P \Vdash \ell_1 \dashv\dashv \ell_2$ to say that there is a policy $\pi$ with $P \Vdash \pi$ and $\ell_1 \dashv\dashv \ell_2 \in \pi$. Analogously, we write $P \Vdash \ell_1 \diamond \ell_2$ if there is a policy $\pi$ with $\ell_1 \diamond \ell_2 \in \pi$ and $P \Vdash \pi$.

**Example 11.** The most permissive policy for a given sort $L \subseteq \mathcal{L}$, written $\pi_{max}(L)$, contains all labels from $L$ as its alphabet but no precedences, i.e., $\ell_1 \diamond \ell_2 \in \pi_{max}(L)$ for all $\ell_1, \ell_2 \in L$. If $P \Vdash \pi_{max}$ then $P$ has sort $L$ and will permit arbitrarily concurrent processes to consume its labels $L$ under c-enabling. The most restrictive policy, $\pi_{min}(L)$, has alphabet $L$, but full precedences, i.e., $\ell_1 \dashv\dashv \ell_2 \in \pi_{min}$ for all $\ell_1, \ell_2 \in L$. If $P \Vdash \pi_{min}(L)$, then $P$ does not permit any concurrency; it can only communicate with a single sequential thread.

**Example 12.** Reflexive precedences $\ell \dashv\dashv \ell \in \pi$ play a special role. They permit a conformant $P \Vdash \pi$ and its derivatives to execute $\ell$ only with a single partner. For instance, ABRO from Ex. 7 satisfies ABRO $\nVdash r \diamond r$ and so ABRO $|\sigma.\bar{r}$ reduces but ABRO $|\sigma.\bar{r} | \sigma.\bar{r}$ will block after the initial clock transition. In contrast, if the policy specifies $\ell \diamond \ell \in \pi$, then in a process $P \Vdash \pi$ any $\ell$-transition is consumable arbitrarily often. For instance, the Esterel signal from Ex. 6 has $S_1 \Vdash \mathit{pres} \diamond \mathit{pres}$ and so $S_1 | \mathit{pres} | \mathit{pres}$ will not block.

We are interested in processes that conform to policies with special properties.

**Definition 8 (Pivot and precedence-closed policy).** A policy $\pi = (L, \dashv\dashv)$ is called

- *pivotable*, if $\overline{L} \subseteq L$ and for all $\ell_1, \ell_2 \in L$ with $\ell_1 \neq \ell_2$ we have $\ell_1 \diamond \ell_2 \in \pi$ or $\overline{\ell_1} \diamond \overline{\ell_2} \in \pi$.

- *precedence-closed* for $L \subseteq \mathcal{L}$, if $\ell_1 \in L$ and $\ell_1 \dashv\dashv \ell_2 \in \pi$ implies $\ell_2 \in L$.

$P$ is *pivotable/precedence-closed* if $P$ conforms to *pivot/precedence-closed policy*.

**Example 13.** An Esterel signal (Ex. 6) has the alphabet $\{\mathit{emit}, \mathit{pres}, \mathit{abs}\} = \mathcal{L}(S_i)$ ($i \in \{1, 2\}$) and for simplicity we ignore the clock $\sigma$) and is conformant to the policy **psig** with $\mathit{emit} \dashv\dashv \mathit{abs} \in \mathit{psig}$. A typical program $R$ accessing the signal has alphabet $\{\overline{\mathit{pres}}, \mathit{abs}\} \subseteq \mathcal{L}(S_i)$ and is of form $R = \overline{\mathit{pres}}:\overline{\mathit{pres}}.R_1 + \mathit{abs}:\{\mathit{abs}, \overline{\mathit{pres}}\}.R_0$. If the signal is present then $R_1$ is executed, if it is absent then $R_0$ is executed. Such $R$ conforms to a policy **prg** with $\overline{\mathit{pres}} \dashv\dashv \mathit{abs} \in \mathit{prg}$ and $\ell \dashv\dashv \ell \in \mathit{prg}$ for $\ell \in \{\overline{\mathit{pres}}, \mathit{abs}\}$. Both **psig** and **prg** as well as their union **psig** $\cup$ **prg** are pivot policies, so that $R|S_i$ is pivotable. In a pivotable process, conflicting choices are resolved by the precedences in a single thread, acting as the “pivot”. In $R|S_i$ the pivot is the signal $S_i$ on reading, resolving the choice $\overline{\mathit{pres}}+\mathit{abs}$ in $R$, and it is the program $R$ on writing, resolving the choice $\mathit{abs}+\mathit{emit}$ in $S_i$.

Non-pivotable processes, in general, may block because of two threads entering into a circular precedence deadlock with each other.
*Example 14.* Let the processes $P \stackrel{\text{def}}{=} a:b.A + b$ and $Q \stackrel{\text{def}}{=} \bar{b}:\bar{a}.B + \bar{a}$ from Ex 2. Their parallel composition $P|Q$ creates a deadlock under (even weak) enabling because of the contradicting precedences in the two possible interactions $a:b|\bar{a}$ and $b|\bar{b}:\bar{a}$. The deadlock is reflected in the non-pivotable policy $\pi$ of $P$ which must satisfy $b \dashv\dashv a \in \pi$ and $\bar{a} \dashv\dashv \bar{b} \in \pi$, violating both $a \diamond b \in \pi$ and $\bar{a} \diamond \bar{b} \in \pi$.

Reductions of pivotable processes never block because of two threads entering into a circular precedence deadlock with each other. This is a consequence of the fact that the race test in the rule (Com) never introduces the silent action $\tau$ into the blocking sets. Another feature of pivotable processes is that they cannot offer a clock action and exhibit reduction at the same time.

**Proposition 2 (Clock Maximal Progress).** Suppose $P$ is coherent and pivotable. If $\sigma \in iA(P)$ then $P$ is in normal form, i.e., there is no reduction $P \xrightarrow{\tau} P'$.

Prop. 2 says that in coherent pivotable processes clocks behave like time steps in standard timed process algebras. A clock is only possible on normal forms, i.e., if there is no reduction possible, which has been termed maximal progress [40, 15]. The advance over these classical theories is coherence, which guarantees that all reductions are confluent. A coherent pivotable process, no matter in which order the reductions are executed, when it terminates, computes a unique normal form. At this point it either stops if there is no clock possible, or it offers a clock step (pausing) to a continuation process from which a new normal form is produced. In this way, coherent pivotable processes correspond to clocked streams.

It remains to be seen how we can obtain coherent processes systematically by construction. The following Thm. 2 identifies a set of closure operators for coherent processes controlled by policy-conformance.

**Theorem 2 (Milner's Confluence Class Extended).**

1. (Idling) If $\mathcal{O} \models \pi$ for all policies $\pi$.

2. (Rendezvous Prefix) If $\mathcal{Q} \models \pi$, then for every $\ell \in \mathcal{R}$ we have $\ell:H.Q \models \pi$ if $\ell \in H \subseteq \{\ell' \mid \ell' \dashv\dashv \ell \in \pi\}$.

3. (Clock Prefix) If $\mathcal{Q} \models \pi$ and $\sigma \in \mathcal{C}$, then $\sigma:H.Q \models \pi$ if $H \subseteq \{\ell \mid \ell \dashv\dashv \sigma \in \pi\}$.

4. (Choice) If $P_1 \models \pi_1$ and $P_2 \models \pi_2$ and for all pairs of initial transitions $P \xrightarrow{\alpha_1} H_1 P_1$ and $P \xrightarrow{\alpha_2} H_2 P_2$ such that $\alpha_1 \neq \alpha_2$ as well as $\alpha_1 \in H_2$ or $\alpha_2 \in H_1$, then $P_1 + P_2 \models \pi$ if $\pi_1 \subseteq \pi$ and $\pi_2 \subseteq \pi$.

5. (Parallel) If $\mathcal{Q} \models \pi$ and $\mathcal{R} \models \pi$ where $\pi \setminus \mathcal{R}$ is a pivot policy, then $(\mathcal{Q} | \mathcal{R}) \models \pi$.

6. (Hiding) If $\mathcal{Q} \models \pi$ and $\sigma \dashv\dashv \ell \notin \pi$ for all $\sigma \in \mathcal{L}$ and $\ell \in \pi$, then $\mathcal{Q} / \mathcal{L} \models \pi / \mathcal{L}$.

7. (Restriction) If $\mathcal{Q} \models \pi$ and $\pi$ precedence-closed for $L \cup \bar{L}$, then $(\mathcal{Q} \setminus L) \models \pi \setminus L$.

Thm. 2 is our generalisation of Milner's Confluence Class [36] in CCS$^{\text{spt}}$, and the main result of the paper. It shows that by decorating processes with policies (*policy typing*), we can identify processes as being coherent, thereby verifying they can be run deterministically in the scheduled SOS semantics of CCS$^{\text{spt}}$. Note that pivotability is crucial in the case (5) of parallel composition. It replaces Milner's "separation conditions" as explained in the next section.
## 5 Conservative Extension

The key result of Milner [36] (Chap. 11, Prop. 19) is that confluence is preserved by inaction 0, prefixing $ℓ.P$ and confluent composition defined as

$$P|_L Q \stackrel{\text{def}}{=} (P|Q) \setminus L$$

subject to the separation conditions $\mathcal{L}(P) \cap \mathcal{L}(Q) = \{\}$ and $\overline{\mathcal{L}(P)} \cap \mathcal{L}(Q) \subseteq L \cup \overline{L}$. Thm. 2(5) is our generalisation of confluent composition. The following Def. 9 captures the connection with Milner's confluence theory more generally. We assume that all processes are unlocked, i.e., each prefix $ℓ:H.Q$ has $H \cup \{ℓ\} \subseteq A \cup \overline{A}$.

**Definition 9 (Milner's Confluence Class).** Milner's confluence class $\mathcal{CCS}^{cc} \subseteq P$ is the set of (unclocked) processes $P$ of $\mathcal{CCS}^{spt}$ such that for all derivatives $Q$ of $P$, if $Q \xrightarrow{\alpha/E} H Q'$, the following holds:

1. If $\alpha \neq \tau$ then $H = \{\alpha\}$ and $\alpha \notin iA^*(E)$.

2. If $\alpha = \tau = \ell | \bar{\ell}$ then $H = \{\}$ and $\{\ell, \bar{\ell}\} \cap iA^*(E) = \{\}$.

Condition (1) in Def. 9 essentially expresses that all actions $\alpha:H[E]$ are self-blocking (discrete) and can only be offered by a single thread. This corresponds to Milner's separation condition $\mathcal{L}(R_1) \cap \mathcal{L}(R_2) = \{\}$ for confluent compositions $(R_1 | R_2) \setminus L$ inside derivative process $Q$. Condition (2) in Def. 9 generalises the second part of the separation condition, $\overline{\mathcal{L}(R_1)} \cap \mathcal{L}(R_2) = L \cup \overline{L}$, for confluent compositions inside $Q$. It states that all reductions $\tau = \ell | \bar{\ell}$ are enabled and the actions $\ell$ and $\bar{\ell}$ are fully restricted to the two threads synchronising in the rendezvous. We recover Milner's result as a special case: Whenever $P, Q \in \mathcal{CCS}^{cc}$ and both $\mathcal{L}(P) \cap \mathcal{L}(Q) = \{\}$ and $\overline{\mathcal{L}(P)} \cap \mathcal{L}(Q) = L \cup \overline{L}$, then $(P|Q) \setminus L \in \mathcal{CCS}^{cc}$. Along these lines we state the following conservativity without proof:

**Proposition 3 (Conservative Extension).** For all $P \in \mathcal{CCS}^{cc}$, $P$ is coherent iff $P$ is confluent. Moreover, a transition of $P$ is c-enabled iff it is admissible.

The motivation of our work is that $\mathcal{CCS}^{cc}$ is too limited a class to model deterministic shared memory such as used in synchronous languages like Esterel. Specifically, we need coherence of broadcast actions with repetitive prefixes. Our theory (Thm. 2) identifies a much larger class of processes that does the job.

## 6 Conclusion and Further Work

For our extension of Milner's confluence theory, priorities are instrumental, and so we build on extensions of CCS with priorities. As indicated, $\mathcal{CCS}^{Ph}$ [42] corresponds to the theory of irreflexive (unclocked) processes of $\mathcal{CCS}^{spt}$ under weak enabling. Likewise the theories [13, 45] can be subsumed in $\mathcal{CCS}^{spt}$ under weak enabling. Specifically, the prioritised sum operator $P \vdash Q$ of [13] can be coded as $P + Q:iA(P)$ in $\mathcal{CCS}^{spt}$. The theory [45] proposes two levels of labels, $a:0$ and $a:1$, where 0 denotes higher priority and 1 ordinary priority. Translated into
CCS$^{spt}$, the prefix a:0.P corresponds to a:{} .P while an action prefix a:1.P maps
in CCS$^{spt}$ to a:Prio.P if we define Prio as the set of all high-prioritised labels.

One can show that for coherent pivotable processes of at most two threads,
the operational semantics of CCS (admissible), of CCS<sup>Ph</sup> (weak enabling) and our
CCS<sup>spt</sup> (constructive enabling) all coincide. However, in the scenario of determin-
istic shared memory, we are looking at more than two processes: two competing
program threads (at least) and one shared memory (at least) with repetitive
shared prefixes. For this, neither CCS nor any of CCS<sup>Ph</sup> or the theories [13, 45]
are sufficient. For the key necessary step, taken in CCS<sup>spt</sup>, is to pass from weak
enabling to constructive enabling. As indicated in this paper, constructive en-
abling is the corner stone in the semantics of Esterel [7]. We leave the formal
proof of equivalence to a follow-up paper.

The second element borrowed from classical process algebra is the notion of
clocks. While PMC [21] has clocks but no priorities, in TPL [25] and CSA [15]
the priorities are hardwired and express precedence only between the rendezvous
actions and a single clock. For contrast, here we use a fully general priority
scheme as in Phillips' CCS<sup>Ph</sup> [42]. By adding clocks to CCS<sup>Ph</sup> we generalise these
earlier clocked extensions of CCS, for expressing precedence between rendezvous
actions and between multiple clocks.

We finally list in spare order some possible future works:

* We envisage that CCS<sup>spt</sup>, extended by process-passing, can be used as a play-
  ground to study compositional embeddings of concurrent λ-calculi. In particular,
  the ones with sharing, for instance [2] or as required for the lazy semantics of
  Haskell, and with deterministic memory such as IVars/TVars [34] and LVars [29].

* We plan to study the interaction of coherence with forms of congruence (static, dynamic and interaction laws in Milner’s jargon) and notions of bisimulation.

* We plan to generalise the interaction model of CCS<sup>spt</sup> to synchronisation alge-
  bras permitting action fusion in the spirit of Milner’s ASCCS and Austry and
  Boudol’s Meije [35, 4]. This will permit us to develop a theory of timing ab-
  straction, by making process synchronise not only at micro-step level but on full
  macro-steps.

* Thm. 2 suggests using policies as types. Among possible type disciplines we just mention: behavioural type systems [3], including session-types [27] and multi-party session-types [50] to capture rendezvous and group interactions; intersection-types [5, 6], including non-idempotent ones [14], to characterise termination and resources awareness, and linear-types [48] to model consuming resources.

* Clocks are unordered in CCS<sup>spt</sup>: introducing a partial order à la Lamport [30] could be an interesting, although economic and fine grained, way to reason about time and time priorities.

* Scaling up our theory from CCS to *Π*-calculus, the higher-order process algebra par excellence, would not simply be a stylistic exercise. Challenges, such as causal dependencies introduced by scope extrusion, are significant and deserve careful analysis, as discussed in [16]. Event structures à la Winskel [49] could undoubtedly play a pivotal role in addressing these issues.
References

1. Aguado, J., Mendler, M., v. Hanxleden, R., Fuhrmann, I.: Grounding synchronous deterministic concurrency in sequential programming. In: Proc. of ESOP, LNCS 8410. pp. 229–248. Springer (2014)

2. Amadio, R.M.: A synchronous pi-calculus. Inf. Comput. 205(9), 1470–1490 (2007)

3. Ancona, D., Bono, V., Bravetti, M., Campos, J., Castagna, G., Deniélou, P., Gay, S., Gesbert, N., Giachino, E., Hu, R., Johnsen, E., Martins, F., Mascardi, V., Montesi, F., Neykova, R., Ng, N., Padovani, L., Vasconcelos, V., Yoshida, N.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2-3), 95–230 (2016)

4. Austry, D., Boudol, G.: Algèbre de processus et synchronisation. Theor. Comput. Sci. 30, 91–131 (1984)

5. Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symb. Log. 48(4), 931–940 (1983)

6. Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in logic, Cambridge University Press (2013)

7. Berry, G.: The Constructive Semantics of Pure Esterel. Draft Book (1999)

8. Berry, G.: The Foundations of Esterel. In: Proof, Language and Interaction: Essays in Honour of Robin Milner. pp. 425–454. MIT Press (2000)

9. Berry, G., Boudol, G.: The chemical abstract machine. Theor. Comput. Sci. 96(1), 217–248 (1992)

10. Bocchino, R., Adve, V., Adve, S., Snir, M.: Parallel programming must be deterministic by default. In: Proceedings of the First USENIX conference on Hot topics in parallelism. pp. 4–4 (2009)

11. Bourke, T., Pouzet, M.: Zélus: a synchronous language with odes. In: Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC 2013, April 8-11, 2013, Philadelphia, PA, USA. pp. 113–118. ACM (2013)

12. Boussinot, F., De Simone, R.: The SL synchronous language. IEEE Transactions on Software Engineering 22(4), 256–266 (1996)

13. Camilleri, J., Winskel, G.: CCS with priority choice. Information and Computation 116(1), 26–37 (1995)

14. de Carvalho, D., de Falco, L.T.: A semantic account of strong normalization in linear logic. Inf. Comput. 248, 104–129 (2016)

15. Cleaveland, R., Lüttgen, G., Mendler, M.: An algebraic theory of multiple clocks. In: Proc. of CONCUR. pp. 166–180. No. 1243 in LNCS (1997)

16. Crafa, S., Varacca, D., Yoshida, N.: Event structure semantics of parallel extrusion in the pi-calculus. In: Proc. of FOSSACS. Lecture Notes in Computer Science, vol. 7213, pp. 225–239. Springer (2012)

17. Dieckert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific (1995)

18. Edwards, S.A.: On determinism. In: et. al., M.L. (ed.) Lee Festschrift, pp. 240–253. Springer (2018)

19. Esterel Technologies: The Esterel v7 reference manual version v7_30 – initial IEEE standardization proposal. Tech. rep., Esterel Technologies (2005)

20. Guernic, P.L., Goutier, T., Borgne, M.L., Maire, C.L.: Programming real time applications with SIGNAL. In: Proceedings of the IEEE. vol. 79, pp. 1321–1336. IEEE Press (1991)

21. H. R. Andersen, M.M.: An asynchronous process algebra with multiple clocks. In: Sannella, D. (ed.) In Proc. ESOP. pp. 58–73 (1994)
22. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE 79(9), 1305–1320 (1991)

23. von Hanxleden, R., Duderstadt, B., Motika, C., Smyth, S., Mendler, M., Aguado, J., Mercer, S., O’Brien, O.: SCCharts: Sequentially Constructive Statecharts for safety-critical applications. In: Proc. of PLDI. ACM (2014)

24. Harel, D., Pnueli, A., Pruzan-Schmidt, J., Sherman, R.: On the formal semantics of Statecharts. In: Proc. of LICS. pp. 54–64. IEEE Press (1987)

25. Hennessy, M., Regan, T.: A process algebra for timed system. Information and Computation 117, 221–239 (1995)

26. Hoare, C.: Communicating Sequential Processes. Prentice-Hall (1985), 256 pages

27. Hüttel, H., Lanese, I., Vasconcelos, V., Caires, L., Carbone, M., Deniélou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1–3:36 (2016)

28. Kloos, C.D., Breuer, P. (eds.): Formal Semantics for VHDL. Kluwer (1995)

29. Kuper, L., Newton, R.: Lvars: lattice-based data structures for deterministic parallelism. In: Functional High-Performance Computing. p. 71–84. ACM, New York, NY, USA (2013)

30. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. In: Malkhi, D. (ed.) Concurrency: the Works of Leslie Lamport, pp. 179–196. ACM (2019)

31. Lee, E.A.: The problem with threads. Computer 39(5), 33–42 (2006)

32. Lin, S., Manerkar, Y.A., Lohstroh, M., Polgreen, E., Yu, S., Jerad, C., Lee, E.A., Seshia, S.A.: Towards building verifiable CPS using Lingua Franca. ACM Trans. Embed. Comput. Syst. 22(5s), 155:1–155:24 (2023)

33. Lüttgen, G., von der Beeck, M., Cleaveland, R.: Statecharts via process algebra. In: Proc. of CONCUR. LNCS, vol. 1664, pp. 399–414. Springer (1999)

34. Marlow, S.: Parallel and concurrent programming in haskell. In: CEFP 2011. pp. 339–401 (2012)

35. Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, 267–310 (1983)

36. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

37. Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)

38. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1–40 (1992)

39. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, II. Inf. Comput. 100(1), 41–77 (1992)

40. Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: theory and application. Inf. Comput. 114(1), 131–178 (1994)

41. Norton, B., Luettgen, G., Mendler, M.: A compositional semantic theory for component-based synchronous design. In: Proc. of CONCUR. pp. 461–476. Springer LNCS 2761 (2003)

42. Phillips, I.: CCS with priority guards. In: Larsen, K.G., Nielsen, M. (eds.) Proc. of CONCUR. pp. 305–320 (2001)

43. Plotkin, G.D.: The origins of structural operational semantics. J. Log. Algebraic Methods Program. 60-61, 3–15 (2004)

44. Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebraic Methods Program. 60-61, 17–139 (2004)

45. R. Cleaveland, G. Lüettgen, V.N.: Handbook of Process Algebra, chap. Priority in Process Algebra. Elsevier (2001)
46. Schneider, K.: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern (2009)

47. Unger, S.: Asynchronous sequential switching circuits with unrestricted input changes. IEEE Transactions on Computers C-20(12), 1437-1444 (1971)

48. Wadler, P.: Linear types can change the world! In: Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods. p. 561. North-Holland (1990)

49. Winskel, G.: Event structures. In: Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986. Lecture Notes in Computer Science, vol. 255, pp. 325-392. Springer (1986)

50. Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: Proc. of ICDCIT. LNCS, vol. 11969, pp. 73-93. Springer (2020)

A Inside Esterel's ABRO encoding in CCS<sup>spt</sup>

This appendix offers a more deep view of the ABRO encoding presented in the paper: for reader's confort ABRO encoding in CCS<sup>spt</sup> look like this:

$$
\begin{align*}
\text{ABRO} &\stackrel{\text{def}}{=} (A | B | R | O) \setminus s \\
A &\stackrel{\text{def}}{=} k:k.0 + a:\{k, a\}.\bar{s}:\bar{s}.0 + \sigma:\{k, a\}.A \\
B &\stackrel{\text{def}}{=} k:k.0 + b:\{k, b\}.\bar{s}:\bar{s}.0 + \sigma:\{k, b\}.B \\
R &\stackrel{\text{def}}{=} r:r.R' + \sigma:r.R \\
R' &\stackrel{\text{def}}{=} \bar{k}.R' + \sigma:\bar{k}.(A | B | R | O) \\
O &\stackrel{\text{def}}{=} k:k.0 + s:k.O' + \sigma:\{k, s\}.O \\
O' &\stackrel{\text{def}}{=} k:k.0 + s:k.\bar{o}:\bar{o}.0 + \sigma:\{k, s\}.O'.
\end{align*}
$$

We use a single (multi-cast) kill signal $k$ shared between A, B, and O: The reset process $R$ keeps sending $\bar{k}$ unboundedly often, until all target processes have received a copy and all receptions $k$ have been consumed. At that point, it takes a clock step to repeat ABRO from the start. One can verify that ABRO is coherent and pivotable using Thm. 2.

- The choices in each of the threads A, B, R, O are fully resolved by the blocking sets, i.e., every pair of actions in the summations are distinct and in precedence relationships. Every rendezvous prefix is self-blocking unless the action can be repeated with the same blocking in the continuation process. This happens for channels $s$ and $k$ in the recursions $O \stackrel{\text{def}}{=} \dots + s:k.O + \dots$ and $R' \stackrel{\text{def}}{=} \bar{k}.R' + \dots$. Thus, the threads A, B, R, O themselves are coherent.

- A suitable policy $\pi$, for which the threads A, B, R, O are coherent, enforces the precedences

* $k \dashrightarrow \ell \in \pi$ for $\ell \in \{k, a, b, s, \sigma\}$

* $\ell \dashrightarrow \ell \in \pi$ for $\ell \in \{r, k, a, b, \bar{s}, \bar{o}\}$

* $\ell \dashrightarrow \sigma \in \pi$ for $\ell \in \{a, b, s\}$.
The dual matching pairs for these precedences, however, are all concurrently independent. More precisely, we look at distinct labels, $\bar{k} \diamond \bar{l} \in \pi$ for all $\ell \in \{r, o, a, b, s, \sigma\}$, and we have $\bar{l} \diamond \sigma \in \pi$ for $\ell \in \{r, o, a, b, s\}$.

- Thus, the policy $\pi$ (and thus $\pi \setminus \mathcal{R}$) is a pivot policy and so the parallel composition $A|B|R|O$ is coherent for $\pi$. Further, $\pi$ is precedence-closed for $\{s\}$ which means that $(A|B|R|O) \setminus s$ is coherent for $\pi \setminus \{s\}$. Finally, since $\{\ell \mid \ell \dashrightarrow \sigma \in \pi \setminus \{s\}\} = \{a, b\}$, the process ABRO (which starts with a prefix $\sigma: H$ where $H = \{\}$) is coherent for $\pi \setminus \{s\}$. $\square$

# B Main Proofs

We start with some auxiliary lemmas and propositions.

**Lemma 1.** Let $P, Q$ be processes:

1. $P \xrightarrow{\sigma_R} Q$ implies $R \equiv 0$.

2. $\alpha \in iA(P)$ iff $P \stackrel{\alpha}{\to} Q$.

3. $iA(P) \cap \mathcal{R} \subseteq iA(P|Q)$.

4. $i\bar{A}^*(P) \subseteq \bar{iA}^*(P|Q)$.

5. If $P$ is single-threaded, then $P \xrightarrow{\alpha_R} H$ implies $\alpha \in \mathcal{L}, R \equiv 0$ and $\tau \notin H$.

6. If $P \xrightarrow{\alpha_R} H$ then $iA(R) \subseteq iA(P)$.

*Proof.* (2) is by definition. The other points follow by an inspection of the SOS rules, using the definition of $iA(P)$.

Lem. 1(1) means that clock actions always run in an empty concurrent environment. Observe that Lem. 1(2) means that the set $iA(P)$ corresponds to the initial actions of $P$. The presence of $\tau$ in the blocking set of a transition provides information about the set of initial actions of a process. Specifically, in rule (Com) the presence of $\tau$ in the set $H = \text{race}(P|Q)$ indicates a blocking situation arising from the priorities in $P$ or $Q$ conflicting with the rendevous actions $\ell$ or $\bar{l}$. Thus, the condition $\tau \notin H$ can be used to implement priority-based scheduling. Lem. 1(5) implies that single-threaded processes are never blocked.

**Lemma 2.** Let $P$ be an arbitrary process:

1. $iA(P) \cap \mathcal{L} \subseteq iA^\tau(P) \subseteq iA^*(P)$.

2. If $P \equiv Q$ then $iA^*(P) = iA^*(Q)$.

3. If $P \stackrel{\alpha}{\to} Q$ for $\alpha \in \mathcal{R} \cup \{\tau\}$, then $iA^*(Q) \subseteq iA^*(P)$.

*Proof.* All points follow by an inspection of the SOS rules, using the definition of $iA^\tau(P)$ and $iA^*(P)$.
On Interference.

**Proposition 4.** Suppose $\alpha_1:H_1[E_1|R]$ and $\alpha_2:H_2[E_2|R]$ are interference-free. Then, $\alpha_1:H'_1[E_1]$ and $\alpha_2:H'_2[E_2]$ are interference-free for arbitrary subsets $H'_1 \subseteq H_1$ and $H'_2 \subseteq H_2$.

As a special case, choosing $R = 0$, Proposition 4 implies non-interference of $\alpha_i:H'_i[E_i]$ for $i \in \{1, 2\}$ from non-interference of $\alpha_i:H_i[E_i]$ for any $H'_i \subseteq H_i$.

*Proof.* We first show $\alpha_i:H'_i[E_i]$ are c-enabled. As $\alpha_i:H_i[E_i|R]$, we know that $H_i \cap (i\bar{A}^*(E_i|R) \cup \tau) = \emptyset$, and we also know that $H'_i \subseteq H_i$ and, by Lem. 1, that $i\bar{A}^*(E_i) \subseteq i\bar{A}^*(E_i|R)$, therefore the transitions are still c-enabled. Moreover, as either $\alpha_1 \neq \alpha_2$ or $\alpha_{3-1} \notin H_i \supseteq H'_i$, these transitions are interference-free.

*On Policies.* We obtain a partial ordering $\pi_1 \le \pi_2$ on precedence policies by subset inclusion. Specifically, we have $(L_1, \dashv\dashv_1) \le (L_2, \dashv\dashv_2)$ if $L_1 \subseteq L_2$ such that for all $\ell_1, \ell_2 \in L_1$, if $\ell_1 \dashv\dashv_2 \ell_2$ then $\ell_1 \dashv\dashv_1 \ell_2$. Intuitively, if $\pi_1 \le \pi_2$ then $\pi_2$ is a tightening of $\pi_1$ in the sense that it exports more labels (resources) subject to possibly fewer precedences (causality constraints) than $\pi_1$. By way of this ordering, we can use policies to measure the degree of concurrency exhibited by a process. The alphabet of the $\le$-maximal policy $\pi_{max}$ contains all labels $\mathcal{L}$ and its precedence relation $\dashv\dashv_{max}$ is empty. It is the largest policy in the $\le$ ordering. The $\le$-minimal policy $\pi_{min}$ has empty alphabet and empty precedences. It is self-dual, i.e., $\bar{\pi}_{min} = \pi_{min}$.

There is also the normal inclusion ordering $\pi_1 \subseteq \pi_2$ between policies defined by $L_1 \subseteq L_2$ and $\dashv\dashv_1 \subseteq \dashv\dashv_2$. It differs from $\le$ in the inclusion direction of the precedence alphabets.

For any policy $\pi$ on alphabet $L$ we define its dual as a policy $\bar{\pi}$ on the set of labels $\overline{L}$ where for all $\overline{\ell}_1, \overline{\ell}_2 \in \overline{L}$ we stipulate $\overline{\ell}_1 \dashv\dashv \overline{\ell}_2 \in \bar{\pi}$ iff $\ell_1 = \ell_2$ or $\ell_1 \diamond \ell_2 \in \pi$, i.e., both $\ell_1 \dashv\dashv \ell_2 \notin \pi$ and $\ell_2 \dashv\dashv \ell_1 \notin \pi$. Intuitively, the dual policy $\bar{\pi}$ consists of matching copies $\overline{\ell}$ of all labels $\ell$ from $\pi$ and puts them in a precedence relation precisely if their original copies are identical or do not stand in precedence to each other, in any direction. This generates a form of “negation” $\bar{\pi}$ from $\pi$, which is reflexive and symmetric. Note that $\bar{\pi}$ need not be identical to $\pi$ but contains more precedences. In general, we have $\bar{\pi} \le \pi$ and $\bar{\pi} = \pi$ if $\pi$ is symmetric. The policy $\bar{\pi}$ captures the independences between actions of $\pi$ and is called the associated *independence alphabet*, in the sense of trace theory [17]. Analogously, $\bar{\pi}$ expresses the dependencies of actions in $\pi$, called the associated *dependence alphabet*.

*Example 15.* Suppose $P \models \ell_1 \diamond \ell_2$ then all transitions with labels $\ell_1$ and $\ell_2$ of $P$ must be from concurrent threads and thus cannot block each other. For instance, both $\ell_1 | \ell_2$ and $\ell_1 + \ell_2$ conform to $\ell_1 \diamond \ell_2$, but the choice $\ell_1 + \ell_2$ is not coherent. It becomes coherent if we add a precedence $\ell_1 + \ell_2:\ell_1$ but then it is not longer conformant to $\ell_1 \diamond \ell_2$. Instead, we now have $\ell_1 + \ell_2:\ell_1 \models \ell_1 \dashv\dashv \ell_2$, where the policy expresses the precedence coded in the blocking sets of the prefixes. More generally, if $\ell_1 \dashv\dashv \ell_2 \in \pi$ and $\ell_1 \neq \ell_2$, then $P \models \pi$ may take $\ell_1$ and $\ell_2$ transitions to completely different states from the same thread.
**Definition 10 (Pivot Policy).** A policy $\pi$ is called a pivot policy if $\bar{\pi} \le \pi$. We call a process $P$ pivotable if $P$ conforms to a pivot policy.

**Proposition 5.** A policy $\pi = (L, \dots)$ is a pivot policy if $\bar{L} \subseteq L$ and for all $\ell_1, \ell_2 \in L$ with $\ell_1 \ne \ell_2$ we have $\ell_1 \diamond \ell_2 \in \pi$ or $\bar{\ell}_1 \diamond \bar{\ell}_2 \in \pi$.

*Proof.* Let $\pi$ be a pivot policy. Since the alphabet of $\bar{\pi}$ is $\bar{L}$ and the alphabet of $\pi$ is $L$ the assumption $\bar{\pi} \le \pi$ implies $\bar{L} \subseteq L$ by definition of $\le$. Given labels $\ell_1, \ell_2 \in L$ with $\ell_1 \ne \ell_2$ suppose $\ell_1 \diamond \ell_2 \notin \pi$. Hence $\ell_1 \dashrightarrow \ell_2 \in \pi$ or $\ell_2 \dashrightarrow \ell_2 \in \pi$. Consider the first case, i.e., $\ell_1 \dashrightarrow \ell_2 \in \pi$. Since $\bar{L} \subseteq L$ and $L = \bar{\bar{L}}$ it follows that also $L \subseteq \bar{L}$, i.e., the labels $\ell_i$ are also in the alphabet of $\bar{\pi}$. But then by definition of the ordering and the fact that $\ell_i = \bar{\ell}_i$, the assumption $\bar{\pi} \le \pi$ implies that $\bar{\bar{\ell}}_1 \dashrightarrow \bar{\bar{\ell}}_2 \in \bar{\pi}$. Now, the definition of the dual policy means that $\bar{\ell}_1 \dashrightarrow \bar{\ell}_2 \notin \pi$ and $\bar{\ell}_2 \dashrightarrow \bar{\ell}_1 \notin \pi$. This is the same as $\bar{\ell}_1 \diamond \bar{\ell}_2 \in \pi$ as desired.

Suppose the properties (1) and (2) of the proposition hold for a policy $\pi$. We claim that $\bar{\pi} \le \pi$. The inclusion of alphabets is by assumption (1). Then, suppose $\bar{\ell}_1 \dashrightarrow \bar{\ell}_2 \in \pi$ which implies $\bar{\ell}_1 \diamond \bar{\ell}_2 \notin \pi$. If $\ell_1 = \ell_2$ we have $\bar{\ell}_1 \dashrightarrow \bar{\ell}_2 \in \bar{\pi}$ directly by definition. So, let $\ell_1 \ne \ell_2$. Because of $\bar{L} \subseteq L$ and (2) this gives us $\ell_1 \diamond \ell_2 \in \pi$ considering again that $\ell_i = \bar{\ell}_i$. But $\ell_1 \diamond \ell_2 \in \pi$ is the same as $\bar{\ell}_1 \dashrightarrow \bar{\ell}_2 \in \bar{\pi}$ by definition.

**Proposition 6.** Suppose $P$ conforms to $\pi_{is}$ and $P \xrightarrow{\alpha} {}_R H$ $Q$ for some $\alpha$, $H$, $R$, $Q$. Then:

1. If $\alpha \in \overline{\mathcal{A}}$ then $H \subseteq \{\alpha, \tau\}$.

2. If $\alpha \in \mathcal{A} \cup \mathcal{C} \cup \{\tau\}$ then $H \subseteq \mathcal{A} \cup \mathcal{C} \cup \{\tau\}$.

*Proof.* Obvious by definition of conformance and the construction of $\pi_{is}$.

The next lemma implies that two coherent threads cannot block each other if they are conformant to the same pivot policy. The blocking of a reduction $\ell | \bar{\ell}$ must always arise from a thread in the concurrent context that is not involved in the synchronisation.

**Lemma 3.** Let $P_1 \dashv \pi$ and $P_2 \dashv \pi$ be coherent for the same pivot policy $\pi$ and $\ell \in \mathcal{L}$ such that $P_1 \xrightarrow{\ell} {}_R H_1 P'_1$ and $P_2 \xrightarrow{\bar{\ell}} {}_R H_2 P'_2$. Then, $H_2 \cap \overline{i\mathcal{A}}(R_1) = \{\}\}$ implies $H_2 \cap \overline{i\mathcal{A}}(P_1) \subseteq \{\bar{\ell}\}$.

*Proof.* Let $\ell \in \mathcal{L}$ and the transitions be given as in the statement of the lemma. Suppose $\alpha \in H_2$ and $\alpha \in \overline{i\mathcal{A}}(P_1)$. We claim that $\alpha = \bar{\ell}$, whence $H_2 \cap \overline{i\mathcal{A}}(P_1) \subseteq \{\bar{\ell}\}$. By contraposition let us assume that $\alpha \ne \bar{\ell}$, or equivalently $\bar{\alpha} \ne \ell$. Further, since $i\mathcal{A}(P_1) \subseteq \mathcal{L}$ we also have $\alpha \ne \tau$. The assumption $\alpha \in H_2$ means $\alpha \dashrightarrow \bar{\ell} \in \pi$ by Def. 5(1) applied to $P_2$. Since $\pi$ is pivot we must thus have $\bar{\alpha} \diamond \ell \in \pi$, specifically $\bar{\alpha} \dashrightarrow \ell \notin \pi$, i.e., $\bar{\alpha} \notin H_1$, again by Def. 5(1), now applied to $P_1$. But since $\bar{\alpha} \in i\mathcal{A}(P_1)$, by Lem. 1, there is a transition $P_1 \xrightarrow{\bar{\alpha}} {}_E H$ $Q$. Since also $\ell \dashrightarrow \bar{\alpha} \notin \pi$, by pivot property, it follows $\ell \notin H$ by Def. 5(1) again for $P_1$. Now both $\bar{\alpha} \notin H_1$
and $\ell \notin H$ mean that the c-actions $\ell:H_1[R_1]$ and $\bar{\alpha}:H[E]$ are interference-free (Def. 11). Since $\ell \neq \bar{\alpha}$ there must exist a reconvergent process $R$ and transitions

$$P'_1 \xrightarrow{\bar{\alpha} / E'} H' R \text{ and } Q \xrightarrow{\ell / R'_1} H'_1 R \text{ with } R_1 \xrightarrow{\bar{\alpha}} R'_1 \text{ and } E \xrightarrow{\ell} E'$$

The latter transitions are strengthenings of the residuals $R_1 \rightsquigarrow \bar{R}'_1$ and $E \rightsquigarrow E'$ that must exist according to the statement of Coherence, because of $\{\ell, \bar{\alpha}\} \subseteq \mathcal{R}$ and $\ell \neq \bar{\alpha}$. However, the transition $R_1 \xrightarrow{\bar{\alpha}} \bar{R}'_1$ implies $\bar{\alpha} \in i\mathcal{A}(R_1)$ which is impossible, because then $\alpha \in H_2 \cap i\bar{\mathcal{A}}(R_1)$ while $H_2 \cap i\bar{\mathcal{A}}(R_1) = \{\}$ by assumption. We can show that pivotable processes do not have internal races.

**Lemma 4.** Let $P \models \pi$ be coherent for a pivot policy $\pi$. Then, for every reduction $P \xrightarrow{\tau/E} H' P'$, if $H \cap i\bar{\mathcal{A}}(E) = \{\}$ then $\tau \notin H$.

*Proof.* Let $P$ be coherent for pivotable $\pi$ and a reduction $P \xrightarrow{\tau/E} H' P'$ such that $H \cap i\bar{\mathcal{A}}(E) = \{\}$ be given. Suppose, by contraposition, $\tau \in H$. Since there are no action prefixes $\tau.P'$ in $\mathbf{CCS}^{\text{spt}}$, the reduction must arise from a synchronisation of two threads $P_1$ and $P_2$ inside $P$, via rule (Com), i.e.,

$$\frac{P_1 \xrightarrow{\ell / R_1} H_1 P'_1 \quad P_2 \xrightarrow{\bar{\ell} / R_2} H_2 P'_2 \quad H' = \text{race}(P_1, P_2)}{P_1 | P_2 \xrightarrow{\ell | \bar{\ell} / R_1 | R_2} H_1 \cup H_2 \cup H' \quad P'_1 | P'_2} \quad (\text{Com})$$

for some $\ell \in \mathcal{L}$. The assumption $H \cap i\bar{\mathcal{A}}(E) = \{\}$ for the top-level reduction implies that $(H_1 \cup H_2) \cap i\bar{\mathcal{A}}(R_1 | R_2) = \{\}$ at the point of (Com). Here we may assume, by induction on the depth of the derivation, that $\tau \notin H_1 \cup H_2$. We must show that the synchronisation action $\tau$ cannot enter into the blocking set by (Com), i.e., $\tau \notin H'$, which is the same as $H_2 \cap i\bar{\mathcal{A}}(P_1) \subseteq \{\bar{\ell}\}$ and $H_1 \cap i\bar{\mathcal{A}}(P_2) \subseteq \{\ell\}$. The sub-expressions $P_1 \models \pi'$ and $P_2 \models \pi'$ are also coherent for a common pivot policy $\pi'$. This policy may contain local labels that are restricted or hidden in the outer process $P$. Since by assumption we have $H_1 \cap i\bar{\mathcal{A}}(R_1) \subseteq (H_1 \cup H_2) \cap i\bar{\mathcal{A}}(R_1 | R_2) = \{\}$ and likewise $H_2 \cap i\bar{\mathcal{A}}(R_2) = \{\}$, we can apply Lem. 3 to show $H_2 \cap i\bar{\mathcal{A}}(P_1) \subseteq \{\bar{\ell}\}$ and $H_1 \cap i\bar{\mathcal{A}}(P_2) \subseteq \{\ell\}$. This means $H' = \{\}$ and we are done.

**The Role of Pivotability.** Let us give an example to show that the requirement of pivotability cannot be removed in the closure statement for parallel compositions of Thm. 1. For compactness of notation let us write $\ell^r:H$ for $\ell:(H \cup \{\ell\})$ to create reflexive prefixes. Let

$$Q = b^r | c^r:a \text{ and } R = \bar{b}^r:\bar{a}.R_1 + \bar{c}^r:\bar{a}.R_2 \text{ with } R_1 = \bar{a}^r + \bar{c}^r:\bar{a} \text{ and } R_2 = \bar{a}^r + \bar{b}^r:\bar{a}.$$

First, we observe that both $Q$ and $R$ are coherent:

- Process $Q$ has two admissible transitions

$$Q \xrightarrow{b \atop 0} \{b\}^{c^r:a} \text{ and } Q \xrightarrow{c \atop 0} \{c,a\}^{b^r}$$
which both are self-interfering. Thus, reconvergence is required only between the two transitions which is guaranteed, because they are from concurrent threads. This can also be obtained from Thm. 2 and the pivot policy with $b \dashrightarrow b \in \pi$, $c \dashrightarrow c \in \pi$ and $a \dashrightarrow c \in \pi$.

- Process $R$ has two admissible transitions, namely the c-action $R \xrightarrow[0]{\bar{b}^r}{\bar{a}} R_1$ and $R \xrightarrow[0]{\bar{c}^r}{\bar{a}} R_2$. Each interferes with itself but not with the other. Thus, coherence implies that $R_1$ and $R_2$ reconverge. This is indeed the case, since we have $R_1 \xrightarrow[0]{\bar{c}^r}{\bar{a}} 0$ and $R_2 \xrightarrow[0]{\bar{b}^r}{\bar{a}} 0$, with commuting actions. The concurrent contexts are residual since $0 \rightsquigarrow \bar{c} \rightsquigarrow 0$ and $0 \rightsquigarrow \bar{b} \rightsquigarrow 0$. Since all admissible transitions of $R_1$ (and $R_2$) are reflexive and interfere with each other, $R_1$ (and $R_2$) are coherent, too.

Next we show that the parallel composition $Q|R$ is not coherent. We have admissible c-actions

$$Q|R \xrightarrow[c^r:a]{b|\bar{b}} \{b,\bar{b},\bar{a}\} c^r:a|R_1 \text{ and } Q|R \xrightarrow[b^r]{c|\bar{c}} \{c,\bar{c},a,\bar{a}\} b^r|R_2.$$

which are in fact c-enabled. However, the continuation process $c^r:a|R_1 = c^r:a|\bar{a}^r + \bar{c}^r:\bar{a}$ on the left is binary blocked by a race condition. We find

$$c^r:a|R_1 \xrightarrow[0]{c|\bar{c}} \{c,\bar{c},\bar{a},\tau\} 0$$

where the silent $\tau$ enters the blocking set, because $\{a\} \cap \overline{\mathbb{A}}(\bar{a}^r + \bar{c}^r:\bar{a}) \not\subseteq \{c\}$. This is a race computed in rule (Com). Thus, the reduction $c|\bar{c}$ of the original state $Q|R$ is not longer c-enabled in the state $c^r:a|R_1$. This breaks coherence.

Finally, we notice that $Q|R$ is not pivotable. A common policy $\pi$ for $Q|R$ must obviously include the precedences $\bar{a} \dashrightarrow \bar{c} \in \pi$, as well as $a \dashrightarrow c \in \pi$. This is not pivot according to Def. 10.

**On Milner's Confluence Class.** CCS corresponds to the unclocked and (blocking) free processes of CCS$^{sp}$. For these processes, admissible transitions and strongly enabled transitions coincide. The key result of Milner [36] (Chap. 11, Prop. 19) is that confluence is preserved by inaction 0, prefixing $\ell.P$ and confluent composition defined as $P|_L Q = (P|Q)\setminus L$ where $\mathcal{L}(P) \cap \mathcal{L}(Q) = \{\}$ and $\overline{\mathcal{L}(P)} \cap \mathcal{L}(Q) \subseteq L \cup \overline{L}$. We will show how confluence for this fragment of CCS processes follows from our more general results on coherence. From now on, for the rest of this section, we assume that all processes are unclocked, i.e., each prefix $\ell:H.Q$ has $H \cup \{\ell\} \subseteq A \cup \overline{A}$.

Let us call a process $P$ discrete if all prefixes occurring in $P$ are of form $\ell:\{\ell\}.Q$, i.e., they are self-blocking. Under strong enabling, a discrete process behaves like a CCS process with the restriction that each action $\ell$ only synchronises if there is a matching partner $\overline{\ell}$ in a unique other parallel thread. If the matching partner is not unique, then the scheduling blocks. For instance, $\ell:\ell|\overline{\ell}:\overline{\ell}|\overline{\ell}:\overline{\ell}$ blocks because there are two concurrent senders $\overline{\ell}$ matching the receiver $\ell$. Now consider
the fragment CCS<sup>cc</sup> of discrete processes built from inaction 0, self-blocking pre-
fixes ℓ: {ℓ}.Q and confluent composition. Milner's result says that the processes
in CCS<sup>cc</sup> are confluent under admissible scheduling.

To emulate Milner’s result in our setting, we consider the sort L(P) of a
process P as the admissible actions of a discrete policy πP with only reflexive
precedences. In other words, ℓ₁ ---→ ℓ₂ ∈ πP iff ℓ₁ = ℓ₂. It is easy to see that a
discrete process always conforms to πP. Also, discrete policies are always pivot
policies (Def. 10) and dependency-closed for all label sets (Def. 10), as one shows
easily. Thus, discrete processes, which are coherent for discrete policies, fullfill all
conditions of the preservation laws for inaction 0 (Prop. 11), self-blocking action
prefix ℓ: {ℓ}.Q (Prop. 12), parallel composition P | Q (Prop. 6) and restriction
P \ L (Prop. 16). As a consequence and in particular, all processes in CCS<sup>cc</sup> are
coherent under strong enabling by our results.

Our final observation now is that, for Milner’s fragment CCS<sup>cc</sup>, the transi-
tion semantics under admissible and strong enabling, as well as the notions of
confluence and coherence, coincide. Firstly, if P is discrete then in every c-action
ℓ:H[E] executed by a derivative Q of P we must have H = {ℓ}. Thus, the co-
herence Def. 5(1) becomes redundant since it is always satisfied. Further, any
two c-actions ℓ<sub>i</sub>:H<sub>i</sub>[E<sub>i</sub>] of transitions Q <sub>E<sub>1</sub></sub><sup>ℓ<sub>1</sub></sup><sub>H<sub>1</sub></sub> Q<sub>1</sub> and Q <sub>E<sub>2</sub></sub><sup>ℓ<sub>2</sub></sup><sub>H<sub>2</sub></sub> Q<sub>2</sub> for ℓ<sub>1</sub> ≠ ℓ<sub>2</sub>
or Q<sub>1</sub> ≠ Q<sub>2</sub> are trivially interference-free. The confluent composition of Milner
has the further effect that for every c-action ℓ:H[E] we must have ℓ ∉ iA<sup>*</sup>(E).
This is proven by induction on the structure of P ∈ CCS<sup>cc</sup>. Further, the side con-
dition of (Com) becomes trivial, and thus generally τ ∉ H. This is a result of the
side-conditions of the confluent composition. Hence, for CCS<sup>cc</sup>, strong enabling
coincides with plain admissibility CCS. Notice that the class of discrete processes
and the class processes coherent for discrete policies is larger than CCS<sup>CW</sup>. In
particular, we can explain coherence of broadcast actions with repetitive pre-
fixes. Hence, our results are more general even for the restricted class of discrete
behaviours.

*Towards the main proof.* First, we adopt a slightly more general form of inter-
ference, for general c-actions not just for those that are constructively enabled,
as in Def. 4.

**Definition 11.** Two c-actions $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are called interference-free if the following holds for all $i \in \{1,2\}$:

1. If $\alpha_1 \neq \alpha_2$ then $\alpha_i \notin H_{3-i}$.

2. If $\alpha_{3-i} = \tau$ then $H_i \cap (iA^*(E_i) \cup \{\tau\}) = \{\}$.

The extra condition (2) in Def. 11 says that for a c-action not to interfere with
a silent (and thus uncontrollable) action it must be c-enabled. Obviously, Def. 11
is a weakening of Def. 4, i.e. if $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are interference-free
according to Def. 11 they are interference-free according to Def. 4.

**Proposition 7.** If a coherent process *P* offers enabled transitions on a clock *σ*
and another distinct action *α* ≠ *σ* with *P* <sub>*R*₁</sub><sup>*α*</sup> *P*₁ and *P* <sub>*R*₂</sub><sup>*σ*</sup> *P*₂ then *α* ∈ *H*₂
or *σ* ∈ *H*₁. In particular, if *α* = *τ* then *σ* ∈ *H*₁.
**Proof.** Since $R_2 = 0$ by Lem. 1(1) and $iA(0) = \{\}$, we have $\alpha \notin iA(R_2)$ and thus $\alpha$ cannot be an initial action $R_2 \xrightarrow{\alpha} R'_2$, by Lem. 1(2). Now we have $\{\alpha, \sigma\} \cap C \neq \{\}$. But then the coherence Def. 5(2) implies that the c-actions $\alpha: H_1[R_1]$ and $\sigma: H_2[R_2]$ must interfere. Since $\alpha \neq \sigma$ this implies $\alpha \in H_2$ or $\sigma \in H_1$, or $\alpha = \tau$ and $H_2 \cap (i\bar{A}^*(R_2) \cup \{\tau\}) \neq \{\}$. Since $R_2 = 0$ the latter reduces to $\alpha = \tau \in H_2$. The last part of the proposition now follows from the fact that the clock transition is enabled and thus $\tau \notin H_2$.

**Theorem 1.** Every coherent process is determinate under c-enabled reductions, i.e., if $P \Downarrow Q_1$ and $P \Downarrow Q_2$ then $Q_1 \equiv Q_2$.

**Proof.** As in the $\lambda$-calculus, the uniqueness of normal forms follows from local confluence of reduction steps: Every two c-enabled reductions from a coherent process must immediately reconverge. Let $P$ be coherent and $Q$ a derivative with c-enabled reductions $Q \xrightarrow{\tau/R_1} H_1$ and $Q \xrightarrow{\tau/R_2} H_2$. If $Q_1 \equiv Q_2$ we are done immediately. Suppose $Q_1 \not\equiv Q_2$. Then c-enabling implies $\tau \notin H_i$ as well as $H_i \cap i\bar{A}^*(R_i) = \{\}$, which implies $H_i \cap (i\bar{A}^*(R_i) \cup \{\tau\}) = \{\}$. But then the c-actions $\tau: H_1[R_1]$ and $\tau: H_2[R_2]$ are interference-free, whence coherence Def. 5 implies there exist $H'_i$ and processes $R'_i$, $Q'$ such that $Q_1 \xrightarrow{\tau/R'_2} H'_2$ and $Q_2 \xrightarrow{\tau/R'_1} H'_1$ and $R'_1$ and $R'_2$ with $H'_i \subseteq H_i$. Finally, observe that $i\bar{A}^*(R'_i) \subseteq i\bar{A}^*(R_i)$ by Lem. 2 from which we infer $H'_i \cap (i\bar{A}^*(R'_i) \cup \{\tau\}) \subseteq H_i \cap (i\bar{A}^*(R_i) \cup \{\tau\}) = \{\}$. Thus, the re-converging reductions $Q_i \xrightarrow{\tau/R'_{3-i}} H'_{3-i}$ and $Q'$ are again c-enabled. Overall, we have shown that if $Q \xrightarrow{\tau} Q_1$ and $Q \xrightarrow{\tau} Q_2$ are c-enabled reductions such that $Q_1 \not\equiv Q_2$, then there exists $Q'$ with c-enabled reductions $Q_1 \xrightarrow{\tau} Q$ and $Q_2 \xrightarrow{\tau} Q$. This is the local confluence from which uniqueness of normal forms follows in the usual fashion.

**Proposition 1.** Every coherent process $P$ is structurally clock deterministic, i.e., if $P \xrightarrow{\sigma} P_1$ and $P \xrightarrow{\sigma} P_2$ are c-enabled, then $P_1 \equiv P_2$.

**Proof.** Let $P$ be coherent with c-enabled transitions

$$P \xrightarrow{\sigma/R_1} H_1 P_1 \text{ and } P \xrightarrow{\sigma/R_2} H_2 P_2.$$

By way of contradiction suppose $P_1 \not\equiv P_2$. Observe that by Lem. 1(1) we have $R_i \equiv 0$ and thus $i\bar{A}^*(R_i) = \{\}$. Thus, the assumption that the clock transitions are c-enabled is equivalent to assuming $\tau \notin H_i$. The c-actions $\sigma: H_i[R_i]$ are trivially interference-free by Def. 4. Since $P_1 \not\equiv P_2$, coherence Def. 5 gives us a $H'_i$ and processes $R'_i$, $Q'$ such that

$$P_1 \xrightarrow{\sigma/R_2} H'_2 Q' \text{ and } P_2 \xrightarrow{\sigma/R'_1} H'_1 Q'$$

with $H'_i \subseteq H_i$ and $R_1 \rightsquigarrow R'_1$ and $R_2 \rightsquigarrow R'_2$. For clock transitions, these residual transitions must be actual transitions $R_1 \xrightarrow{\sigma} R'_1$ and $R_2 \xrightarrow{\sigma} R'_2$ (Coherence Def. 5). But then we would have $\sigma \in iA(R_i)$ which contradicts the assumption $R_i \equiv 0$. Thus, we must have $P_1 \not\equiv P_2$ as desired.
**Lemma 5.** Let $P_1 \Vdash \pi$ and $P_2 \Vdash \pi$ be coherent for the same pivot policy $\pi$. If $P_1$ and $P_2$ are single-threaded, then every admissible transition of $P_1|P_2$ is c-enabled.

*Proof.* Consider an admissible transition of $P_1|P_2$ where $P_1$ and $P_2$ are single-threaded. Firstly, by Lem. 1, each of the single-threaded processes can only generate c-actions $\ell_i:H_i[R_i]$ where $\tau \notin H_i$ and $R_i = 0$. Such transitions are always c-enabled for trivial reasons. Further, any rendez-vous synchronisation of such an $\ell_1:H_1[R_1]$ and $\ell_2:H_2[R_2]$ generates a c-action $\tau:(H_1 \cup H_2 \cup H') [R_1 | R_2]$ with $R_1|R_2 = 0$. Because of Lem. 3, the set $H' = \text{race}(P_1, P_2)$ must be empty. Thus, the reduction $\ell_1|\ell_2$ is c-enabled, too.

**Proposition 2** Suppose $P$ is coherent and pivotable. If $\sigma \in iA(P)$ then $P$ is in normal form, i.e., there is no reduction $P \xrightarrow{\tau} P'$.

Instead of Prop. 2 we prove the following slightly extended statement of Prop. 8. It that says that a pivotable process cannot offer a clock action and exhibit another clock or a rendez-vous synchronisation at the same time. This means that in this class of processes, clocks and reductions are sequentially scheduled.

**Proposition 8 (Sequential Schedule and Clock Maximal Progress).** Suppose $P$ is coherent and pivotable and $\sigma \in iA(P)$. Then, for all $\ell \in \mathcal{L}$ with $\ell \neq \sigma$ we have $\ell \notin iA(P)$ or $\ell' \notin iA(P)$. In particular, $P$ is in normal form, i.e., there is no reduction $P \xrightarrow{\tau} P'$.

*Proof.* The proof proceeds by contradiction. Let $P \Vdash \pi$ for pivot policy $\pi$. Suppose $\ell \in \mathcal{L}$, $\ell \neq \sigma$ and $P \xrightarrow[0]{\sigma} H_1 P_1$ and $P \xrightarrow[F]{\ell} N P_2$ and $P \xrightarrow[G]{\ell} M P_3$. By Prop. 7 we infer $\sigma \in N$ or $\ell \in H$, i.e., by conformance Def. 7 we have $\pi \Vdash \sigma \dashrightarrow \ell$ or $\pi \Vdash \ell \dashrightarrow \sigma$. Hence, $\pi \nVdash \sigma \diamond \ell$. For the same reason we have $\pi \nVdash \sigma \diamond \ell'$. However, this contradicts the pivot property of $\pi$, which requires $\pi \Vdash \sigma \diamond \ell$ or $\pi \Vdash \sigma \diamond \ell'$. Finally, if $P \xrightarrow{\tau} P'$ then the reduction must arise from a rendez-vous synchronisation inside $P$, i.e., there is $\ell \in \mathcal{R}$ with $\ell \in iA(P)$ and $\ell' \in iA(P)$. But then $\sigma \in iA(P)$ is impossible as we have just seen.

**Theorem 2**

1. (Idling) $0 \Vdash \pi$ for all policies $\pi$.

2. (Rendezvous Prefix) If $Q \Vdash \pi$, then for every $\ell \in \mathcal{R}$ we have $\ell:H.Q \Vdash \pi$ if $\ell \in H \subseteq \{\ell' | \ell' \dashrightarrow \ell \in \pi\}$.

3. (Clock Prefix) If $Q \Vdash \pi$ and clock $\sigma \in \mathcal{C}$, then $\sigma:H.Q \Vdash \pi$ if $H \subseteq \{\beta | \beta \dashrightarrow \sigma \in \pi\}$.

4. (Choice) If $P_1 \Vdash \pi_1$ and $P_2 \Vdash \pi_2$ and for all pairs of initial transitions $P \xrightarrow[\alpha_1]{\alpha_1} H_1 P_1$ and $P \xrightarrow[\alpha_2]{\alpha_2} H_2 P_2$ such that $\alpha_1 \neq \alpha_2$ as well as $\alpha_1 \in H_2$ or $\alpha_2 \in H_1$. Then $P_1 + P_2 \Vdash \pi$ if $\pi_1 \subseteq \pi$ and $\pi_2 \subseteq \pi$.

5. (Parallel) If $Q \Vdash \pi$ and $R \Vdash \pi$ where $\pi \setminus \mathcal{R}$ is a pivot policy, then $(Q|R) \Vdash \pi$.

6. (Hiding) If $Q \Vdash \pi$ and $\sigma \dashrightarrow \ell \notin \pi$ for all $\sigma \in L$ and $\ell \in \pi$, then $Q/L \Vdash \pi$.
7. (Restriction) If $Q \Vdash \pi$ and $\pi$ precedence-closed for $L \cup \bar{L}$, then $(Q \setminus L) \Vdash \pi \setminus L$.

The proof of Thm. 2 will be conducted in the following Secs. B.1–B.4. It proceeds by induction on the structure of derivations in the SOS of CCS<sup>spt</sup>, given in Fig. 2. Here, in preparation, we first show that the indirections of syntactic transformations via the static laws of Fig. 1, built into the SOS by the (Struct) rule, can in fact be eliminated in terms of a finite number of standard SOS rules that do not refer to structural laws.

**Definition 12.** A process *P* is called 0-free if either *P* = 0 or all occurrences of 0 in *P* are guarded by a prefix *ℓ*:H.R.

**Proposition 9.** Every process *P* is structurally congruent to a 0-free process *Q*.

*Proof.* By application of the laws $P \star 0 \equiv P$ and $0 \lozenge L \equiv 0$, where $\star \in \{|, +\}$ and $\lozenge \in \{\setminus, /\}$ we can eliminate every occurrence of 0 in an process *P* that is not of the form $\alpha:H.O$.

**Proposition 10.** If *P* is a 0-free process, and there is a derivation *D* for $P \xrightarrow{\alpha} H * Q$, then all uses of the rule (Struct) in *D* can be eliminated in terms of the following symmetric versions of the rules (Par) and (Sum):

$$ \frac{P \xrightarrow{\alpha} H P'}{P + Q \xrightarrow{\alpha} H P'} \quad (\text{Sum}_1) $$

$$ \frac{Q \xrightarrow{\alpha} H Q'}{P + Q \xrightarrow{\alpha} H Q'} \quad (\text{Sum}_2) $$

$$ \frac{P \xrightarrow{\alpha} H P' \quad \alpha \notin C}{P | Q \xrightarrow{\alpha} H P' | Q} \quad (\text{Par}_1) $$

$$ \frac{Q \xrightarrow{\alpha} H Q' \quad \alpha \notin C}{P | Q \xrightarrow{\alpha} H P | Q'} \quad (\text{Par}_2) $$

More specifically, there is a derivation $D'$ for $P \xrightarrow{\alpha} H Q'$ with $R' \equiv R$ and $Q' \equiv Q$.

*Proof (Proof Sketch).* By induction on the structure of processes one shows that the transitions generated by the SOS with (Struct) can be simulated by the extended SOS without (Struct). The argument is based on the following case analysis:

- If $P = 0$ then no process structurally equivalent to $P$ can generate any transition: If $P \equiv Q$ and $Q \xrightarrow{\alpha} H Q'$ then $P \neq 0$. Hence, the statement of the proposition holds trivially.

- For prefixes we show that if $P \equiv \ell:H.Q$ and $P \xrightarrow{\ell} H' Q'$ then $\ell' = \ell$, $H' = H$, $E' \equiv 0$ and $Q' \equiv Q$.

- For sums we observe that if $P \equiv P_1 + P_2$ and $P \xrightarrow{\ell} H Q$ then there exists $i \in \{1, 2\}$ such that $P_i \xrightarrow{\ell} H Q'$ such that $E' \equiv E$ and $Q' \equiv Q$.
- For all other operators, e.g. $P \equiv P_1 | P_2$, $P \equiv Q / L$, $P \equiv Q \setminus L$, we can easily show that transitions $P \xrightarrow{\alpha} H$ $P'$ can be obtained from transitions of $P_i$ and $Q$.

Note that the restriction in Prop. 10 is necessary. If $P$ is not 0-free, say $P = 0 | Q$, then we can have $0 | Q \xrightarrow{\sigma} Q'$ because of (Struct), because $0 | Q \equiv Q$ and $Q \xrightarrow{\sigma} Q'$, but without (Struct) we could not derive $0 | Q \xrightarrow{\sigma} Q'$.

Because of Prop. 9 we may assume our processes are 0-free. Because of Prop. 10 we may prove the preservation of coherence (for 0-free processes) by induction on the SOS rules without considering (Struct), but including the symmetric rules ($Par_i$) and ($Sum_i$) for $i \in \{1, 2\}$.

## B.1 Stop and Prefixes

**Proposition 11.** *The process 0 is coherent for any policy, i.e., $0 \models \pi$ for all $\pi$.*

*Proof.* The inactive process 0 is locally coherent for trivial reasons, simply because it does not offer any transitions at all. There is no SOS rule applicable to it in the (Struct)-free setting. Note that in the system with (Struct) rule, we would have to argue that no process structurally equivalent to 0 has any transitions.

**Proposition 12.** *Let process $Q$ be coherent for $\pi$. Then, for every action $\ell \in \mathcal{R}$ the prefix expression $\ell:H.Q$ is coherent for $\pi$, if $\ell \in H \subseteq \{\ell' | \ell' \dashv\vdash \ell \in \pi\}$.*

*Proof.* A prefix expression $P = \ell:H.Q$ generates only a single transition by rule (Act), so that the assumption

$$P \xrightarrow{\alpha_1} H_1 Q_1 \text{ and } P \xrightarrow{\alpha_2} H_2 Q_2 \quad (1)$$

implies $\alpha_i = \ell$, $H_i = H$, $E_i \equiv 0$ and $Q_i \equiv Q$. It is easy to see that $\ell:H.Q$ conforms to $\pi$ if $H \subseteq \{\beta | \beta \dashv\vdash \alpha \in \pi\}$. Since $\alpha_i = \ell \in H = H_i$ and $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ nothing needs to be proved. Finally, note that the only immediate derivative of $\alpha:H.Q$ is $Q$ which is coherent for $\pi$ by assumption.

Again, it is important to notice that the SOS with (Struct) would not immediately warrant the conclusion that both derivations (1) are by (Act). This is because these transitions could be the transitions of two syntactically distinct (but structurally congruent) expressions $P_1 \equiv P \equiv P_2$. Instead, we would have to argue that if $P = \ell:H.Q \equiv P'$ and $P' \xrightarrow{\alpha'} H' Q'$ then $\alpha' = \ell$, $H' = H$, $E' \equiv 0$ and $Q' \equiv Q$. That this is the case is a property of our specific system of structural laws and handled by the above Prop. 10. This would obviously be violated, e.g., if we added a structural law like $\ell:H.Q \equiv \alpha':H'.Q'$ where $\alpha' \neq \ell$, $H' \neq H$, $E' \neq 0$ or $Q' \neq Q$.

As Examples 5 and 6 show, a prefix $\ell:H.Q$ for $\ell \in \mathcal{R}$ can very well be coherent even if $\ell \notin H$. Here we note that for clock prefixes, the blocking set is only constrained by the policy.
**Proposition 13.** If $Q$ is coherent for $\pi$ and $\sigma \in C$ is a clock, then the prefix expression $\sigma:H.Q$ is coherent for $\pi$, too, if $H \subseteq \{\beta | \beta \dashv\dashv \sigma \in \pi\}$.

*Proof.* The argument runs exactly as in case of Prop. 12. However, we do not need to require condition $\sigma \in H$ because if $\alpha_i = \sigma$ then $\alpha_1 = \alpha_2$, $Q_1 \equiv Q_2$ and $\{\alpha_1, \alpha_2\} \not\subseteq \mathcal{R}$. So, no reconvergence is required. Again, we observe that the only immediate derivative of $\sigma:H.Q$ is $Q$ which is coherent for $\pi$ by assumption.

## B.2 Summation

**Proposition 14.** Let $P_1 \models \pi_1$ and $P_2 \models \pi_2$ be coherent and for all pairs of initial transitions $P \xrightarrow{\alpha_1}_{F_1} H_1$, $P_1$ and $P \xrightarrow{\alpha_2}_{F_2} H_2$, $P_2$ we have $\alpha_1 \neq \alpha_2$ as well as $\alpha_1 \in H_2$ or $\alpha_2 \in H_1$. Then $P_1 + P_2$ is coherent for $\pi$ if $\pi_1 \subseteq \pi$ and $\pi_2 \subseteq \pi$.

*Proof.* Let $P = Q + R$ be given with $Q$ and $R$ locally coherent for $\pi_1$ and $\pi_2$, respectively and the rest as in the statement of the proposition. Every transition of $P$ is either a transition of $Q$ or of $R$ via rules (Sum$_i$). Conformance to $\pi$ directly follows from the same property of $Q$ or $R$, respectively. The proof of coherence Def. 5 is straightforward, exploiting that two competing but non-interfering transitions must either be both from $Q$ or both from $R$. More precisely, suppose $P \xrightarrow{\alpha_1}_{F_1} H_1$, $P_1$ and $P \xrightarrow{\alpha_2}_{F_2} H_2$, $P_2$ with $\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}$. Also, we assume that $\alpha_1:H_1[F_1]$ and $\alpha_2:H_2[F_2]$ are interference-free. Now if the two transitions of $P$ are by (Sum$_1$) from $Q$ or by (Sum$_2$) from $R$, then $\alpha_1 \in iA(Q)$ and $\alpha_2 \in iA(R)$. But then by assumption, $\alpha_1 \neq \alpha_2$ and $\alpha_1 \in H_2$ or $\alpha_2 \in H_1$, which implies that $\alpha_1:H_1[F_1]$ and $\alpha_2:H_2[E_2]$ are not interference-free. This means, to prove coherence Def. 5(2) we may assume that both transitions of $P$ are either by (Sum$_1$) from $Q$ or both by (Sum$_2$) from $R$. Suppose both reductions of $P = Q + R$ are generated by rule (Sum$_1$), i.e., $Q \xrightarrow{\alpha_1}_{F_1} H_1$, $Q_1$ and $Q \xrightarrow{\alpha_2}_{F_2} H_2$, $Q_2$ where the transitions generated by (Sum$_1$) are $Q + R \xrightarrow{\alpha_1}_{F_1} H_1$, $Q_1$ and $Q + R \xrightarrow{\alpha_2}_{F_2} H_2$, $Q_2$. Under the given assumptions, the reconverging transitions of coherence Def. 5(2) are obtained directly from coherence of $Q$, by induction. The case that both transitions are from $R$ by rule (Sum$_2$) is symmetrical. Finally, the immediate derivatives $P_1$ and $P_2$ of $P_1 + P_2$ are coherent for $\pi$, because they are coherent for $\pi_i$ by assumption and thus also for the common extension $\pi_i \subseteq \pi$.

## B.3 Parallel

**Lemma 6 (Key lemma).** Let $Q \models \pi$ and $R \models \pi$ be such that $\pi \setminus \mathcal{R}$ is a pivot policy. Then $(Q | R) \models \pi$.

*Proof.* Let $P = Q | R$ such that both $Q$ and $R$ are coherent for $\pi$ where $\pi \setminus \mathcal{R}$ is a pivot policy. For conformance consider a transition

$$P \xrightarrow{\ell} H, P'$$
with $\ell \in \mathcal{L}$ and $\ell' \in H$. First suppose $\ell \notin \mathcal{C}$. Then this transition is not a synchronisation but a transition of either one of the sub-processes $Q$ by $(Par_1)$ or $P$ by $(Par_2)$ with the same blocking set $H$. In either case, we thus use coherence $Q \models \pi$ or $R \models \pi$ to conclude $\ell' \dashrightarrow \ell \in \pi$. If $\ell = \sigma$, then the transition in question is a synchronisation of $Q$ and $R$ via rule (Com)

$$Q | R \xrightarrow{\sigma_0} H_2 \cup N_2 \cup H' Q_2 | R_2$$

with $E \equiv 0$, $H = H_2 \cup N_2 \cup H'$ and $P' = Q_2 | R_2$ generated from transitions

$$Q \xrightarrow{\sigma_0} H_2 Q_2 \text{ and } R \xrightarrow{\sigma_0} N_2 R_2.$$

and $H' = race(Q, R)$. By Lem. 3 we have $H' = \{\}$. If we now take an arbitrary $\ell' \in H \cap \mathcal{L}$ then $\ell' \in H_2$ or $\ell' \in N_2$. In these cases, we obtain $\ell' \dashrightarrow \ell \in \pi$ by conformance Def. 7 from $Q \models \pi$ or $R \models \pi$.

In the sequel, we tackle coherence Def. 5. As before, we work in the SOS without (Struct) but with symmetrical rules $(Par_i)$. First we observe that the immediate derivatives of $Q | R$ are always parallel compositions $Q' | R'$ of derivatives of $Q$ and $R$. Thus, we may assume that the immediate derivatives $Q' | R'$ are coherent for $\pi$ because coherence of $P$ and $Q$ is preserved under transitions (i.e., by co-induction). Now suppose

$$P \xrightarrow{\alpha_1} H_1 P_1 \text{ and } P \xrightarrow{\alpha_2} H_2 P_2$$

such that $\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}$. Moreover, the c-actions $\alpha_1:H_1[E_1]$ and $\alpha_2:H_2[E_2]$ are interference-free. We argue reconvergence by case analysis on the rules that generate these transitions. These could be $(Par_1)$, $(Par_2)$ or (Com). First note that by Lem. 3 we can drop the consideration of the synchronisation action $\ell | \bar{\ell}$ for the blocking set in (Com) altogether:

$$\frac{P \xrightarrow{\ell} H_1 P' \quad Q \xrightarrow{\bar{\ell}} H_2 Q' \qquad (\text{Com})}{P | Q \xrightarrow{\ell | \bar{\ell}} H_1 \cup H_2 P' | Q'}$$

We will use the name $(Com_a)$ to refer to the instance of (Com) with $\ell \in \mathcal{R}$ and the name $(Com_\sigma)$ for the instance with $\ell \in \mathcal{C}$ and we proceed by case analysis.

- $(Par_1, Par_2) \diamond (Com_a)$. We start with the case where one of the reductions to $P_i$ is non-synchronising by $(Par_1)$ or $(Par_2)$ and the second reduction to $P_{3-i}$ is a synchronisation obtained by $(Com_a)$. By symmetry, it suffices to consider the case that the non-synchronising transition is by $(Par_1)$ from $Q$, i.e., $\alpha_1 \notin \mathcal{C}$ and $\alpha_2 = \ell | \bar{\ell}$ and

$$Q | R \xrightarrow{\alpha_1} H_1 Q_1 | R \text{ and } Q | R \xrightarrow{\ell | \bar{\ell}} H_2' \cup N_2 Q_2 | R_2$$

with $E_1 = F_1 | R$, $E_2 = F_2 | G_2$, $H_2 = H_2' \cup N_2$, $P_1 = Q_1 | R$ and $P_2 = Q_2 | R_2$, where $\ell \in \mathcal{R}$ is a rendezvous action such that

$$Q \xrightarrow{\alpha_1} H_1 Q_1 \text{ and } Q \xrightarrow{\ell} H_2' Q_2 \text{ and } R \xrightarrow{\bar{\ell}} N_2 R_2.$$
We may safely assume $\alpha_1 \neq \ell | \bar{\ell} = \tau$ or $Q_1 | R \neq Q_2 | R_2$. The third case $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ is excluded since $\alpha_2 = \tau$. Further, suppose the c-actions $\alpha_1:H_1[F_1|R]$ and $\ell | \bar{\ell}:(H'_2 \cup N_2)[F_2|G_2]$ are non-interfering. Observe that $\{\alpha_1, \ell | \bar{\ell}\} \notin \mathcal{R}$ and also $\{\alpha_1, \ell | \bar{\ell}\} \cap C = \{\}$. Thus only a weak environment shift is needed. We wish to exploit coherence of $Q$. The first observation is that since $\alpha_2 = \tau$, the assumptions on non-interference Def. 4(2) implies that $H_1 \cap \overline{\mathbb{A}}^*(F_1|R) = \{\}$. Since $\ell = \bar{\ell} \in \overline{\mathbb{A}}(R) \cap \mathcal{L} \subseteq \overline{\mathbb{A}}^*(F_1|R)$ by Lem. 1 and Lem. 2, this implies that $\ell \notin H_1$ up front. Next, if $\alpha_1 \neq \ell | \bar{\ell}$, non-interference Def. 4(1) means $\alpha_1 \notin H_2 = H'_2 \cup N_2$ and thus $\alpha_1 \notin H'_2$. The same is true if $\alpha_1 = \ell | \bar{\ell} = \tau$, but then by non-interference Def. 4(2) we have the non-interference equation

$$ (H'_2 \cup N_2) \cap (\overline{\mathbb{A}}^*(F_2|G_2) \cup \{\tau\}) = H_2 \cap (\overline{\mathbb{A}}^*(E_2) \cup \{\tau\}) = \{\} $$

from which $\alpha_1 = \tau \notin H'_2$ follows. This settles the first part of the non-interference property Def. 4(1) for the diverging transitions out of $Q$.

For the second part of non-interference, suppose $\alpha_1 = \tau$. Then the non-interference assumption implies that $H'_2 \cap \overline{\mathbb{A}}^*(F_2|G_2) = \{\}$. Now since $\overline{\mathbb{A}}^*(F_2) \subseteq \overline{\mathbb{A}}^*(F_2|G_2)$ we conclude from this that $H'_2 \cap \overline{\mathbb{A}}^*(F_2) = \{\}$. This completes the proof that the c-actions $\alpha_1:H_1[F_1]$ and $\ell:H'_2[F_2]$ must be non-interfering in all cases.

Note that we always have $\alpha_1 \neq \ell$ or $\{\alpha_1, \ell\} \subseteq \mathcal{R}$, and in the latter case also $\alpha_1 \notin H'_2$ and $\ell \notin H_1$ from the above. Hence, we can use coherence Def. 5 of $Q$ and obtain processes $F'_1, F'_2, Q'$ with reconverging transitions

$$ Q_1 \xrightarrow{\ell} F'_2 H''_2 Q' \text{ and } Q_2 \xrightarrow{\alpha_1} F'_1 Q' $$

such that $H''_2 \subseteq H'_2$ and $H'_1 \subseteq H_1$. We now invoke $(\mathrm{Com}_a)$ and $(\mathrm{Par}_1)$ to obtain reconverging transitions

$$ Q_1 | R \xrightarrow{\ell | \bar{\ell}} F'_2 H''_2 \cup N_2 Q' | R_2 \text{ and } Q_2 | R_2 \xrightarrow{\alpha_1} F'_1 Q' | R_2 $$

such that $H'_1 \subseteq H_1$ and $H''_2 \cup N_2 \subseteq H'_2 \cup N_2$.

Regarding the concurrent environments, if $\alpha_1 \in \mathcal{R}$ then the coherence of $Q$ guarantees that $F_1 \xrightarrow{\ell} F'_1$ and $F_2 \xrightarrow{\alpha_1} F'_2$ from which we infer $F_2 | G_2 \xrightarrow{\alpha_1} F'_2 | G_2$ and $F_1 | R \xrightarrow{\ell | \bar{\ell}} F'_1 | R_2$.

If $\alpha_1 = \tau$ the above guarantee from the coherence of $Q$ is weaker: We only have $F_1 \rightsquigarrow F'_1$ and $F_2 \rightsquigarrow F'_2$. In any case we obtain the environment shifts $F_2 | G_2 \rightsquigarrow F'_2 | G_2$ and $F_1 | R \rightsquigarrow F'_1 | R_2$, as required.

– $(\mathrm{Par}_1) \diamond (\mathrm{Par}_2)$: Suppose the two non-interfering transitions of $P = Q | R$ are by $(\mathrm{Par}_1)$ from $Q$ and $(\mathrm{Par}_2)$ from $R$. Thus, we are looking at transitions

$$ Q \xrightarrow{\alpha_1} F_1 Q_1 \text{ and } R \xrightarrow{\alpha_2} F_2 R_2 $$

for $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R} \cup \{\tau\}$ combined via $(\mathrm{Par})$ to generate

$$ Q | R \xrightarrow{\alpha_1} F_1 Q_1 | R \text{ and } Q | R \xrightarrow{\alpha_2} F_2 Q | R_2 $$
with $E_1 = F_1 | R$ and $E_2 = Q | F_2$. Then we can directly construct reconverging transitions, applying (Par) for

$$Q_1 | R \xrightarrow[Q_1 | F_2]{\alpha_2} H_2 Q_1 | R_2 \text{ and } Q | R_2 \xrightarrow[F_1 | R_2]{\alpha_1} H_1 Q_1 | R_2.$$

Obviously, $Q_1 | R_2$ reduces to $Q_1 | R_2$ and by (Par$_1$) and (Par$_2$) we also have the strong environment shifts $F_1 | R \xrightarrow{\alpha_2} F_1 | R_2$ and $Q | F_2 \xrightarrow{\alpha_1} Q_1 | F_2$ which completes the claim for we have, in particular, $F_1 | R \xrightarrow{\alpha_2} F_1 | R_2$ and $Q | F_2 \xrightarrow{\alpha_1} Q_1 | F_2$. Notice that in this case we do not need to assume that $Q$ or $R$ are coherent, i.e., the assumption that the c-actions $\alpha_i:H_i[E_i]$ are interference-free.

– (Par$_i$) ◦ (Par$_i$) for $i \in \{1, 2\}$: Suppose both non-interfering and diverging reductions are by (Par$_1$) from $Q$ (or symmetrically, both by (Par$_2$) from $R$). Then,

$$Q | R \xrightarrow[F_1 | R]{\alpha_1} H_1 Q_1 | R \text{ and } Q | R \xrightarrow[F_2 | R]{\alpha_2} H_2 Q_2 | R$$

with $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R} \cup \{\tau\}$ and $P_i = Q_i | R, E_i = F_i | R$, where

$$Q \xrightarrow[F_1]{\alpha_1} H_1 Q_1 \text{ and } Q \xrightarrow[F_2]{\alpha_2} H_2 Q_2$$

with $\alpha_1 \neq \alpha_2$ or $Q_1 | R \neq Q_2 | R$ or $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_i \notin H_{3-i}$. This, in particular, implies $Q_1 \neq Q_2$. Further, assume non-interference of $\alpha_i:H_i[F_i|R]$. We obtain non-interference of $\alpha_i:H_i[F_i]$ by Prop. 4. We can therefore apply coherence Def. 5 of $Q$ and obtain processes $F'_1, F'_2$ and $Q'$ with reconverging transitions

$$Q_1 \xrightarrow[F'_2]{\alpha_2} H'_2 Q' \text{ and } Q_2 \xrightarrow[F'_1]{\alpha_1} H'_1 Q'$$

with $H'_i \subseteq H_i$ and such that

$$F_1 \xrightarrow{\alpha_2} F'_1 \text{ and } F_2 \xrightarrow{\alpha_1} F'_2 \qquad (2)$$

and if $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_1 \neq \alpha_2$ or $Q_1 \neq Q_2$, more strongly

$$F_1 \xrightarrow{\alpha_2} F'_1 \text{ and } F_2 \xrightarrow{\alpha_1} F'_2. \qquad (3)$$

Reapplying (Par$_1$) we construct the transitions

$$Q_1 | R \xrightarrow[F'_2]{\alpha_2} H'_2 Q' | R \text{ and } Q_2 | R \xrightarrow[F'_1]{\alpha_1} H'_1 Q' | R.$$

By (Par$_1$) and (Par$_2$) we also obtain transitions $F_1 | R \xrightarrow{\alpha_2} F'_1 | R$ and $F_2 | R \xrightarrow{\alpha_1} F'_2 | R$ from (2) or, more strongly, $F_1 | R \xrightarrow{\alpha_2} F'_1 | R$ and $F_2 | R \xrightarrow{\alpha_1} F'_2 | R$ from (3) if $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_1 \neq \alpha_2$ or $Q_1 | R \neq Q_2 | R$.
– $(Com_a) \diamond (Com_a)$: This is the most interesting case in which we are going to exploit the assumption that $Q$ and $R$ are coherent for the same pivot policy $\pi$. Without loss of generality we assume $P = Q | R$ and both the reductions

$$Q | R \xrightarrow{\alpha_i \atop E_i} H_i \cup N_i, Q_i | R_i$$

with $P_i = Q_i | R_i$ are $\tau$-actions generated by the communication rule $(Com)$, i.e. $\alpha_1 = \ell_1 | \bar{\ell}_1 = \tau = \ell_2 | \bar{\ell}_2 = \alpha_2$ for actions $\ell_i \in \mathcal{R}$. Since $\alpha_1 = \alpha_2$ and $\{\alpha_1, \alpha_2\} = \{\tau\} \notin \mathcal{R}$ we only need to prove confluence the case that $P_1 \not\equiv P_2$, i.e., $Q_1 \not\equiv Q_2$ or $R_1 \not\equiv R_2$. Moreover, we only need a weak environment shift, because $\{\alpha_1, \alpha_2\} = \{\tau\} \notin \mathcal{R}$ and $\{\alpha_1, \alpha_2\} \cap \mathcal{C} = \{\}$. Also, non-interference Def. 4(2) means that $(H_i \cup N_i) \cap (\overline{\mathbb{A}^*}(E_i) \cup \{\tau\}) = \{\}$, i.e.,

$$H_i \cap (\overline{\mathbb{A}^*}(E_i) \cup \{\tau\}) = \{\} \text{ and } N_i \cap (\overline{\mathbb{A}^*}(E_i) \cup \{\tau\}) = \{\}. \quad (4)$$

Thus, we are looking at transitions

$$Q \xrightarrow{\ell_i \atop F_i} H_i, Q_i \text{ and } R \xrightarrow{\bar{\ell}_i \atop G_i} N_i, R_i.$$

We claim that the two c-actions $\ell_i:H_i[F_i]$ of $Q$, and likewise the two c-actions $\bar{\ell}_i:N_i[G_i]$ of $R$, are interference-free. Note that since $\ell_i \neq \tau$, we only need to consider the first part of Def. 4(1). We first show that at least one of these pairs of c-actions must be interference free, because of coherence and conformance to $\pi$ where $\pi \setminus \mathcal{R}$ is a pivot policy. It will then transpire that the other must be interference-free, too, because of the assumption (4). Obviously, if $\ell_1 = \ell_2$ then both $\ell_i:H_i[F_i]$ of $Q$ and $\bar{\ell}_i:N_i[G_i]$ are interference-free for trivial reasons. We distinguish two cases depending on whether $\ell_1$ and $\ell_2$ are identical or not. So, suppose $\ell_1 \neq \ell_2$. Both $Q$ and $R$ are coherent for the same policy $\pi$ and $\pi \setminus \mathcal{R}$ is a pivot policy. Thus, $\ell_1 \diamond \ell_2 \in \pi$ or $\bar{\ell}_1 \diamond \bar{\ell}_2 \in \pi$, by Def. 10. Hence, $\ell_i \notin H_{3-i}$ or $\bar{\ell}_i \notin N_{3-i}$ by conformance Def. 7, which means that at least one of the pairs of c-actions $\ell_i:H_i[F_i]$ of $Q$ or the two c-actions $\bar{\ell}_i:N_i[G_i]$ must be interference-free by policy. Now we argue that if $\ell_1 \neq \ell_2$ and one of the pairs $\ell_i:H_i[F_i]$ or $\bar{\ell}_i:N_i[G_i]$ is interference-free the other must be, too, and so we can close the diamond for both $Q$ and $R$. By symmetry, it suffices to run the argument in case that the c-actions $\ell_i:H_i[F_i]$ of $Q$ are non-interfering. Then, we have $\{\ell_1, \ell_2\} \subseteq \mathcal{R}$ and $\ell_i \notin H_{3-i}$. Hence, we invoke coherence Def. 5 of $Q$ obtaining processes $F'_1$ and $F'_2$ with transitions (strong environment shift) $F_1 \xrightarrow{\ell_2} F'_1$ and $F_2 \xrightarrow{\ell_1} F'_2$ and a process $Q'$ with transitions

$$Q_1 \xrightarrow{\ell_2 \atop F'_2} H'_2, Q' \text{ and } Q_2 \xrightarrow{\ell_1 \atop F'_1} H'_1, Q'$$

such that $H'_i \subseteq H_i$. This means $\ell_i \in i\mathbb{A}(F_{3-i}) \subseteq i\mathbb{A}(F_{3-i} | G_{3-i}) = i\mathbb{A}(E_{3-i}) \subseteq i\mathbb{A}^*(E_{3-i})$ and therefore $\bar{\ell}_i \notin N_{3-i}$ because of (4). Thus, as claimed, the c-actions $\bar{\ell}_i:N_i[G_i]$ are interference-free, too. Again $\{\bar{\ell}_1, \bar{\ell}_2\} \subseteq \mathcal{R}$ and $\bar{\ell}_i \notin N_{3-i}$ entitles us to exploit coherence Def. 5 for $R$ from which we obtain
processes $G'_1$ and $G'_2$ with transitions (again, a strong environment shift)
$G_1 \xrightarrow{\bar{\ell}_2} G'_1$ as well as $G_2 \xrightarrow{\bar{\ell}_1} G'_2$ as well as a process $R'$ with

$$
R_1 \xrightarrow{\bar{\ell}_2 / G'_2} N'_2 R' \text{ and } R_2 \xrightarrow{\bar{\ell}_1 / G'_1} N'_1 R'.
$$

with $N'_i \subseteq N_i$. Finally, we invoke (Com) to obtain the re-converging reduc-
tions

$$
Q_1 | R_1 \frac{\ell_2 | \bar{\ell}_2}{F'_2 | G'_2} \rightarrow H'_2 \cup N'_2 Q' | R' \text{ and } Q_2 | R_2 \frac{\ell_1 | \bar{\ell}_1}{F'_1 | G'_1} \rightarrow H'_1 \cup N'_1 Q' | R'
$$

with $H'_i \cup N'_i \subseteq H_i \cup N_i$, and also

$$
F_i | G_i \xrightarrow{\ell_{3-i} | \overline{\ell_{3-i}}} F'_i | G'_i
$$

as required, since this implies the weaker form $F_i | G_i \xrightarrow{\tau} F'_i | G'_i$ of environ-
ment shift.

It remains to consider the case that $\ell_1 = \ell = \ell_2$. By assumption $P_1 \neq P_2$ and so we must have $Q_1 \neq Q_2$ or $R_1 \neq R_2$. Suppose $Q_1 \neq Q_2$. If $R_1 \neq R_2$ we apply a symmetric argument with the role of $\ell_i$ and $\bar{\ell}_i$ interchanged. As observed above, the c-actions $\ell_i:H_i[F_i]$ are trivially interference-free ac- cording to Def. 4, because $\ell_1 = \ell_2$ and $\ell_i \neq \tau$. Then, by coherence Def. 5 applied to $Q$ we conclude that there are processes $F'_1$ and $F'_2$ with transi- tions $F_1 \xrightarrow{\ell} F'_1$ and $F_2 \xrightarrow{\ell} F'_2$ and a process $Q'$ with transitions (the strong environment shift arises here because we have $\ell \in \mathcal{R}$ and $Q_1 \neq Q_2$)

$$
Q_1 \xrightarrow{\ell / F'_2} H'_2 Q' \text{ and } Q_2 \xrightarrow{\ell / F'_1} H'_1 Q'.
$$

such that $H'_i \subseteq H_i$. This means that $\ell \in i\mathbb{A}(F_{3-i}) \subseteq i\mathbb{A}(E_{3-i})$ and so $\bar{\ell} \notin N_{3-i}$ because of $N_{3-i} \cap i\mathbb{A}^*(E_{3-i}) = \{\}$ as per (4). If $R_1 = R_2$ then for each $i \in \{1,2\}$, by coherence Def. 5 (as $\bar{\ell} \notin N_{3-i} \cup C$) there is a transition

$$
R_i \xrightarrow{\bar{\ell} / G'_{3-i}} N'_{3-i} R'
$$

with $N'_i \subseteq N_i$ and $G_i \equiv G'_i$ or $G_i \xrightarrow{\bar{\ell}} G'_i$. Using these transitions we now
recombine

$$
Q_i | R_i \xrightarrow{\ell / \bar{\ell} / G'_{3-i}} H'_{3-i} \cup N'_{3-i} Q' | R'
$$

with $H'_i \cup N'_i \subseteq H_i \cup N_i$. Note that if $G_i \equiv G'_i$ then

$$
F_i | G_i \xrightarrow{\ell} F'_i | G_i = F'_i | G'_i
$$

or if $G_i \xrightarrow{\bar{\ell}} G'_i$ then

$$
F_i | G_i \xrightarrow{\ell | \bar{\ell}} F'_i | G'_i.
$$

This means that, in all cases, $F_i | G_i \xrightarrow{\ell | \bar{\ell}} F'_i | G'_i$ as desired. If $R_1 \neq R_2$ we
can apply coherence Def 5 to $R$ in the same way and close the diamond with
processes $G'_1$ and $G'_2$ and transitions (again, the strong environment shift arises here because we have $\bar{l} \in \mathcal{R}$ and $R_1 \not\equiv R_2$) $G_1 \xrightarrow{\bar{l}} G'_1$ and $G_2 \xrightarrow{\bar{l}} G'_2$ as well as a process $R'$ with

$$R_1 \xrightarrow{\bar{l}} G'_2 R' \text{ and } R_2 \xrightarrow{\bar{l}} G'_1 R'$$

with $N'_i \subseteq N_i$. Finally, we invoke (Com) to obtain the re-converging reductions

$$Q_1 | R_1 \xrightarrow{\ell | \bar{l}} F'_2 \cup N'_2 Q' | R' \text{ and } Q_2 | R_2 \xrightarrow{\ell | \bar{l}} F'_1 \cup N'_1 Q' | R'$$

with $H'_i \cup N'_i \subseteq H_i \cup N_i$, and also $F_i | G_i \xrightarrow{\ell | \bar{l}} F'_i | G'_i$ which also implies $F_i | G_i \xrightarrow{\ell | \bar{l}} F'_i | G'_i$ as required.

- $(Com_a) \diamond (Com_\sigma)$ and, by symmetry, the induction case $(Com_\sigma) \diamond (Com_a)$:
  We assume $P = Q | R$ and the non-interfering, diverging reductions

$$Q | R \xrightarrow{\ell | \bar{l}} H_1 \cup N_1 \cup H'_1 Q_1 | R_1 \text{ and } Q | R \xrightarrow{\sigma | 0} H_2 \cup N_2 \cup H'_2 Q_2 | R_2$$

for $\ell \in \mathcal{L}$, $\sigma \in \mathcal{C}$, with $P_i = Q_i | R_i$ and $E_i = F_i | G_i$ are generated by instances $(Com_a)$ and $(Com_\sigma)$ of the communication rules, respectively. These transitions arise from

$$Q \xrightarrow{\ell} H_1 Q_1 \text{ and } R \xrightarrow{\bar{l}} N_1 R_1 \text{ and } Q \xrightarrow{\sigma} H_2 Q_2 \text{ and } R \xrightarrow{\sigma} N_2 R_2.$$

We assume that the c-actions $(\ell | \bar{l}): (H_1 \cup N_1 \cup H'_1)[E_1]$ and $\sigma: (H_2 \cup N_2 \cup H'_2)[0]$ are non-interfering. Note that $\ell \neq \sigma$ and $\bar{l} \neq \sigma$. First, observe that by Lem. 3, $H'_1 = \{\} = H'_2$. Also, $\ell | \bar{l} = \tau \neq \sigma$ and so the non-interference assumption means that $\sigma \notin H_1 \cup N_1 \cup H'_1$ as well as $\tau \notin H_2 \cup N_2 \cup H'_2$. The other part of the non-interference, from Def. 4(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. 4. But then, since $\{\ell, \sigma\} \cap \mathcal{C} \neq \{\}$, coherence Def. 5 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{l} \in N_2$ in the same fashion. Now we invoke the fact that $\tau \notin H'_2$, i.e. $H_2 \cap i\bar{A}(R) \subseteq \{\sigma\}$ and $N_2 \cap i\bar{A}(Q) \subseteq \{\sigma\}$. But $\bar{l} \in iA(R)$ and $\ell \in iA(Q)$, whence we must have $\ell \notin H_2$ and $\bar{l} \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{\alpha_1} H_1 Q_1 | R \text{ and } Q | R \xrightarrow{\sigma} 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{\alpha_1}{F_1} Q_1 \text{ and } Q \xrightarrow{\sigma}{0} H_2 Q_2 \text{ and } R \xrightarrow{\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 H'_2)[0]$ are interference-free. First, Def. 4(1) implies $\alpha_1 \notin H_2 \cup N_2 \cup H'_2$ and $\sigma \notin H_1$. Further, if $\alpha_1 = \tau$ then $(H_2 \cup N_2 \cup H'_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. 5 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{\sigma_1}{H_1 \cup N_1 \cup B'_1} Q_1 | R_1 \text{ and } Q | R \xrightarrow{\sigma_2}{H_2 \cup N_2 \cup H'_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}{H_1} Q_1$ and $Q \xrightarrow{\sigma}{H_2} Q_2$ and the likewise the transitions $R \xrightarrow{\sigma}{N_1} R_1$ and $R \xrightarrow{\sigma}{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.

## B.4 Hiding

**Proposition 15.** If $Q$ is coherent for $\pi$ and $\sigma \dashv\vdash \ell \notin \pi$ for all $\sigma \in L$ and $\ell \in \pi$, then $Q/L$ is coherent for $\pi/L$.

*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{\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{\frac{\alpha_1}{\sigma}}_{E_1} H_1 P_1 \text{ and } P \xrightarrow{\frac{\alpha_2}{\sigma}}_{E_2} H_2 P_2$$

arise by (Hide) from transitions

$$Q \xrightarrow{\alpha_1}{F_1} N_1 Q_1 \text{ and } Q \xrightarrow{\alpha_2}{F_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. 5 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 1). Thus, the actions $\alpha_i$ cannot both be the clock $\sigma$ that is hidden. The case $\alpha_i = \sigma$ and $\alpha_{3-i} \in \text{Act} - \{\sigma\}$, for some fixed $i \in \{1, 2\}$ can also be excluded as follows: By Prop. 7 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 \text{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{\mathbf{A}}^*(F_{3-i}/\sigma) = H_{3-i} \cap \overline{\mathbf{A}}^*(E_{3-i}) = \{\}.$$

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

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

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

$$P_1 \xrightarrow{\alpha_2/\sigma} F'_2 H''_2 Q'/\sigma \text{ and } P_2 \xrightarrow{\alpha_1/\sigma} F'_1 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 \rightsquigarrow F'_1/\sigma \text{ and } F_2/\sigma \rightsquigarrow 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 C = \{\alpha_1, \alpha_2\} \cap C \neq \{\}$ we obtain the stronger context shifts $F_1 \rightsquigarrow F'_1$ and $F_2 \rightsquigarrow F'_2$ from which we infer

$$F_1/\sigma \rightsquigarrow F'_1/\sigma \text{ and } F_2/\sigma \rightsquigarrow F'_2/\sigma.$$

This completes the proof.
## B.5 Restriction

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

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{a \atop (1 | b.\bar{s}) \setminus s} \{ (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.

**Proposition 16.** 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{\alpha_E} H R \quad \alpha \notin \{a, \bar{a}\} \quad H' = H - \{a, \bar{a}\}}{Q \setminus a \xrightarrow{\alpha} H' R \setminus a} \quad (Restr)$$

Consider a transition

$$Q \setminus a \xrightarrow{\ell \atop E \setminus a} H' Q' \setminus a \text{ derived from } Q \xrightarrow{\ell} H 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. 7 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{\alpha_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{\alpha_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 \dashrightarrow \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. 5 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. 4(1) to show that the c-actions $\alpha_i:N_i[F_i]$ are interference-free. For the second part Def. 4(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\bar{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\bar{A}^*(F_i \setminus a) = \{\}. $$

Since $\{a, \bar{a}\} \cap N_{3-i} = \{\}$ we have $N_i \cap i\bar{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\bar{A}^*(F_i) = \{\}$ observing that $\tau \notin H_i = N_i$. By contraposition, suppose $\beta \in N_i \cap i\bar{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\bar{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\bar{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} F'_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} E'_2 H''_2 Q' \setminus a \text{ and } P_2 \xrightarrow{\alpha_1} E'_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 $$

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 $\{\alpha_1, \alpha_2\} \subseteq \mathcal{R}$ and $\alpha_1 \neq \alpha_2$ or $P_1 \neq P_2$ or $\{\alpha_1, \alpha_2\} \cap \mathcal{C} \neq \{\}$ we can rely on the stronger 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$. This completes the proof.