Process algebra with strategic interleaving

TL;DR

This paper extends process algebra ACP to incorporate interleaving strategies, such as process-scheduling policies, enabling more accurate modeling of systems with both arbitrary and strategy-based parallel process interleaving.

Contribution

It introduces a new extension of ACP that models interleaving strategies, with proven properties like elimination, conservativity, and unique expansion.

Findings

Extended ACP with interleaving strategies

Proved elimination and conservative extension properties

Supports modeling of hardware/software system behaviors

Abstract

In process algebras such as ACP (Algebra of Communicating Processes), parallel processes are considered to be interleaved in an arbitrary way. In the case of multi-threading as found in contemporary programming languages, parallel processes are actually interleaved according to some interleaving strategy. An interleaving strategy is what is called a process-scheduling policy in the field of operating systems. In many systems, for instance hardware/software systems, we have to do with both parallel processes that may best be considered to be interleaved in an arbitrary way and parallel processes that may best be considered to be interleaved according to some interleaving strategy. Therefore, we extend ACP in this paper with the latter form of interleaving. The established properties of the extension concerned include an elimination property, a conservative extension property, and a unique expansion property.

Tables

Table 1. Table 1: Axioms of ACP ACP \mathrm{ACP}

Table 2. Table 2: Axioms for guarded recursion

Table 3. Table 3: Axioms for strategic interleaving

Table 4. Table 4: Alternative axioms for SI2

Equations

$$\begin{array}[]{@{}l@{}}\sigma_{n}({\langle\,\rangle},s)=1\;,\\ \sigma_{n}(h\mathbin{\raisebox{1.72218pt}{$\scriptstyle\curvearrowright$}}\left(j,n\right),s)=(j+1)\bmod n\;,\end{array}$$

$$\begin{array}[]{@{}l@{}}\vartheta_{n}(h,s,i,a)=s\;.\end{array}$$

$$\begin{array}[]{@{}l@{}}\begin{array}[t]{@{}l@{}}\theta(X)=\underline{X}\;,\\ \theta(a)=2\;,\\ \theta(\delta)=2\;,\\ \theta(\mathsf{cr}(d))=\theta(\phi(d))^{2}+1\;,\\ \theta(t_{1}\mathbin{+}t_{2})=\theta(t_{1})+\theta(t_{2})\;,\\ \theta(t_{1}\cdot t_{2})=\theta(t_{1})^{2}\cdot\theta(t_{2})\;,\end{array}\qquad\begin{array}[t]{@{}l@{}}\theta(t_{1}\mathbin{\parallel}t_{2})=3\cdot(\theta(t_{1})\cdot\theta(t_{2}))^{2}+1\;,\\ \theta(t_{1}\mathbin{\lfloor\lfloor}t_{2})=(\theta(t_{1})\cdot\theta(t_{2}))^{2}\;,\\ \theta(t_{1}\mathbin{\mid}t_{2})=(\theta(t_{1})\cdot\theta(t_{2}))^{2}\;,\\ \theta({\partial_{H}}(t))=2^{\theta(t)}\;,\\ \theta(\mathop{\parallel^{n}_{h,s}}(t_{1},\ldots,t_{n})=(\theta(t_{1})\cdot{}\ldots{}\cdot\theta(t_{n}))^{2}+1\;,\\ \theta(\mathop{{\rfloor\lfloor}^{n,i}_{h,s}}(t_{1},\ldots,t_{n}))=(\theta(t_{1})\cdot{}\ldots{}\cdot\theta(t_{n}))^{2}\;,\end{array}\vspace*{1ex}\\ \hfill\begin{array}[t]{@{}l@{}}\theta(\langle X|E\rangle)=\left\{\begin{array}[]{l@{\;\;}l}2&\mathrm{if}\;E\mathrm{\;is\;a\;guarded\;recursive\;specification\;over\;}\mathrm{ACP}\\ 3&\mathrm{otherwise},\end{array}\right.\end{array}\hfill\end{array}$$

$$\begin{array}[]{@{}l@{}}\mathop{\parallel^{n}_{h,s}}^{\mathcal{B}}(p_{1},\ldots,p_{n})={\mathit{NF}(\mathop{\parallel^{n}_{h,s}}(\underline{p_{1}},\ldots,\underline{p_{n}}))}^{\mathcal{A}}\;,\\ \mathop{{\rfloor\lfloor}^{n,i}_{h,s}}^{\mathcal{B}}(p_{1},\ldots,p_{n})={\mathit{NF}(\mathop{{\rfloor\lfloor}^{n,i}_{h,s}}(\underline{p_{1}},\ldots,\underline{p_{n}}))}^{\mathcal{A}}\;,\end{array}$$

Full text

1998 ACM Computing Classification: D.1.3, D.4.1, F.1.2

Note: In the published version of “Process algebra with strategic interleaving” (Theory of Computing Systems 63(3), 488–505 (2019)) the proof outline of Theorem 3.1 appears to be inadequate. In particular, a head normal form result is used that is too weak. This revision of the published version has been made to rectify this.

1 Introduction

In algebraic theories of processes, such as $\mathrm{ACP}$ [5, 7], CCS [18, 22] and CSP [12, 19], processes are discrete behaviours that proceed by doing steps in a sequential fashion. The parallel composition of two processes is usually considered to incorporate all conceivable interleavings of their steps. In each interleaving, the steps of both processes occur in some order where each time one step is taken from either of the processes. According to many, this interpretation of parallel composition, called arbitrary interleaving, is a plausible, general, if not idealized interpretation. Underlying the usual justification of this claim is the assumption that at most one step is done at each point in time. However, others contend that interpretations in which this simplifying assumption is fulfilled are not faithful. Be that as it may, arbitrary interleaving turns out to be appropriate for many applications and to facilitate formal algebraic reasoning.

Multi-threading as found in programming languages such as Java [16] and C# [17], gives rise to parallel composition of processes. In the case of multi-threading, however, the steps of the processes concerned are interleaved according to a process-scheduling policy. We use the term strategic interleaving for this more constrained form of interleaving; and we further use the term interleaving strategy instead of process-scheduling policy. Arbitrary interleaving and strategic interleaving are quite different. The following points illustrate this: (a) whether the interleaving of certain processes leads to inactiveness depends on the interleaving strategy used; (b) sometimes inactiveness occurs with a particular interleaving strategy whereas arbitrary interleaving would not lead to inactiveness and vice versa.

In previous work, we studied strategic interleaving in the setting of thread algebra, which is built on a specialized algebraic theory of processes devoted to the behaviours produced by instruction sequences under execution (see e.g. [8, 9, 10]). We have, for instance, given demonstrations of points (a) and (b) above in this setting. Nowadays, multi-threading is often used in the implementation of systems. Because of this, in many systems, for instance hardware/software systems, we have to do with parallel processes that may best be considered to be interleaved in an arbitrary way as well as parallel processes that may best be considered to be interleaved according to some interleaving strategy. This is what motivated us to do the work presented in this paper, namely extending $\mathrm{ACP}$ such that it supports both arbitrary interleaving and strategic interleaving.

To our knowledge, there exists no work on strategic interleaving in the setting of a general algebraic theory of processes like ACP, CCS and CSP. In the work presented in this paper, we consider strategic interleaving where process creation is taken into account. The approach to process creation followed in this paper originates from the one first followed in [6] to extend $\mathrm{ACP}$ with process creation and later followed in [2, 11, 3] to extend different timed versions of $\mathrm{ACP}$ with process creation. The only other approach that we know of is the approach, based on [1], that has for instance been followed in [4, 14]. However, with that approach, it is unlikely that data about the creation of processes can be made available for the decision making concerning the strategic interleaving of processes.

The extension of $\mathrm{ACP}$ presented in this paper covers a generic interleaving strategy that can be instantiated with different specific interleaving strategies. We found two plausible ways to deal with inactiveness of a process whose steps are being interleaved with steps of other processes in the case of strategic interleaving. This gives rise to two plausible extensions of $\mathrm{ACP}$. We will treat only one of them in detail.

The rest of this paper is organized as follows. In Section 2, we review $\mathrm{ACP}$ (Section 2.1) and guarded recursion in the setting of $\mathrm{ACP}$ (Section 2.2). In Section 3, we extend $\mathrm{ACP}$ with strategic interleaving (Section 3.1) and establish some important properties of the extension (Section 3.2). In Section 4, we make some concluding remarks.

2 ACP with Guarded Recursion

In this section, we give a survey of $\mathrm{ACP}$ (Algebra of Communicating Processes) and guarded recursion in the setting of $\mathrm{ACP}$. For a comprehensive overview, the reader is referred to [5, 13].

2.1 $\mathrm{ACP}$

In $\mathrm{ACP}$, it is assumed that a fixed but arbitrary set $\mathsf{A}$ of actions, with $\delta\notin\mathsf{A}$, has been given. We write $\mathsf{A}_{\delta}$ for $\mathsf{A}\cup\left\{\delta\right\}$. It is further assumed that a fixed but arbitrary commutative and associative communication function $\gamma\mathbin{:}\mathsf{A}_{\delta}\times\mathsf{A}_{\delta}\to\mathsf{A}_{\delta}$, with $\gamma(\delta,a)=\delta$ for all $a\in\mathsf{A}_{\delta}$, has been given. The function $\gamma$ is regarded to give the result of synchronously performing any two actions for which this is possible, and to give $\delta$ otherwise.

The signature of $\mathrm{ACP}$ consists of the following constants and operators:

• •

for each $a\in\mathsf{A}$, the action constant $a$ ;

• •

the inaction constant $\delta$ ;

• •

the binary alternative composition operator ${\_\hskip 1.00006pt}\mathbin{+}{\_\hskip 1.00006pt}$ ;

• •

the binary sequential composition operator ${\_\hskip 1.00006pt}\cdot{\_\hskip 1.00006pt}$ ;

• •

the binary parallel composition operator ${\_\hskip 1.00006pt}\mathbin{\parallel}{\_\hskip 1.00006pt}$ ;

• •

the binary left merge operator ${\_\hskip 1.00006pt}\mathbin{\lfloor\lfloor}{\_\hskip 1.00006pt}$ ;

• •

the binary communication merge operator ${\_\hskip 1.00006pt}\mathbin{\mid}{\_\hskip 1.00006pt}$ ;

• •

for each $H\subseteq\mathsf{A}$, the unary encapsulation operator ${\partial_{H}}$ .

We assume that there are infinitely many variables, including $x,y,z$. Terms are built as usual. We use infix notation for the binary operators. The precedence conventions used with respect to the operators of $\mathrm{ACP}$ are as follows: $\mathbin{+}$ binds weaker than all others, $\cdot$ binds stronger than all others, and the remaining operators bind equally strong.

The constants and operators of $\mathrm{ACP}$ can be explained as follows:

• •

the constant $a$ denotes the process that is only capable of first performing action $a$ and next terminating successfully;

• •

the constant $\delta$ denotes the process that is not capable of doing anything;

• •

a closed term of the form $t\mathbin{+}t^{\prime}$ denotes the process that behaves either as the process denoted by $t$ or as the process denoted by $t^{\prime}$, but not both;

• •

a closed term of the form $t\cdot t^{\prime}$ denotes the process that first behaves as the process denoted by $t$ and on successful termination of that process it next behaves as the process denoted by $t^{\prime}$;

• •

a closed term of the form $t\mathbin{\parallel}t^{\prime}$ denotes the process that behaves as the process that proceeds with the processes denoted by $t$ and $t^{\prime}$ in parallel;

• •

a closed term of the form $t\mathbin{\lfloor\lfloor}t^{\prime}$ denotes the process that behaves the same as the process denoted by $t\mathbin{\parallel}t^{\prime}$, except that it starts with performing an action of the process denoted by $t$;

• •

a closed term of the form $t\mathbin{\mid}t^{\prime}$ denotes the process that behaves the same as the process denoted by $t\mathbin{\parallel}t^{\prime}$, except that it starts with performing an action of the process denoted by $t$ and an action of the process denoted by $t^{\prime}$ synchronously;

• •

a closed term of the form ${\partial_{H}}(t)$ denotes the process that behaves the same as the process denoted by $t$, except that actions from $H$ are blocked.

The operators $\mathbin{\lfloor\lfloor}$ and $\mathbin{\mid}$ are of an auxiliary nature. They are needed to axiomatize $\mathrm{ACP}$.

The axioms of $\mathrm{ACP}$ are the equations given in Table 1.

In these equations, $a$, $b$ and $c$ stand for arbitrary constants of $\mathrm{ACP}$, and $H$ stands for an arbitrary subset of $\mathsf{A}$. Moreover, $\gamma(a,b)$ stands for the action constant for the action $\gamma(a,b)$. In D1 and D2, side conditions restrict what $a$ and $H$ stand for.

In other presentations of $\mathrm{ACP}$, $\gamma(a,b)$ is regularly replaced by $a\mathbin{\mid}b$ in CM5–CM7. By CM12, which is more often called CF, these replacements give rise to an equivalent axiomatization. In other presentations of $\mathrm{ACP}$, CM10 and CM11 are usually absent. These equations are not derivable from the other axioms, but all there closed substitution instances are derivable from the other axioms. Moreover, CM10 and CM11 hold in virtually all models of ACP that have been devised.

In the sequel, we will use the sum notation $\sum_{i<n}t_{i}$. For each $i\in\mathbb{N}$, let $t_{i}$ be a term of $\mathrm{ACP}$ or an extension of $\mathrm{ACP}$. Then $\sum_{i<0}t_{i}=\delta$ and, for each $n\in\mathbb{N}_{1}$,111We write $\mathbb{N}_{1}$ for the set $\left\{n\in\mathbb{N}\mathrel{\mid}n\geq 1\right\}$ of positive natural numbers. the term $\sum_{i<n}t_{i}$ is defined by induction on $n$ as follows: $\sum_{i<1}t_{i}=t_{0}$ and $\sum_{i<n+1}t_{i}=\sum_{i<n}t_{i}\mathbin{+}t_{n}$.

2.2 Guarded Recursion

A closed $\mathrm{ACP}$ term denotes a process with a finite upper bound to the number of actions that it can perform. Guarded recursion allows the description of processes without a finite upper bound to the number of actions that it can perform.

Let $T$ be $\mathrm{ACP}$ or a concrete extensions of $\mathrm{ACP}$,222A concrete extension of $\mathrm{ACP}$ is an extension of $\mathrm{ACP}$ that does not offer the possibility of abstraction from certain actions. All extensions of $\mathrm{ACP}$ introduced in this paper are concrete extensions. and let $t$ be a $T$ term containing a variable $X$. Then an occurrence of $X$ in $t$ is guarded if $t$ has a subterm of the form $a\cdot t^{\prime}$ where $a\in\mathsf{A}$ and $t^{\prime}$ is a $T$ term containing this occurrence of $X$.

Let $T$ be $\mathrm{ACP}$ or a concrete extension of $\mathrm{ACP}$. Then a $T$ term $t$ is a guarded $T$ term if all occurrences of variables in $t$ are guarded.

Let $T$ be $\mathrm{ACP}$ or a concrete extension of $\mathrm{ACP}$. Then a guarded recursive specification over $T$ is a finite or countably infinite set of recursion equations $E=\left\{X=t_{X}\mathrel{\mid}X\in V\right\}$, where $V$ is a set of variables and each $t_{X}$ is either a guarded $T$ term in which variables other than the variables from $V$ do not occur or a $T$ term rewritable to such a term using the axioms of $T$ in either direction and/or the equations in $E$, except the equation $X=t_{X}$, from left to right. We write $\mathrm{V}(E)$ for the set of all variables that occur in $E$. A solution of $E$ in some model of $T$ is a set $\left\{P_{X}\mathrel{\mid}X\in\mathrm{V}(E)\right\}$ of elements of the carrier of that model such that the equations of $E$ hold if, for all $X\in\mathrm{V}(E)$, $X$ is assigned $P_{X}$. We are only interested models of $\mathrm{ACP}$ and concrete extensions of $\mathrm{ACP}$ in which guarded recursive specifications have unique solutions.

Let $T$ be $\mathrm{ACP}$ or a concrete extension of $\mathrm{ACP}$. We extend $T$ with guarded recursion by adding constants for solutions of guarded recursive specifications over $T$ and axioms concerning these additional constants. For each guarded recursive specification $E$ over $T$ and each $X\in\mathrm{V}(E)$, we add a constant standing for the unique solution of $E$ for $X$ to the constants of $T$. The constant standing for the unique solution of $E$ for $X$ is denoted by $\langle X|E\rangle$. We use the following notation. Let $t$ be a $T$ term and $E$ be a guarded recursive specification. Then we write $\langle t|E\rangle$ for $t$ with, for all $X\in\mathrm{V}(E)$, all occurrences of $X$ in $t$ replaced by $\langle X|E\rangle$. We add the equation RDP and the conditional equation RSP given in Table 2 to the axioms of $T$.

In RDP and RSP, $X$ stands for an arbitrary variable, $t_{X}$ stands for an arbitrary $T$ term, and $E$ stands for an arbitrary guarded recursive specification over $T$. Side conditions restrict what $X$, $t_{X}$ and $E$ stand for. We write $T_{\mathrm{rec}}$ for the resulting theory.

The equations $\langle X|E\rangle=\langle t_{X}|E\rangle$ for a fixed $E$ express that the constants $\langle X|E\rangle$ make up a solution of $E$. The conditional equations $E\mathrel{\,\Rightarrow\,}X=\langle X|E\rangle$ express that this solution is the only one.

In extensions of $\mathrm{ACP}$ whose axioms include RSP, we have to deal with conditional equational formulas with a countably infinite number of premises. Therefore, infinitary conditional equational logic is used in deriving equations from the axioms of extensions of $\mathrm{ACP}$ whose axioms include RSP. A complete inference system for infinitary conditional equational logic can be found in, for example, [15]. In the case of infinitary conditional equational logic derivation trees may be infinitely branching, but they may not have infinite branches.

3 Strategic Interleaving

In this section, we extend $\mathrm{ACP}$ with strategic interleaving, i.e. interleaving according to some interleaving strategy. Interleaving strategies are abstractions of scheduling algorithms. Interleaving according to some interleaving strategy is what really happens in the case of multi-threading as found in contemporary programming languages.

3.1 $\mathrm{ACP}$ with Strategic Interleaving

In the extension of $\mathrm{ACP}$ with strategic interleaving presented below, it is expected that an interleaving strategy uses the interleaving history in one way or another to make process-scheduling decisions.

The set $\mathcal{H}$ of interleaving histories is the subset of ${(\mathbb{N}_{1}\times\mathbb{N}_{1})}^{\ast}$ that is inductively defined by the following rules:

• •

${\langle\,\rangle}\in\mathcal{H}$;

• •

if $i\leq n$, then $\left(i,n\right)\in\mathcal{H}$;

• •

if h\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\left(i,n\right)\in\mathcal{H}, $j\leq n$, and $n-1\leq m\leq n+1$, then h\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\left(i,n\right)\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\left(j,m\right)\in\mathcal{H}.333We write ${\langle\,\rangle}$ for the empty sequence, $d$ for the sequence having $d$ as sole element, and \alpha\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\alpha^{\prime} for the concatenation of sequences $\alpha$ and $\alpha^{\prime}$. We assume that the usual identities, such as {\langle\,\rangle}\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\alpha=\alpha and (\alpha\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\alpha^{\prime})\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\alpha^{\prime\prime}=\alpha\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}(\alpha^{\prime}\mathbin{\raisebox{1.72218pt}{\scriptstyle\curvearrowright}}\alpha^{\prime\prime}), hold.

The intuition concerning interleaving histories is as follows: if the $k$th pair of an interleaving history is $\left(i,n\right)$, then the $i$th process got a turn in the $k$th interleaving step and after its turn there were $n$ processes to be interleaved. The number of processes to be interleaved may increase due to process creation (introduced below) and decrease due to successful termination of processes.

The presented extension of $\mathrm{ACP}$ is called $\mathrm{ACP{+}SI}$ ($\mathrm{ACP}$ with Strategic Interleaving). It covers a generic interleaving strategy that can be instantiated with different specific interleaving strategies that can be represented in the way that is explained below.

In $\mathrm{ACP{+}SI}$, it is assumed that the following has been given:

• •

a fixed but arbitrary set $S$;

• •

for each $n\in\mathbb{N}_{1}$, a fixed but arbitrary function $\sigma_{n}\mathbin{:}\mathcal{H}\times S\to\left\{1,\ldots,n\right\}$;

• •

for each $n\in\mathbb{N}_{1}$, a fixed but arbitrary function $\vartheta_{n}\mathbin{:}\mathcal{H}\times S\times\left\{1,\ldots,n\right\}\times\mathsf{A}\to S$.

The elements of $S$ are called control states, $\sigma_{n}$ is called an abstract scheduler (for $n$ processes), and $\vartheta_{n}$ is called a control state transformer (for $n$ processes). The intuition concerning $S$, $\sigma_{n}$, and $\vartheta_{n}$ is as follows:

• •

the control states from $S$ encode data that are relevant to the interleaving strategy, but not derivable from the interleaving history;

• •

if $\sigma_{n}(h,s)=i$, then the $i$th process gets the next turn after interleaving history $h$ in control state $s$;

• •

if $\vartheta_{n}(h,s,i,a)=s^{\prime}$, then $s^{\prime}$ is the control state that arises from the $i$th process doing $a$ after interleaving history $h$ in control state $s$.

Thus, $S$, ${\left\langle\sigma_{n}\right\rangle}_{n\in\mathbb{N}_{1}}$, and ${\left\langle\vartheta_{n}\right\rangle}_{n\in\mathbb{N}_{1}}$ make up a way to represent an interleaving strategy. This way to represent an interleaving strategy is engrafted on [23].

Consider the case where $S$ is a singleton set, for each $n\in\mathbb{N}_{1}$, $\sigma_{n}$ is defined by

[TABLE]

and, for each $n\in\mathbb{N}_{1}$, $\vartheta_{n}$ is defined by

[TABLE]

In this case, the interleaving strategy corresponds to the round-robin scheduling algorithm. More advanced strategies can be obtained if the scheduling makes more advanced use of the interleaving history and the control state. The interleaving history may, for example, be used to factor the individual lifetimes of the processes to be interleaved and their creation hierarchy into the process-scheduling decision making. Individual properties of the processes to be interleaved that depend on the actions performed by them can be taken into account by making use of the control state. The control state may, for example, be used to factor the processes being interleaved that currently wait to acquire a lock from a process that manages a shared resource into the process-scheduling decision making.444In [8], various examples of interleaving strategies are given in the setting of the relatively unknown thread algebra. The representation of the more serious of these examples in the current setting demands nontrivial use of the control state.

In $\mathrm{ACP{+}SI}$, it is also assumed that a fixed but arbitrary set $D$ of data and a fixed but arbitrary function $\phi\mathbin{:}D\to P$, where $P$ is the set of all closed terms over the signature of $\mathrm{ACP{+}SI}$ (given below), have been given and that, for each $d\in D$ and $a,b\in\mathsf{A}$, $\mathsf{cr}(d),\overline{\mathsf{cr}}(d)\in\mathsf{A}$, $\gamma(\mathsf{cr}(d),a)=\delta$, and $\gamma(a,b)\neq\mathsf{cr}(d)$. The action $\mathsf{cr}(d)$ can be considered a process creation request and the action $\overline{\mathsf{cr}}(d)$ can be considered a process creation act. They represent the request to start the process denoted by $\phi(d)$ in parallel with the requesting process and the act of carrying out that request, respectively.

The signature of $\mathrm{ACP{+}SI}$ consists of the constants and operators from the signature of $\mathrm{ACP}$ and in addition the following operators:

• •

for each $n\in\mathbb{N}_{1}$, $h\in\mathcal{H}$, and $s\in S$, the $n$-ary strategic interleaving operator $\mathop{\parallel^{n}_{h,s}}$;

• •

for each $n,i\in\mathbb{N}_{1}$ with $i\leq n$, $h\in\mathcal{H}$, and $s\in S$, the $n$-ary positional strategic interleaving operator $\mathop{{\rfloor\lfloor}^{n,i}_{h,s}}$.

The strategic interleaving operators can be explained as follows:

• •

a closed term of the form $\mathop{\parallel^{n}_{h,s}}(t_{1},\ldots,t_{n})$ denotes the process that results from interleaving of the $n$ processes denoted by $t_{1},\ldots,t_{n}$ after interleaving history $h$ in control state $s$, according to the interleaving strategy represented by $S$, ${\left\langle\sigma_{n}\right\rangle}_{n\in\mathbb{N}_{1}}$, and ${\left\langle\vartheta_{n}\right\rangle}_{n\in\mathbb{N}_{1}}$.

The positional strategic interleaving operators are auxiliary operators used to axiomatize the strategic interleaving operators. The role of the positional strategic interleaving operators in the axiomatization is similar to the role of the left merge operator found in $\mathrm{ACP}$.

The axioms of $\mathrm{ACP{+}SI}$ are the axioms of $\mathrm{ACP}$ and in addition the equations given in Table 3.

In the additional equations, $n$ and $i$ stand for arbitrary numbers from $\mathbb{N}_{1}$ with $i\leq n$, $h$ stands for an arbitrary interleaving history from $\mathcal{H}$, $s$ stands for an arbitrary control state from $S$, $a$ stands for an arbitrary action constant that is not of the form $\mathsf{cr}(d)$ or $\overline{\mathsf{cr}}(d)$, and $d$ stands for an arbitrary datum $d$ from $D$.

Axiom SI2 expresses that, in the event of inactiveness of the process whose turn it is, the whole becomes inactive immediately. A plausible alternative is that, in the event of inactiveness of the process whose turn it is, the whole becomes inactive only after all other processes have terminated or become inactive. In that case, the functions $\vartheta_{n}\mathbin{:}\mathcal{H}\times S\times\left\{1,\ldots,n\right\}\times\mathsf{A}\to S$ must be extended to functions $\vartheta_{n}\mathbin{:}\mathcal{H}\times S\times\left\{1,\ldots,n\right\}\times(\mathsf{A}\cup\left\{\delta\right\})\to S$ and axiom SI2 must be replaced by the axioms in Table 4.

In $\mathrm{(ACP{+}SI)_{rec}}$, i.e. $\mathrm{ACP{+}SI}$ extended with guarded recursion in the way described in Section 2, the processes that can be created are restricted to the ones denotable by a closed $\mathrm{ACP{+}SI}$ term. This restriction stems from the requirement that $\phi$ is a function from $D$ to the set of all closed $\mathrm{ACP{+}SI}$ terms. The restriction can be removed by relaxing this requirement to the requirement that $\phi$ is a function from $D$ to the set of all closed $\mathrm{(ACP{+}SI)_{rec}}$ terms. We write $\mathrm{(ACP{+}SI)_{rec}^{+}}$ for the theory resulting from this relaxation. In other words, $\mathrm{(ACP{+}SI)_{rec}^{+}}$ differs from $\mathrm{(ACP{+}SI)_{rec}}$ in that it is assumed that a fixed but arbitrary function $\phi\mathbin{:}D\to P$, where $P$ is the set of all closed terms over the signature of $\mathrm{(ACP{+}SI)_{rec}}$, has been given.

It is customary to associate transition systems with closed terms of the language of an ACP-like theory of processes by means of structural operational semantics and to use this to construct a model in which closed terms are identified if their associated transition systems are bisimilar. The structural operational semantics of $\mathrm{ACP}$ can be found in [5, 13]. The additional transition rules for the strategic interleaving operators and the positional strategic interleaving operators are given in Appendix 0.A.

3.2 Basic Properties of $\mathrm{ACP}$ with Strategic Interleaving

In this section, the subject of concern is the connection between $\mathrm{ACP}$ and $\mathrm{ACP{+}SI}$. The main results are an elimination result, a conservative extension result, and a unique expansion result. We begin with establishing some results that will be used in the proof of those main results.

Let $T$ be $\mathrm{ACP{+}SI}$ or $\mathrm{(ACP{+}SI)_{rec}}$. Then the set $\mathit{HNF}$ of head normal forms of $T$ is inductively defined by the following rules:

• •

$\delta\in\mathit{HNF}$;

• •

if $a\in\mathsf{A}$, then $a\in\mathit{HNF}$;

• •

if $a\in\mathsf{A}$ and $t$ is a $T$ term, then $a\cdot t\in\mathit{HNF}$;

• •

if $t,t^{\prime}\in\mathit{HNF}$, then $t\mathbin{+}t^{\prime}\in\mathit{HNF}$.

Each head normal form of $T$ is derivably equal to a head normal form of the form $\sum_{i<n}a_{i}\cdot t_{i}\mathbin{+}\sum_{j<m}b_{i}$, where $n,m\in\mathbb{N}$, for all $i\in\mathbb{N}$ with $i<n$, $a_{i}\in\mathsf{A}$ and $t_{i}$ is a $T$ term, and, for all $j\in\mathbb{N}$ with $j<m$, $b_{j}\in\mathsf{A}$.

Each guarded $\mathrm{(ACP{+}SI)_{rec}}$ term is derivably equal to a head normal form of $\mathrm{(ACP{+}SI)_{rec}}$.

Proposition 1 (Head normal form)

For each guarded $\mathrm{(ACP{+}SI)_{rec}}$ term $t$, there exists a head normal form $t^{\prime}$ of $\mathrm{(ACP{+}SI)_{rec}}$ such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{(ACP{+}SI)_{rec}}$.

Proof

First we prove the following weaker result about head normal forms:

For each guarded $\mathrm{ACP{+}SI}$ term $t$, there exists a head normal form $t^{\prime}$ of $\mathrm{ACP{+}SI}$ such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{ACP{+}SI}$.

The proof is straightforward by induction on the structure of $t$. The case where $t$ is of the form $\delta$ and the case where $t$ is of the form $a$ ($a\in\mathsf{A}$) are trivial. The case where $t$ is of the form $t_{1}\cdot t_{2}$ follows immediately from the induction hypothesis and the claim that, for all head normal forms $t_{1}$ and $t_{2}$ of $\mathrm{ACP{+}SI}$, there exists a head normal form $t^{\prime}$ of $\mathrm{ACP{+}SI}$ such that $t_{1}\cdot t_{2}=t^{\prime}$ is derivable from the axioms of $\mathrm{ACP{+}SI}$. This claim is easily proved by induction on the structure of $t_{1}$. The case where $t$ is of the form $t_{1}\mathbin{+}t_{2}$ follows immediately from the induction hypothesis. The cases where $t$ is of one of the forms $t_{1}\mathbin{\lfloor\lfloor}t_{2}$, $t_{1}\mathbin{\mid}t_{2}$, ${\partial_{H}}(t_{1})$ or $\mathop{{\rfloor\lfloor}^{n,i}_{h,s}}(t_{1},\ldots,t_{n})$ are proved along the same lines as the case where $t$ is of the form $t_{1}\cdot t_{2}$. In the case that $t$ is of the form $t_{1}\mathbin{\mid}t_{2}$, each of the cases to be considered in the inductive proof of the claim demands a proof by induction on the structure of $t_{2}$. In the case that $t$ is of the form $\mathop{{\rfloor\lfloor}^{n,i}_{h,s}}(t_{1},\ldots,t_{n})$, the claim is of course proved by induction on the structure of $t_{i}$ instead of $t_{1}$. The case that $t$ is of the form $t_{1}\mathbin{\parallel}t_{2}$ follows immediately from the case that $t$ is of the form $t_{1}\mathbin{\lfloor\lfloor}t_{2}$ and the case that $t$ is of the form $t_{1}\mathbin{\mid}t_{2}$. The case that $t$ is of the form $\mathop{\parallel^{n}_{h,s}}(t_{1},\ldots,t_{n})$ follows immediately from the case that $t$ is of the form $\mathop{{\rfloor\lfloor}^{n,i}_{h,s}}(t_{1},\ldots,t_{n})$. Because $t$ is a guarded $\mathrm{ACP{+}SI}$ term, the case where $t$ is a variable cannot occur.

The proof of the proposition itself is also straightforward by induction on the structure of $t$. The cases other than the case where $t$ is of the form $\langle X|E\rangle$ is proved in the same way as in the above proof of the weaker result. The case where $t$ is of the form $\langle X|E\rangle$ follows immediately from the weaker result and RDP. ∎

Each of the four theorems to come refer to several process algebras. It is implicit that the same set $\mathsf{A}$ of actions and the same communication function $\gamma$ are assumed in the process algebras referred to.

Each guarded recursive specification over $\mathrm{ACP{+}SI}$ can be reduced to a guarded recursive specification over $\mathrm{ACP}$.

Theorem 3.1 (Reduction)

For each guarded recursive specification $E$ over $\mathrm{ACP{+}SI}$ and each $X\in\mathrm{V}(E)$, there exists a guarded recursive specification $E^{\prime}$ over $\mathrm{ACP}$ such that $\langle X|E\rangle=\langle X|E^{\prime}\rangle$ is derivable from the axioms of $\mathrm{(ACP{+}SI)_{rec}}$.

Proof

We start with devising an algorithm to construct the guarded recursive specification $E^{\prime}$. The algorithm keeps a set $V$ of recursion equations from $E^{\prime}$ that are already found and a sequence $W$ of equations of the form $X_{k}=\langle t_{k}|E\rangle$ that still have to be transformed. The algorithm has a finite or countably infinite number of stages. In each stage, $V$ and $W$ are finite. Initially, $V$ is empty and $W$ contains only the equation $X_{0}=\langle X|E\rangle$.

In each stage, we remove the first equation from $W$. Assume that this equation is $X_{k}=\langle t_{k}|E\rangle$. We bring the term $\langle t_{k}|E\rangle$ into head normal form. If $t_{k}$ is not a guarded term, then we use RDP here to turn $t_{k}$ into a guarded term first. Thus, by Proposition 1, we can always bring the term $\langle t_{k}|E\rangle$ into head normal form. Assume that the resulting head normal form is $\sum_{i<n}a_{i}\cdot t^{\prime}_{i}\mathbin{+}\sum_{j<m}b_{j}$. Then, we add the equation $X_{k}=\sum_{i<n}a_{i}\cdot X_{k+i+1}\mathbin{+}\sum_{j<m}b_{j}$, where the $X_{k+i+1}$ are fresh variables, to the set $V$. Moreover, for each $i<n$, we add the equation $X_{k+i+1}=t^{\prime}_{i}$ to the end of the sequence $W$. Notice that the terms $t^{\prime}_{i}$ are of the form $\langle t_{k+i+1}|E\rangle$.

Because $V$ grows monotonically, there exists a limit. That limit is the finite or countably infinite linear recursive specification $E^{\prime}$. Every equation that is added to the finite sequence $W$, is also removed from it. Therefore, the right-hand side of each equation from $E^{\prime}$ only contains variables that also occur as the left-hand side of an equation from $E^{\prime}$.

Now, we want to use RSP to show that $\langle X|E\rangle=\langle X|E^{\prime}\rangle$ is derivable from the axioms of $\mathrm{(ACP{+}SI)_{rec}}$. The variables occurring in $E^{\prime}$ are $X_{0},X_{1},X_{2},\ldots\;$. For each $k$, the variable $X_{k}$ has been exactly once in $W$ as the left-hand side of an equation. For each $k$, assume that this equation is $X_{k}=\langle t_{k}|E\rangle$. To use RSP, we have to show for each $k$ that the equation $X_{k}=\sum_{i<n}a_{i}\cdot X_{k+i+1}\mathbin{+}\sum_{j<m}b_{j}$ from $E^{\prime}$ with, for each $l$, all occurrences of $X_{l}$ replaced by $\langle t_{l}|E\rangle$ is derivable from the axioms of $\mathrm{(ACP{+}SI)_{rec}}$. For each $k$, this follows from the construction. ∎

The next three theorems will be proved by means of term rewriting systems. In Appendix 0.B, basic definitions and results regarding term rewriting systems are collected. This appendix also serves to fix the terminology on term rewriting systems used in the proofs of the next three theorems.

Each closed $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term is derivably equal to a closed $\mathrm{ACP_{rec}}$ term.

Theorem 3.2 (Elimination)

For each closed $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term $t$, there exists a closed $\mathrm{ACP_{rec}}$ term $t^{\prime}$ such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{(ACP{+}SI)_{rec}^{+}}$.

Proof

We prove this by means of a term rewriting system that takes equational axioms of $\mathrm{(ACP{+}SI)_{rec}^{+}}$ and equations derivable from the axioms of $\mathrm{(ACP{+}SI)_{rec}^{+}}$ as rewrite rules. Thus, the proof boils down to showing that (a) the term rewriting system concerned has the property that each $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term has a unique normal form modulo axioms A1 and A2 and (b) each closed $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term that is a normal form modulo axioms A1 and A2 is a closed $\mathrm{ACP_{rec}}$ term. Henceforth, we will write AC for the set of equations that consists of axioms A1 and A2.

Let $R$ be a set of equations that contains for each guarded recursive specification $E$ over $\mathrm{ACP{+}SI}$ and $X\in\mathrm{V}(E)$ an equation $\langle X|E\rangle=\langle X|E^{\prime}\rangle$, where $E^{\prime}$ is a guarded recursive specification over $\mathrm{ACP}$, that is derivable from the axioms of $\mathrm{(ACP{+}SI)_{rec}^{+}}$. Such a set $R$ exists by Theorem 3.1. Consider the term rewriting system $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ that consists of the axioms of $\mathrm{(ACP{+}SI)_{rec}^{+}}$, with the exception of A1, A2, RDP, and RSP, and the equations from $R$ taken as rewrite rules.

We show that $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ has the property that each $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term has a unique normal form modulo AC by proving that $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is terminating modulo AC and confluent modulo AC.

First, we show that $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is terminating modulo AC. This can be proved by the reduction ordering $>$ induced by the extended integer polynomials $\theta(t)$ associated with $\mathrm{(ACP{+}SI)_{rec}^{+}}$ terms $t$ as follows:555Here, extended polynomials differ from polynomials in that both variables and expressions of the form $2^{X}$, where $X$ is a variable, are allowed where only variables are allowed in polynomials.

[TABLE]

where it is assumed that, for each variable $X$ over processes, $\underline{X}$ is a variable over integers. The following is easy to see: (a) $t>t^{\prime}$ for all rewrite rules $t=t^{\prime}$ of $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ and (b) $t>t^{\prime}$ implies $s>s^{\prime}$ for all $\mathrm{(ACP{+}SI)_{rec}^{+}}$ terms $s$ and $s^{\prime}$ for which $t=s$ and $t^{\prime}=s^{\prime}$ are derivable from AC.666We do not have that $t>t^{\prime}$ for all rewrite rules $t=s$ if SI2 is replaced by SI2a and SI2b (see Table 4). Hence, $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is terminating modulo AC.

Next, we show that $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is confluent modulo AC. It follows from Theorems 5 and 16 in [20] and the fact that $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is terminating modulo AC that $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is confluent modulo AC if it does not give rise to critical pairs modulo AC that are not convergent. It is easy to see that all critical pairs modulo AC arise from overlappings of (a) A3 on A4, CM4, CM8, CM9, D3, and SI8, (b) A6 on A4, CM4, CM8, CM9, D3, and SI8, (c) A7 on CM3, CM5, CM6, CM7, D4, and SI5, (d) CM10 on CM9, and (e) CM11 on CM8. It is straightforward to check that all critical pairs concerned are convergent. Hence, $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is confluent modulo AC.

Above, we have shown that $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ is terminating modulo AC and confluent modulo AC and by this that it has the property that each $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term has a unique normal form modulo AC. It remains to be shown that each closed $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term that is a normal form modulo AC is a closed $\mathrm{ACP_{rec}}$ term. It is not hard to see that, for each closed $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term in which other operators than $\mathbin{+}$ and $\cdot$ occur, a reduction step modulo AC is still possible in $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$. Because a reduction step modulo AC is impossible for a normal form modulo AC, no other operators than $\mathbin{+}$ or $\cdot$ can occur in a closed $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term that is a normal form modulo AC. Hence, each closed $\mathrm{(ACP{+}SI)_{rec}^{+}}$ term that is a normal form modulo AC is a closed $\mathrm{ACP_{rec}}$ term. ∎

Each equation between closed $\mathrm{ACP}$ terms that is derivable in $\mathrm{ACP{+}SI}$ is also derivable in $\mathrm{ACP}$.

Theorem 3.3 (Conservative extension)

For each two closed $\mathrm{ACP}$ terms $t$ and $t^{\prime}$, $t=t^{\prime}$ is derivable from the axioms of $\mathrm{ACP{+}SI}$ only if $t=t^{\prime}$ is derivable from the axioms of $\mathrm{ACP}$.

Proof

We prove this by means of a restriction of the term rewriting system from the proof of Theorem 3.2. Consider the term rewriting system $\mathcal{R}(\mathrm{ACP{+}SI})$ that consists of the axioms of $\mathrm{ACP{+}SI}$, with the exception of A1 and A2. $\mathcal{R}(\mathrm{ACP{+}SI})$ is $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ restricted to $\mathrm{ACP{+}SI}$ terms. Just like $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$, $\mathcal{R}(\mathrm{ACP{+}SI})$ is terminating modulo AC and confluent modulo AC. The proofs of these properties for $\mathcal{R}(\mathrm{(ACP{+}SI)_{rec}^{+}})$ carry over to $\mathcal{R}(\mathrm{ACP{+}SI})$.

Let $t$ and $t^{\prime}$ be two closed $\mathrm{ACP}$ terms such that $t=t^{\prime}$ is derivable from the axioms of $\mathrm{ACP{+}SI}$. Reduce $t$ and $t^{\prime}$ to normal forms $s$ and $s^{\prime}$, respectively, by means of the term rewriting system $\mathcal{R}(\mathrm{ACP{+}SI})$. By Theorem 5 in [20], being confluent modulo AC is equivalent to being Church-Rosser modulo AC for a term rewriting system that is terminating modulo AC. This means that $t$ and $t^{\prime}$ have the same normal form modulo AC. In other words, $s=s^{\prime}$ is derivable from axioms A1 and A2. Because (a) no other operators than $\mathbin{+}$ and $\cdot$ occur in $t$ and $t^{\prime}$ and (b) no rewrite rule introduces one or more of the other operators if one or more of the other operators was not already in its left-hand side, each rewrite rule applied in the reduction from $t$ to $s$ or the reduction from $t^{\prime}$ to $s^{\prime}$ is one of the axioms of $\mathrm{ACP}$. Therefore, each rewrite rule involved in the reduction from $t$ to $s$ or the reduction from $t^{\prime}$ to $s^{\prime}$ is an axiom of $\mathrm{ACP}$. Hence, the reduction from $t$ to $s$ shows that $t=s$ is derivable from the axioms of $\mathrm{ACP}$ and the reduction from $t^{\prime}$ to $s^{\prime}$ shows that $t^{\prime}=s^{\prime}$ is derivable from the axioms of $\mathrm{ACP}$. From this and the fact that $s=s^{\prime}$ is derivable from axioms A1 and A2, it follows $t=t^{\prime}$ is derivable from the axioms of $\mathrm{ACP}$. ∎

The following theorem concerns the expansion of minimal models of $\mathrm{ACP}$ to models of $\mathrm{ACP{+}SI}$.

Theorem 3.4 (Unique expansion)

Each minimal model of $\mathrm{ACP}$ has a unique expansion to a model of $\mathrm{ACP{+}SI}$.

Proof

We write $f^{\mathcal{A}}$, where $\mathcal{A}$ is a model of $\mathrm{ACP}$ or $\mathrm{ACP{+}SI}$ and $f$ is a constant or operator from the signature of $\mathcal{A}$, for the interpretation of $f$ in $\mathcal{A}$. We write $t^{\mathcal{A}}$, where $\mathcal{A}$ is a model of $\mathrm{ACP}$ or $\mathrm{ACP{+}SI}$ and $t$ is a closed term over the signature of $\mathcal{A}$, for the interpretation of $t$ in $\mathcal{A}$.

Let $\mathcal{A}$ be a minimal model of $\mathrm{ACP}$. Let $\mathit{CT}$ be a function from the carrier of $\mathcal{A}$ to the set of all closed $\mathrm{ACP}$ terms such that, for each element $p$ of the carrier of $\mathcal{A}$, $\mathit{CT}(p)^{\mathcal{A}}=p$. Because $\mathcal{A}$ is a minimal model of $\mathrm{ACP}$, $\mathit{CT}(p)$ is a total function. We write $\underline{p}$, where $p$ is an element of the carrier of $\mathcal{A}$, for $\mathit{CT}(p)$. Let $\mathit{NF}$ be a function from the set of all closed $\mathrm{ACP{+}SI}$ terms to the set of all closed $\mathrm{ACP}$ terms such that, for each closed $\mathrm{ACP{+}SI}$ term $t$, $\mathit{NF}(t)$ is one of the normal forms that $t$ can be reduced to by means of the term rewriting system $\mathcal{R}(\mathrm{ACP{+}SI})$ from the proof of Theorem 3.3.

We start with constructing an expansion of $\mathcal{A}$ with interpretations of the additional operators of $\mathrm{ACP{+}SI}$. Let $\mathcal{B}$ be the expansion of $\mathcal{A}$ with interpretations of the additional operators of $\mathrm{ACP{+}SI}$ where these interpretations are defined as follows:

[TABLE]

for all $p_{1},\ldots,p_{n}$ from the carrier of $\mathcal{A}$.

We proceed with proving that $\mathcal{B}$ is a model of $\mathrm{ACP{+}SI}$. By Theorem 3.3, it is sufficient to prove that $\mathcal{B}$ satisfies axioms SI1–SI8. By its construction, $\mathcal{B}$ is a minimal algebra and consequently it is sufficient to prove that $\mathcal{B}$ satisfies all closed substitution instances of SI1–SI8. We use the following three claims to prove this:

• •

for all closed substitution instances $t=t^{\prime}$ of SI1–SI8, $t^{\mathcal{B}}={\mathit{NF}(t)}^{\mathcal{A}}$;

• •

for all closed substitution instances $t=t^{\prime}$ of SI1–SI8, $t^{\prime\mathcal{B}}={\mathit{NF}(t^{\prime})}^{\mathcal{A}}$;

• •

for all closed substitution instances $t=t^{\prime}$ of SI1–SI8, $\mathit{NF}(t)^{\mathcal{A}}=\mathit{NF}(t^{\prime})^{\mathcal{A}}$.

The first claim follows easily from the definitions of the interpretations of the additional operators of $\mathrm{ACP{+}SI}$ given above. The second claim follows easily from these definitions and the proof of the first claim. Because $\mathcal{R}(\mathrm{ACP{+}SI})$ is Church-Rosser modulo AC (see the proof of Theorem 3.3), we have that $\mathit{NF}(t)=\mathit{NF}(t^{\prime})$ is derivable from axioms A1 and A2. From this, the third claim follows immediately. It is an immediate consequence of the three claims that $\mathcal{B}$ satisfies all closed substitution instances of SI1–SI8.

We still have to prove that $\mathcal{B}$ is the only expansion of $\mathcal{A}$ to a model of $\mathrm{ACP{+}SI}$. We can prove this by contradiction. Assume that $\mathcal{C}$ is an expansion of $\mathcal{A}$ to a model of $\mathrm{ACP{+}SI}$ that differs from $\mathcal{B}$. Then at least one of the additional operators of $\mathrm{ACP{+}SI}$ has different interpretations in $\mathcal{B}$ and $\mathcal{C}$. By the definitions of the interpretations of the additional operators of $\mathrm{ACP{+}SI}$ in $\mathcal{B}$, this means that there exists a closed $\mathrm{ACP{+}SI}$ term $t$ such that $t^{\mathcal{C}}\neq\mathit{NF}(t)^{\mathcal{A}}$. Moreover, because because $t=\mathit{NF}(t)$ is derivable from the axioms of $\mathrm{ACP{+}SI}$, $t^{\mathcal{C}}=\mathit{NF}(t)^{\mathcal{C}}$. Hence, $\mathit{NF}(t)^{\mathcal{C}}\neq\mathit{NF}(t)^{\mathcal{A}}$. Because $\mathit{NF}(t)$ is a closed $\mathrm{ACP}$ term, this contradicts the fact that $\mathcal{C}$ is an expansion of $\mathcal{A}$. ∎

4 Concluding Remarks

We have extended the algebraic theory of processes known as $\mathrm{ACP}$ with the form of interleaving that underlies multi-threading as found in contemporary programming languages. We have also established some basic properties of the resulting theory. It remains an open question whether strategic interleaving is definable in an established extension of $\mathrm{ACP}$.

In [21], we extend a minor variant of $\mathrm{ACP}$, known as $\mathrm{ACP}$ϵ, with strategic interleaving and show that the resulting theory can deal with a process-scheduling policy that supports mutual exclusion of critical subprocesses.

Appendix 0.A Structural Operational Semantics of ACP+SI

It is customary to associate transition systems with closed terms of the language of an ACP-like theory about processes by means of structural operational semantics and to use this to construct a model in which closed terms are identified if their associated transition systems are bisimilar. The structural operational semantics of $\mathrm{ACP}$ can be found in [5, 13]. The additional transition rules for the strategic interleaving operators and the positional strategic interleaving operators are given in Table 5.

In this table,

• •

$t\buildrel{a}\over{\hbox to11.20012pt{\rightarrowfill}}{\scriptstyle\surd}$ indicates that $t$ is capable of performing action $a$ and then terminating successfully;

• •

$t\buildrel{a}\over{\hbox to11.20012pt{\rightarrowfill}}t^{\prime}$ indicates that $t$ is capable of performing action $a$ and then behaving as $t^{\prime}$.

The transition rules for the strategic interleaving operator are similar to the transition rules for the positional strategic interleaving operators, but each transition rule for the strategic interleaving operator has the side-condition $i=\sigma_{n}(h,s)$.

Appendix 0.B Term Rewriting Systems

In this appendix, basic definitions and results regarding term rewriting systems are collected. This appendix also serves to fix the terminology on term rewriting systems used in the proofs that make use of term rewriting systems.

We assume that a set of constants, a set of operators with fixed arities, and a set of variables have been given; and we consider an arbitrary term rewriting system $\mathcal{R}$ for terms that can be built from the constants, operators, and variables in these sets.

A rewrite rule is a pair of terms $t\mathrel{\to}s$, where $t$ is not a variable and each variable occurring in $s$ occurs in $t$ as well. A term rewriting system is a set of rewrite rules.

A reduction step of $\mathcal{R}$ is a pair $t\mathrel{\to}s$ such that for some substitution instance $t^{\prime}\mathrel{\to}s^{\prime}$ of a rewrite rule of $\mathcal{R}$, $t^{\prime}$ is a subterm of $t$, and $s$ is $t$ with $t^{\prime}$ replaced by $s^{\prime}$. Here, $t^{\prime}$ is called the redex of the reduction step. A reduction of $\mathcal{R}$ is a pair $t\mathrel{\to\to}s$ such that either $t\equiv s$ or there exists a finite sequence $t_{1}\mathrel{\to}t_{2}$, …, $t_{n}\mathrel{\to}t_{n+1}$ of consecutive reduction steps of $\mathcal{R}$ such that $t\equiv t_{1}$ and $s\equiv t_{n+1}$.

A term $t$ is a normal form of $\mathcal{R}$ if there does not exist a term $s$ such that $t\mathrel{\to}s$ is a reduction step of $\mathcal{R}$. A term $t$ has a normal form in $\mathcal{R}$ if there exists a reduction $t\mathrel{\to\to}s$ of $\mathcal{R}$ and $s$ is a normal form of $\mathcal{R}$. $\mathcal{R}$ is terminating on term $t$ if there does not exist an infinite sequence $t\mathrel{\to}t_{1}$, $t_{1}\mathrel{\to}t_{2}$, $t_{2}\mathrel{\to}t_{3}$, … of consecutive reduction steps of $\mathcal{R}$. $\mathcal{R}$ is terminating if $\mathcal{R}$ is terminating on all terms. $\mathcal{R}$ is confluent if for all reductions $t\mathrel{\to\to}s_{1}$ and $t\mathrel{\to\to}s_{2}$ of $\mathcal{R}$ there exist reductions $s_{1}\mathrel{\to\to}s$ and $s_{2}\mathrel{\to\to}s$ of $\mathcal{R}$. If $\mathcal{R}$ is terminating and confluent, then each term has a unique normal form in $\mathcal{R}$.

A reduction ordering for $\mathcal{R}$ is a well-founded ordering on terms that is closed under substitutions and contexts. $\mathcal{R}$ is terminating if and only if there exists a reduction ordering $>$ for $\mathcal{R}$ such that $t>s$ for each rewrite rule $t\mathrel{\to}s$ of $\mathcal{R}$.

A unifier of two terms $s$ and $t$ is a substitution $\sigma$ such that $\sigma(s)\equiv\sigma(t)$. A critical pair of $\mathcal{R}$ is a pair $(t_{1},t_{2})$ of terms for which there exist rewrite rules $s\mathrel{\to}s^{\prime}$ and $t\mathrel{\to}t^{\prime}$ of $\mathcal{R}$ and a ‘most general unifier’ $\sigma$ of $s$ and a non-variable subterm of $t$ such that $t_{1}\equiv\sigma(t^{\prime\prime})$ and $t_{2}\equiv\sigma(t^{\prime})$, where $t^{\prime\prime}$ is $t$ with $\sigma(s)$ replaced by $\sigma(s^{\prime})$.777See e.g. Definition 10 in [20] for the definitions of most general unifier and complete set of unifiers modulo $E$. A critical pair $(t_{1},t_{2})$ of $\mathcal{R}$ is convergent if there exist reductions $t_{1}\mathrel{\to\to}s$ and $t_{2}\mathrel{\to\to}s$ of $\mathcal{R}$. If $\mathcal{R}$ is terminating, then $\mathcal{R}$ is confluent if and only if all critical pairs of $\mathcal{R}$ are convergent.

Henceforth, we consider an arbitrary set $E$ of equations between terms.

A reduction step modulo $E$ of $\mathcal{R}$ is a pair $t\mathrel{\to_{\scriptscriptstyle E}}s$ such that there exists a reduction step $t^{\prime}\mathrel{\to}s^{\prime}$ of $\mathcal{R}$ such that $t=t^{\prime}$ and $s=s^{\prime}$ are derivable from $E$. A reduction modulo $E$ of $\mathcal{R}$ is pair $t\mathrel{{\to\to}_{\scriptscriptstyle E}}s$ such that either $t=s$ is derivable from $E$ or there exists a finite sequence $t_{1}\mathrel{\to_{\scriptscriptstyle E}}t_{2}$, …, $t_{n}\mathrel{\to_{\scriptscriptstyle E}}t_{n+1}$ of consecutive reduction steps modulo $E$ of $\mathcal{R}$ such that $t\equiv t_{1}$ and $s\equiv t_{n+1}$.

A term $t$ is a normal form modulo $E$ of $\mathcal{R}$ if there does not exist a term $s$ such that $t\mathrel{\to_{\scriptscriptstyle E}}s$ is a reduction step modulo $E$ of $\mathcal{R}$. A term $t$ has a normal form modulo $E$ in $\mathcal{R}$ if there exists a reduction modulo $E$ $t\mathrel{{\to\to}_{\scriptscriptstyle E}}s$ of $\mathcal{R}$ and $s$ is a normal form modulo $E$ of $\mathcal{R}$. $\mathcal{R}$ is terminating modulo $E$ on term $t$ if there does not exist an infinite sequence $t\mathrel{\to_{\scriptscriptstyle E}}t_{1}$, $t_{1}\mathrel{\to_{\scriptscriptstyle E}}t_{2}$, $t_{2}\mathrel{\to_{\scriptscriptstyle E}}t_{3}$, … of consecutive reduction steps modulo $E$ of $\mathcal{R}$. $\mathcal{R}$ is terminating modulo $E$ if $\mathcal{R}$ is terminating modulo $E$ on all terms. $\mathcal{R}$ is confluent modulo $E$ if for all reductions modulo $E$ $t\mathrel{{\to\to}_{\scriptscriptstyle E}}s_{1}$ and $t\mathrel{{\to\to}_{\scriptscriptstyle E}}s_{2}$ of $\mathcal{R}$ there exist reductions modulo $E$ $s_{1}\mathrel{{\to\to}_{\scriptscriptstyle E}}s$ and $s_{2}\mathrel{{\to\to}_{\scriptscriptstyle E}}s$ of $\mathcal{R}$. If $\mathcal{R}$ is terminating modulo $E$ and confluent modulo $E$, then each term has a unique normal form modulo $E$ in $\mathcal{R}$.

A reduction ordering $>$ for $\mathcal{R}$ is $E$-compatible if $t>s$ implies $t^{\prime}>s^{\prime}$ for all terms $t^{\prime}$ and $s^{\prime}$ for which $t=t^{\prime}$ and $s=s^{\prime}$ are derivable from $E$. $\mathcal{R}$ is terminating modulo $E$ if and only if there exists an $E$-compatible reduction ordering $>$ for $\mathcal{R}$ such that $t>s$ for each rewrite rule $t\mathrel{\to}s$ of $\mathcal{R}$.

A unifier modulo $E$ of two terms $s$ and $t$ is a substitution $\sigma$ such that $\sigma(s)=\sigma(t)$ is derivable from $E$. A critical pair modulo $E$ of $\mathcal{R}$ is a pair $(t_{1},t_{2})$ of terms for which there exist rewrite rules $s\mathrel{\to}s^{\prime}$ and $t\mathrel{\to}t^{\prime}$ of $\mathcal{R}$ and a substitution $\sigma$ from a ‘complete set of unifiers modulo $E$’ of $s$ and a non-variable subterm of $t$ such that $t_{1}\equiv\sigma(t^{\prime\prime})$ and $t_{2}\equiv\sigma(t^{\prime})$, where $t^{\prime\prime}$ is $t$ with $\sigma(s)$ replaced by $\sigma(s^{\prime})$.77footnotemark: 7 If $\mathcal{R}$ is terminating modulo $E$, then $\mathcal{R}$ is confluent modulo $E$ if and only if all critical pairs modulo $E$ of $\mathcal{R}$ are convergent.

An $E$-equality step is a pair $t\mathrel{{\mid{-}\mid}}_{\scriptscriptstyle E}s$ such that, for some substitution instance $t^{\prime}=s^{\prime}$ of an equation from $E$, either $t^{\prime}$ is a subterm of $t$ and $s$ is $t$ with $t^{\prime}$ replaced by $s^{\prime}$ or $s^{\prime}$ is a subterm of $t$ and $s$ is $t$ with $s^{\prime}$ replaced by $t^{\prime}$. An $\mathcal{R}\cup E$-equality step is a pair $t\mathrel{\models\mid}_{\scriptscriptstyle E}s$ such that $t\mathrel{\to}s$ is a reduction step of $\mathcal{R}$ or $s\mathrel{\to}t$ is a reduction step of $\mathcal{R}$ or $t\mathrel{{\mid{-}\mid}}_{\scriptscriptstyle E}s$ is an $E$-equality step. An $\mathcal{R}\cup E$-equality is a pair $t\mathrel{\models{}^{*}\mid}_{\scriptscriptstyle E}s$ such that either $t\equiv s$ or there exists a finite sequence $t_{1}\mathrel{\models\mid}_{\scriptscriptstyle E}t_{2}$, …, $t_{n}\mathrel{\models\mid}_{\scriptscriptstyle E}t_{n+1}$ of consecutive $\mathcal{R}\cup E$-equality steps such that $t\equiv t_{1}$ and $s\equiv t_{n+1}$. $\mathcal{R}$ is Church-Rosser modulo $E$ if for all $\mathcal{R}\cup E$-equalities $t\mathrel{\models{}^{*}\mid}_{\scriptscriptstyle E}t^{\prime}$ there exist reductions modulo $E$ $t\mathrel{{\to\to}_{\scriptscriptstyle E}}s$ and $t^{\prime}\mathrel{{\to\to}_{\scriptscriptstyle E}}s$ of $\mathcal{R}$. If $\mathcal{R}$ is terminating modulo $E$, then $\mathcal{R}$ is Church-Rosser modulo $E$ if and only if $\mathcal{R}$ is confluent modulo $E$.