Imperative Process Algebra with Abstraction

Generally speaking, process algebras focus on the main role of a reactive system, namely maintaining a certain ongoing interaction with its environment. Reactive systems contrast with transformational systems. A transformational system is a system whose main role is to produce, without interruption by its environment, output data from input data.¹¹1The terms reactive system and transformational system are used here with the meaning given in [26]. In general, early computer-based systems were transformational systems. Nowadays, many systems are composed of both reactive components and transformational components. A process carried out by such a system is a process in which data are involved. Usually, the data change in the course of the process, the process proceeds at certain stages in a way that depends on the changing data, and the interaction of the process with other processes consists of communication of data.

This paper introduces an extension of ACP [6] with features that are relevant to processes of the kind referred to above. The extension concerned is called $\textup{ACP}_{\epsilon}^{\tau}$-I. Its additional features include assignment actions to change the data in the course of a process, guarded commands to proceed at certain stages of a process in a way that depends on the changing data, and data parameterized actions to communicate data between processes. The processes of the kind that $\textup{ACP}_{\epsilon}^{\tau}$-I is concerned with are reminiscent of the processes that arise from the execution of imperative programs. In [33], the term imperative process algebra was coined for process algebras like $\textup{ACP}_{\epsilon}^{\tau}$-I. Other imperative process algebras are VPLA [27], IPAL [33], CSP_σ [16], AWN [19], and the unnamed process algebra introduced in [13].

$\textup{ACP}_{\epsilon}^{\tau}$-I distinguishes itself from those imperative process algebras by being the only one with the following three properties: (1) it supports abstraction from actions that are considered not to be visible; (2) a verification of the equivalence of two processes in its semantics is automatically valid in any semantics that is fully abstract with respect to some notion of observable behaviour (cf. [41]); (3) it offers the possibility of equational verification of process equivalence. CSP_σ is the only one of the above-mentioned imperative process algebras that has property (1) and none of them has property (2). $\textup{ACP}_{\epsilon}^{\tau}$-I is probably unique in being the only imperative process algebra with properties (1), (2) and (3).

Property (1) is achieved by providing a special constant (called the silent step constant), special operators (called abstraction operators), and an appropriate notion of equivalence of processes in the semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I. Property (2) is achieved by using a notion of branching bisimulation equivalence [41] for the equivalence of processes in the semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I. Property (3) is achieved by providing an equational axiomatization of the equivalence concerned.

Property (1) is essential for the verification of properties concerning the external behaviour of a system. Property (2) is desirable for such verifications in applications where the final word on what exactly is observable behaviour has not been pronounced. This means that $\textup{ACP}_{\epsilon}^{\tau}$-I is an interesting process algebra for the verification of properties concerning the external behaviour of a system whose description calls for an imperative process algebra. It makes $\textup{ACP}_{\epsilon}^{\tau}$-I, among other things, suitable for the verification of properties concerning the information-flow security of a system in which confidential and non-confidential data, contained in state components of the system, are looked up and changed and an ongoing interaction with the environment of the system is maintained.

A great part of the work done on information-flow security is concerned with secure information flow in programs, where information flow in a program is considered secure if information derivable from the confidential data contained in its high-security variables cannot be inferred from the non-confidential data contained in its low-security variables (see e.g. [42, 40, 12, 34, 10]). A notable exception is the work done in a process-algebra setting, where the focus has shifted from programs to processes of the kind to which programs in execution belong and where the information flow in a process is usually considered secure if information derivable from confidential actions cannot be inferred from non-confidential actions (see e.g. [20, 36, 11, 31]).

Recent work done on information-flow security in a process-algebra setting occasionally deals with the data-oriented notion of secure information flow, but on such occasions program variables are always mimicked by processes (see e.g. [21, 29]). A suitable imperative process algebra would obviate the need to mimic program variables. This state of affairs motivated the development of $\textup{ACP}_{\epsilon}^{\tau}$-I. This paper also shows how $\textup{ACP}_{\epsilon}^{\tau}$-I can be used for information-flow security analysis of the kind that is concerned with the leakage of confidential data.

The development of $\textup{ACP}_{\epsilon}^{\tau}$-I was primarily aimed at obtaining an imperative process algebra with the properties that are designated above as essential and desirable for the verification of properties concerning the external behaviour of a system. The starting point of the development of $\textup{ACP}_{\epsilon}^{\tau}$-I is $\textup{ACP}_{\epsilon}^{\tau}$ [3, Section 5.3], which is a non-imperative process algebra with these properties. This makes it a convenient starting point in view of the primary aim of the development.

$\textup{ACP}_{\epsilon}^{\tau}$-I is closely related to $\textup{ACP}_{\epsilon}^{*}$-D [9]. The main differences between them can be summarized as follows: (a) only the former supports abstraction from actions that are considered not to be visible and (b) only the latter has an iteration operator. This paper introduces, in addition to $\textup{ACP}_{\epsilon}^{\tau}$-I, guarded linear recursion in the setting of $\textup{ACP}_{\epsilon}^{\tau}$-I. The set of processes that can be defined by means of the operators of $\textup{ACP}_{\epsilon}^{\tau}$-I extended with the iteration operator is a proper subset of the set of processes that can be defined by means of guarded linear recursion in the setting of $\textup{ACP}_{\epsilon}^{\tau}$-I. Therefore, (a) should be considered the important difference. However, using the semantics of $\textup{ACP}_{\epsilon}^{*}$-D as presented in [9] as the starting point of the semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I turned out to result in a semantics that is too complicated to establish the soundness and semi-completeness results.

This paper is organized as follows. First, a survey of the algebraic theory $\textup{ACP}_{\epsilon}^{\tau}$, which is the extension of ACP with the empty process constant $\epsilon$ and the silent step constant $\tau$, is given (Section 2). Next, the algebraic theory $\textup{ACP}_{\epsilon}^{\tau}$-I is introduced as an extension of $\textup{ACP}_{\epsilon}^{\tau}$ (Section 3) and guarded linear recursion in the setting of $\textup{ACP}_{\epsilon}^{\tau}$-I is treated (Section 4). After that, a structural operational semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I is presented and a notion of branching bisimulation equivalence based on this semantics is defined (Section 5). Following this, the reasons for two relatively uncommon choices made in the preceding sections are clarified (Section 6). Then, results concerning the soundness and (semi-)completeness of the given axiomatization with respect to branching bisimulation equivalence are established (Section 7). Thereafter, it is explained how $\textup{ACP}_{\epsilon}^{\tau}$-I can be used for information-flow security analysis of the kind that is concerned with the leakage of confidential data (Section 8). Finally, some concluding remarks are made (Section 9).

There is also an appendix in which, for comparison, an alternative structural operational semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I is presented and a notion of branching bisimulation equivalence based on this alternative structural operational semantics is defined. The alternative in question is the above-mentioned result of using the structural operational semantics of $\textup{ACP}_{\epsilon}^{*}$-D as the starting point.

Section 2, Section 3, and the appendix mainly extend the material in Section 2, Section 3, and Section 4, respectively, of [9]. Portions of that material have been copied near verbatim or slightly modified.

In this section, $\textup{ACP}_{\epsilon}^{\tau}$ is presented. $\textup{ACP}_{\epsilon}^{\tau}$ is ACP [6] extended with the empty process constant $\epsilon$ and the silent step constant $\tau$ as in [3, Section 5.3]. In $\textup{ACP}_{\epsilon}^{\tau}$, it is assumed that a fixed but arbitrary finite set $\mathsf{A}$ of basic actions, with $\tau,\delta,\epsilon\not\in\mathsf{A}$, and a fixed but arbitrary commutative and associative communication function ${\gamma}\mathbin{:}(\mathsf{A}\cup\{\tau,\delta\})\times(\mathsf{A}\cup\{\tau,\delta\})\to(\mathsf{A}\cup\{\tau,\delta\})$, such that $\gamma(\tau,a)=\delta$ and $\gamma(\delta,a)=\delta$ for all $a\in\mathsf{A}\cup\{\tau,\delta\}$, have been given. Basic actions are taken as atomic processes. The function $\gamma$ is regarded to give the result of synchronously performing any two basic actions for which this is possible, and to be $\delta$ otherwise. Henceforth, we write ${\mathsf{A}_{\tau}}$ for $\mathsf{A}\cup\{\tau\}$.

The algebraic theory $\textup{ACP}_{\epsilon}^{\tau}$ has one sort: the sort $\mathbf{P}$ of processes. This sort is made explicit to anticipate the need for many-sortedness later on. The algebraic theory $\textup{ACP}_{\epsilon}^{\tau}$ has the following constants and operators to build terms of sort $\mathbf{P}$:

• •

  for each $a\in\mathsf{A}$, the basic action constant ${a}\mathbin{:}\mathbf{P}$;

• •

  the silent step constant ${\tau}\mathbin{:}\mathbf{P}$;

• •

  the inaction constant ${\delta}\mathbin{:}\mathbf{P}$;

• •

  the empty process constant ${\epsilon}\mathbin{:}\mathbf{P}$;

• •

  the binary alternative composition operator ${\mathbin{+}}\mathbin{:}\mathbf{P}\times\mathbf{P}\to\mathbf{P}$;

• •

  the binary sequential composition operator ${\cdot}\mathbin{:}\mathbf{P}\times\mathbf{P}\to\mathbf{P}$;

• •

  the binary parallel composition operator ${\mathbin{\parallel}}\mathbin{:}\mathbf{P}\times\mathbf{P}\to\mathbf{P}$;

• •

  the binary left merge operator ${\mathbin{\lfloor\lfloor}}\mathbin{:}\mathbf{P}\times\mathbf{P}\to\mathbf{P}$;

• •

  the binary communication merge operator ${\mathbin{\mid}}\mathbin{:}\mathbf{P}\times\mathbf{P}\to\mathbf{P}$;

• •

  for each $H\subseteq\mathsf{A}$ and for $H={\mathsf{A}_{\tau}}$, the unary encapsulation operator ${{\partial_{H}}}\mathbin{:}\mathbf{P}\to\mathbf{P}$;

• •

  for each $I\subseteq\mathsf{A}$, the unary abstraction operator ${{\tau_{I}}}\mathbin{:}\mathbf{P}\to\mathbf{P}$.

It is assumed that there is a countably infinite set $\mathcal{X}$ of variables of sort $\mathbf{P}$, which contains $x$, $y$ and $z$. Terms are built as usual. Infix notation is used for the binary operators. The following precedence conventions are used to reduce the need for parentheses: the operator ${}\cdot{}$ binds stronger than all other binary operators and the operator ${}\mathbin{+}{}$ binds weaker than all other binary operators.

The constants of $\textup{ACP}_{\epsilon}^{\tau}$ can be explained as follows ($a\in\mathsf{A}$):

• •

  $a$ denotes the process that performs the observable action $a$ and after that terminates successfully;

• •

  $\tau$ denotes the process that performs the unobservable action $\tau$ and after that terminates successfully;

• •

  $\epsilon$ denotes the process that terminates successfully without performing any action;

• •

  $\delta$ denotes the process that cannot do anything, it cannot even terminate successfully.

Let $t$ and $t^{\prime}$ be closed $\textup{ACP}_{\epsilon}^{\tau}$ terms denoting processes $p$ and $p^{\prime}$, respectively, let $H\subseteq\mathsf{A}$ or $H={\mathsf{A}_{\tau}}$, and let $I\subseteq\mathsf{A}$. Then the operators of $\textup{ACP}_{\epsilon}^{\tau}$ can be explained as follows:

• •

  $t\mathbin{+}t^{\prime}$ denotes the process that behaves either as $p$ or as $p^{\prime}$, where the choice between the two is resolved at the instant that one of them performs its first action or terminates successfully without performing any action, and not before;

• •

  $t\cdot t^{\prime}$  denotes the process that first behaves as $p$ and following successful termination of $p$ behaves as $p^{\prime}$;

• •

  $t\mathbin{\parallel}t^{\prime}$ denotes the process that behaves as $p$ and $p^{\prime}$ in parallel, by which is meant that, each time an action is performed, either a next action of $p$ is performed or a next action of $p^{\prime}$ is performed or a next action of $p$ and a next action of $p^{\prime}$ are performed synchronously — successful termination may take place at any time that both $p$ and $p^{\prime}$ can terminate successfully;

• •

  $t\mathbin{\lfloor\lfloor}t^{\prime}$ denotes the same process as $t\mathbin{\parallel}t^{\prime}$, except that it starts with performing an action of $p$;

• •

  $t\mathbin{\mid}t^{\prime}$ denotes the same process as $t\mathbin{\parallel}t^{\prime}$, except that it starts with performing an action of $p$ and an action of $p^{\prime}$ synchronously;

• •

  ${\partial_{H}}(t)$ denotes the process that behaves the same as $p$, except that actions from $H$ are blocked from being performed;

• •

  ${\tau_{I}}(t)$ denotes the process that behaves the same as $p$, except that actions from $I$ are turned into the unobservable action $\tau$.

The operators $\mathbin{\lfloor\lfloor}$ and $\mathbin{\mid}$ are of an auxiliary nature. They make a finite axiomatization of $\textup{ACP}_{\epsilon}^{\tau}$ possible.

The operator ${\partial_{{\mathsf{A}_{\tau}}}}$ can also be explained as follows: ${\partial_{{\mathsf{A}_{\tau}}}}\!(t)$ denotes the process that behaves the same as $\epsilon$ if $t$ denotes a process that has the option to behave the same as $\epsilon$ and it denotes the process that behaves the same as $\delta$ otherwise. In [3, Section 5.3], the symbol $\surd$ is used instead of ${\partial_{{\mathsf{A}_{\tau}}}}$.

The axioms of $\textup{ACP}_{\epsilon}^{\tau}$ are presented in Table 1.

In these equations, $a$, $b$, and $\alpha$ stand for arbitrary constants of $\textup{ACP}_{\epsilon}^{\tau}$ other than $\epsilon$,  $H$ stands for an arbitrary subset of $\mathsf{A}$ or the set ${\mathsf{A}_{\tau}}$, and $I$ stands for an arbitrary subset of $\mathsf{A}$. So, CM3, CM7, D0–D4, T0–T4, and BE are actually axiom schemas. In this paper, axiom schemas will usually be referred to as axioms.

The occurrence of the strange-looking term ${\partial_{{\mathsf{A}_{\tau}}}}\!(x)\cdot{\partial_{{\mathsf{A}_{\tau}}}}\!(y)$ in axiom CM1E deserves some explanation. This term is needed to handle successful termination in the presence of $\epsilon$: it stands for the process that behaves the same as $\epsilon$ if both $x$ and $y$ stand for a process that has the option to behave the same as $\epsilon$ and it stands for the process that behaves the same as $\delta$ otherwise.

Notice that there are no operators ${\partial_{H}}$ for $H\subset{\mathsf{A}_{\tau}}$ with $\tau\in H$ in $\textup{ACP}_{\epsilon}^{\tau}$. If one or more of them were present, the equation $\alpha\cdot\delta=\alpha$ would be derivable from the axioms of $\textup{ACP}_{\epsilon}^{\tau}$.

In the sequel, the notation $\sum_{i=1}^{n}t_{i}$, where $n\geq 1$, will be used for right-nested alternative compositions. For each $n\in\mathbb{N}^{+}$,²²2We write $\mathbb{N}^{+}$ for the set $\{n\in\mathbb{N}\mathrel{\mid}n\geq 1\}$ of positive natural numbers. the term $\sum_{i=1}^{n}t_{i}$ is defined by induction on $n$ as follows: $\sum_{i=1}^{1}t_{i}=t_{1}$ and $\sum_{i=1}^{n+1}t_{i}=t_{1}\mathbin{+}\sum_{i=1}^{n}t_{i+1}$. In addition, the convention will be used that $\sum_{i=1}^{0}t_{i}=\delta$.

In this section, $\textup{ACP}_{\epsilon}^{\tau}$-I, imperative $\textup{ACP}_{\epsilon}^{\tau}$, is presented. This extension of $\textup{ACP}_{\epsilon}^{\tau}$ has been inspired by [8]. It extends $\textup{ACP}_{\epsilon}^{\tau}$ with features that are relevant to processes in which data are involved, such as guarded commands (to deal with processes that only take place if some data-dependent condition holds), data parameterized actions (to deal with process interactions with data transfer), and assignment actions (to deal with data that change in the course of a process).

In $\textup{ACP}_{\epsilon}^{\tau}$-I, it is assumed that the following has been given with respect to data:

• •

  a many-sorted signature $\mathrm{\Sigma}_{\mathfrak{D}}$ that includes:

  • –

    a sort ${\mathbf{D}}$ of data and a sort ${\mathbf{B}}$ of booleans;

  • –

    constants of sort ${\mathbf{D}}$ and/or operators with result sort ${\mathbf{D}}$;

  • –

    constants $\mathsf{t\!t}$ and $\mathsf{f\!f}$ of sort ${\mathbf{B}}$ and operators with result sort ${\mathbf{B}}$;

• •

  a minimal algebra $\mathfrak{D}$ of the signature $\mathrm{\Sigma}_{\mathfrak{D}}$ in which the carrier of sort ${\mathbf{B}}$ has cardinality $2$ and the equation $\mathsf{t\!t}=\mathsf{f\!f}$ does not hold.

We write $\mathbb{D}$ for the set of all closed terms over the signature $\mathrm{\Sigma}_{\mathfrak{D}}$ that are of sort ${\mathbf{D}}$. The sort ${\mathbf{B}}$ is assumed to be given in order to make it possible for operators to serve as predicates.

It is also assumed that a finite or countably infinite set $\mathcal{V}$ of flexible variables has been given. A flexible variable is a variable whose value may change in the course of a process.³³3The term flexible variable is used for this kind of variables in e.g. [39, 30]. Typical examples of flexible variables are the program variables known from imperative programming. An evaluation map is a function from $\mathcal{V}$ to $\mathbb{D}$. We write $\mathcal{E}\!\mathcal{M}$ for the set of all evaluation maps.

The algebraic theory $\textup{ACP}_{\epsilon}^{\tau}$-I has the following sorts: the sort $\mathbf{P}$ of processes, the sort ${\mathbf{C}}$ of conditions, and the sorts from $\mathrm{\Sigma}_{\mathfrak{D}}$.

It is assumed that there are countably infinite sets of variables of sort ${\mathbf{C}}$ and ${\mathbf{D}}$ and that the sets of variables of sort $\mathbf{P}$, ${\mathbf{C}}$, and ${\mathbf{D}}$ are mutually disjoint and disjoint from $\mathcal{V}$.

Below, the constants and operators of $\textup{ACP}_{\epsilon}^{\tau}$-I are introduced. The operators of $\textup{ACP}_{\epsilon}^{\tau}$-I include two variable-binding operators. The formation rules for $\textup{ACP}_{\epsilon}^{\tau}$-I terms are the usual ones for the many-sorted case (see e.g. [38, 43]) and in addition the following rule:

• •

  if $O$ is a variable-binding operator ${O}\mathbin{:}S_{1}\times\ldots\times S_{n}\to S$ that binds a variable of sort $S^{\prime}$, $t_{1},\ldots,t_{n}$ are terms of sorts $S_{1},\ldots,S_{n}$, respectively, and $X$ is a variable of sort $S^{\prime}$, then $OX(t_{1},\ldots,t_{n})$ is a term of sort $S$.

An extensive formal treatment of the phenomenon of variable-binding operators can be found in [35].

$\textup{ACP}_{\epsilon}^{\tau}$-I has the constants and operators from $\mathrm{\Sigma}_{\mathfrak{D}}$ to build terms of the sorts from $\mathrm{\Sigma}_{\mathfrak{D}}$ — which include the sort ${\mathbf{B}}$ and the sort ${\mathbf{D}}$ — and in addition the following constants to build terms of sort ${\mathbf{D}}$:

• •

  for each $v\in\mathcal{V}$, the flexible variable constant ${v}\mathbin{:}{\mathbf{D}}$.

We write $\mathcal{D}$ for the set of all closed $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort ${\mathbf{D}}$.

Evaluation maps are intended to provide the data values assigned to flexible variables when an $\textup{ACP}_{\epsilon}^{\tau}$-I term of sort ${\mathbf{D}}$ is evaluated. However, in order to fit better in an algebraic setting, they provide closed terms over the signature $\mathrm{\Sigma}_{\mathfrak{D}}$ that denote those data values instead. The requirement that $\mathfrak{D}$ is a minimal algebra guarantees that each data value can be represented by a closed term.

$\textup{ACP}_{\epsilon}^{\tau}$-I has the following constants and operators to build terms of sort ${\mathbf{C}}$:

• •

  the binary equality operator ${=}\mathbin{:}{\mathbf{B}}\times{\mathbf{B}}\to{\mathbf{C}}$;

• •

  the binary equality operator ${=}\mathbin{:}{\mathbf{D}}\times{\mathbf{D}}\to{\mathbf{C}}$;⁴⁴4The overloading of $=$ can be trivially resolved if $\mathrm{\Sigma}_{\mathfrak{D}}$ is without overloaded symbols.

• •

  the truth constant ${{\mathsf{t}}}\mathbin{:}{\mathbf{C}}$;

• •

  the falsity constant ${{\mathsf{f}}}\mathbin{:}{\mathbf{C}}$;

• •

  the unary negation operator ${\lnot}\mathbin{:}{\mathbf{C}}\to{\mathbf{C}}$;

• •

  the binary conjunction operator ${\land}\mathbin{:}{\mathbf{C}}\times{\mathbf{C}}\to{\mathbf{C}}$;

• •

  the binary disjunction operator ${\lor}\mathbin{:}{\mathbf{C}}\times{\mathbf{C}}\to{\mathbf{C}}$;

• •

  the binary implication operator ${\mathrel{\Rightarrow}}\mathbin{:}{\mathbf{C}}\times{\mathbf{C}}\to{\mathbf{C}}$;

• •

  the unary variable-binding universal quantification operator ${\forall}\mathbin{:}{\mathbf{C}}\to{\mathbf{C}}$ that binds a variable of sort ${\mathbf{D}}$;

• •

  the unary variable-binding existential quantification operator ${\exists}\mathbin{:}{\mathbf{C}}\to{\mathbf{C}}$ that binds a variable of sort ${\mathbf{D}}$.

We write $\mathcal{C}$ for the set of all closed $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort ${\mathbf{C}}$.

Each term from $\mathcal{C}$ can be taken as a formula of a first-order language with equality of $\mathfrak{D}$ by taking the flexible variable constants as additional variables of sort ${\mathbf{D}}$. The flexible variable constants are implicitly taken as additional variables of sort ${\mathbf{D}}$ wherever the context asks for a formula. In this way, each term from $\mathcal{C}$ can be interpreted as a formula in $\mathfrak{D}$.

$\textup{ACP}_{\epsilon}^{\tau}$-I has the constants and operators of $\textup{ACP}_{\epsilon}^{\tau}$ and in addition the following operators to build terms of sort $\mathbf{P}$:

• •

  the binary guarded command operator ${\mathbin{:\rightarrow}\,}\mathbin{:}{\mathbf{C}}\times\mathbf{P}\to\mathbf{P}$;

• •

  for each $n\in\mathbb{N}$, for each $a\in\mathsf{A}$, the $n$-ary data parameterized action operator ${a}\mathbin{:}\underbrace{{\mathbf{D}}\times\cdots\times{\mathbf{D}}}_{n\;\mathrm{times}}\to\mathbf{P}$;

• •

  for each $v\in\mathcal{V}$, a unary assignment action operator ${v\mathbin{{:}{=}}\,}\mathbin{:}{\mathbf{D}}\to\mathbf{P}$;

• •

  for each $\sigma\in\mathcal{E}\!\mathcal{M}$, a unary evaluation operator ${{\mathsf{V}_{\sigma}}}\mathbin{:}\mathbf{P}\to\mathbf{P}$.

We write $\mathcal{P}$ for the set of all closed $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort $\mathbf{P}$.

The same notational conventions are used as before. Infix notation is also used for the additional binary operators. Moreover, the notation $[v\mathbin{{:}{=}}e]$, where $v\in\mathcal{V}$ and $e$ is a $\textup{ACP}_{\epsilon}^{\tau}$-I term of sort ${\mathbf{D}}$, is used for the term $v\mathbin{{:}{=}}(e)$.

The notation $\phi\mathrel{\Leftrightarrow}\psi$, where $\phi$ and $\psi$ are $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort ${\mathbf{C}}$, is used for the term $(\phi\mathrel{\Rightarrow}\psi)\land(\psi\mathrel{\Rightarrow}\phi)$. The axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I (given below) include an equation $\phi=\psi$ for each two terms $\phi$ and $\psi$ from $\mathcal{C}$ for which the formula $\phi\mathrel{\Leftrightarrow}\psi$ holds in $\mathfrak{D}$.

Let $t$ be a term from $\mathcal{P}$, $\phi$ be a term from $\mathcal{C}$, $e_{1},\ldots,e_{n}$ and $e$ be terms from $\mathcal{D}$, and $a$ be a basic action from $\mathsf{A}$. Then the additional operators to build terms of sort $\mathbf{P}$ can be explained as follows:

• •

  the term $\phi\mathbin{:\rightarrow}t$ denotes the process that behaves as the process denoted by $t$ if condition $\phi$ holds and as $\delta$ otherwise;

• •

  the term $a(e_{1},\ldots,e_{n})$ denotes the process that performs the data parameterized action $a(e_{1},\ldots,e_{n})$ and after that terminates successfully;

• •

  the term $[v\mathbin{{:}{=}}e]$ denotes the process that performs the assignment action $[v\mathbin{{:}{=}}e]$, whose intended effect is the assignment of the result of evaluating $e$ to flexible variable $v$, and after that terminates successfully;

• •

  the term ${\mathsf{V}_{\sigma}}(t)$ denotes the process that behaves the same as the process denoted by $t$ except that each subterm of $t$ that belongs to $\mathcal{D}$ is evaluated using the evaluation map $\sigma$ updated according to the assignment actions that have taken place at the point where the subterm is encountered.

Evaluation operators are a variant of state operators (see e.g. [1]).

The following closed $\textup{ACP}_{\epsilon}^{\tau}$-I term is reminiscent of a program that computes the difference between two integers by subtracting the smaller one from the larger one ($i,j,d\in\mathcal{V}$):

$$\begin{array}[]{@{}l@{}}[d\mathbin{{:}{=}}i]\cdot((d\geq j=\mathsf{t\!t})\mathbin{:\rightarrow}[d\mathbin{{:}{=}}d-j]\mathbin{+}(d\geq j=\mathsf{f\!f})\mathbin{:\rightarrow}[d\mathbin{{:}{=}}j-d])\;.\end{array}$$

That is, the final value of $d$ is the absolute value of the result of subtracting the initial value of $i$ from the initial value of $j$. An evaluation operator can be used to show that this is the case for given initial values of $i$ and $j$. For example, consider the case where the initial values of $i$ and $j$ are $11$ and $3$, respectively. Let $\sigma$ be an evaluation map such that $\sigma(i)=11$ and $\sigma(j)=3$. Then the following equation can be derived from the axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I given below:

$$\begin{array}[]{@{}l@{}}{\mathsf{V}_{\sigma}}([d\mathbin{{:}{=}}i]\cdot((d\geq j=\mathsf{t\!t})\mathbin{:\rightarrow}[d\mathbin{{:}{=}}d-j]\mathbin{+}(d\geq j=\mathsf{f\!f})\mathbin{:\rightarrow}[d\mathbin{{:}{=}}j-d]))\\ \;{}=[d\mathbin{{:}{=}}11]\cdot[d\mathbin{{:}{=}}8]\;.\end{array}$$

This equation shows that in the case where the initial values of $i$ and $j$ are $11$ and $3$ the final value of $d$ is $8$ (which is the absolute value of the result of subtracting $11$ from $3$).

An evaluation map $\sigma$ can be extended homomorphically from flexible variables to $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort ${\mathbf{D}}$ and $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort ${\mathbf{C}}$. These extensions are denoted by $\sigma$ as well. Below, we write $\sigma\{e/v\}$ for the evaluation map $\sigma^{\prime}$ defined by $\sigma^{\prime}(v^{\prime})=\sigma(v^{\prime})$ if $v^{\prime}\neq v$ and $\sigma^{\prime}(v)=e$.

Three subsets of $\mathcal{P}$ are defined:

$$\begin{array}[]{@{}l@{}}\begin{array}[t]{@{}l@{\;}c@{\;}l@{}l@{}}\mathcal{A}^{\mathit{dpa}}&=&{}\bigcup_{n\in\mathbb{N}^{+}}\{a(e_{1},\dots,e_{n})\mathrel{\mid}a\in\mathsf{A}\land e_{1},\dots,e_{n}\in\mathcal{D}\}\;,\\ \mathcal{A}^{\mathit{ass}}&=&\{[v\mathbin{{:}{=}}e]\mathrel{\mid}v\in\mathcal{V}\land e\in\mathcal{D}\}\;,\\ \mathcal{A}&=&\{a\mathrel{\mid}a\in\mathsf{A}\}\cup\mathcal{A}^{\mathit{dpa}}\cup\mathcal{A}^{\mathit{ass}}\;.\end{array}\end{array}$$

In $\textup{ACP}_{\epsilon}^{\tau}$-I, the elements of $\mathcal{A}$ are the terms from $\mathcal{P}$ that denote the processes that are considered to be atomic. Henceforth, we write $\mathcal{A}_{\tau}$ for $\mathcal{A}\cup\{\tau\}$ and $\mathcal{A}_{\tau\delta}$ for $\mathcal{A}\cup\{\tau,\delta\}$.

The axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I are the axioms presented in Table 1, on the understanding that $\alpha$ now stands for an arbitrary term from $\mathcal{A}_{\tau\delta}$,  $H$ now stands for an arbitrary subset of $\mathcal{A}$ or the set $\mathcal{A}_{\tau}$, and $I$ now stands for an arbitrary subset of $\mathcal{A}$, and in addition the axioms presented in Table 2.

In the latter table, $\phi$ and $\psi$ stand for arbitrary terms from $\mathcal{C}$,  $e$, $e_{1},e_{2},\ldots$, and $e^{\prime}$, $e^{\prime}_{1},e^{\prime}_{2},\ldots$ stand for arbitrary terms from $\mathcal{D}$,  $v$ stands for an arbitrary flexible variable from $\mathcal{V}$,  $\sigma$ stands for an arbitrary evaluation map from $\mathcal{E}\!\mathcal{M}$,  $a,b$, and $c$ stand for arbitrary basic actions from $\mathsf{A}$, and $\alpha$ stands for an arbitrary term from $\mathcal{A}_{\tau\delta}$.

Axioms GC1–GC12 have been taken from [2] (using a different numbering), but with the axioms with occurrences of Hoare’s ternary counterpart of the guarded command operator (see below) replaced by simpler axioms. Axioms CM7Da and CM7Db have been inspired by [8]. Axiom BED is axiom BE generalized to the current setting. An equivalent axiomatization is obtained if axiom BED is replaced by the equation $\alpha\cdot(\phi\mathbin{:\rightarrow}\tau\cdot x)=\alpha\cdot(\phi\mathbin{:\rightarrow}x)$.

Some earlier extensions of ACP include Hoare’s ternary counterpart of the binary guarded command operator (see e.g. [2]). This operator can be defined by the equation $x\mathbin{\lhd\,u\,\rhd}y=u\mathbin{:\rightarrow}x\mathbin{+}(\lnot\,u)\mathbin{:\rightarrow}y$. From this defining equation, it follows that $u\mathbin{:\rightarrow}x=x\mathbin{\lhd\,u\,\rhd}\delta$. In [25], a unary counterpart of the binary guarded command operator is used. This operator can be defined by the equation $\{u\}=u\mathbin{:\rightarrow}\epsilon$. From this defining equation, it follows that $u\mathbin{:\rightarrow}x=\{u\}\cdot x$ and also that $\{{\mathsf{t}}\}=\epsilon$ and $\{{\mathsf{f}}\}=\delta$.

A closed $\textup{ACP}_{\epsilon}^{\tau}$-I term of sort $\mathbf{P}$ denotes a process with a finite upper bound to the number of actions that it can perform. Recursion allows the description of processes without a finite upper bound to the number of actions that it can perform.

A recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I is a set $\{X_{i}=t_{i}\mathrel{\mid}i\in I\}$, where $I$ is a finite set, each $X_{i}$ is a variable from $\mathcal{X}$, each $t_{i}$ is a $\textup{ACP}_{\epsilon}^{\tau}$-I term of sort $\mathbf{P}$ in which only variables from $\{X_{i}\mathrel{\mid}i\in I\}$ occur, and $X_{i}\neq X_{j}$ for all $i,j\in I$ with $i\neq j$. We write $\mathrm{vars}(E)$, where $E$ is a recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I, for the set of all variables that occur in $E$. Let $E$ be a recursive specification and let $X\in\mathrm{vars}(E)$. Then the unique equation $X\!=t\;\in\,E$ is called the recursion equation for $X$ in $E$.

Below, recursive specifications over $\textup{ACP}_{\epsilon}^{\tau}$-I are introduced in which the right-hand sides of the recursion equations are linear $\textup{ACP}_{\epsilon}^{\tau}$-I terms. The set $\mathcal{L}$ of linear $\textup{ACP}_{\epsilon}^{\tau}$-I terms is inductively defined by the following rules:

• •

  $\delta\in\mathcal{L}$;

• •

  if $\phi\in\mathcal{C}$, then $\phi\mathbin{:\rightarrow}\epsilon\in\mathcal{L}$;

• •

  if $\phi\in\mathcal{C}$, $\alpha\in\mathcal{A}_{\tau}$, and $X\in\mathcal{X}$, then $\phi\mathbin{:\rightarrow}\alpha\cdot X\in\mathcal{L}$;

• •

  if $t,t^{\prime}\in\mathcal{L}$, then $t\mathbin{+}t^{\prime}\in\mathcal{L}$.

Let $t\in\mathcal{L}$. Then we refer to the subterms of $t$ that have the form $\phi\mathbin{:\rightarrow}\epsilon$ or the form $\phi\mathbin{:\rightarrow}\alpha\cdot X$ as the summands of $t$.

Let $X$ be a variable from $\mathcal{X}$ and let $t$ be an $\textup{ACP}_{\epsilon}^{\tau}$-I term in which $X$ occurs. Then an occurrence of $X$ in $t$ is guarded if $t$ has a subterm of the form $\alpha\cdot t^{\prime}$ where $\alpha\in\mathcal{A}$ and $t^{\prime}$ contains this occurrence of $X$. An occurrence of a variable $X$ in a linear $\textup{ACP}_{\epsilon}^{\tau}$-I term may not be guarded because a linear $\textup{ACP}_{\epsilon}^{\tau}$-I term may have summands of the form $\phi\mathbin{:\rightarrow}\tau\cdot X$.

A guarded linear recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I is a recursive specification $\{X_{i}=t_{i}\mathrel{\mid}i\in I\}$ over $\textup{ACP}_{\epsilon}^{\tau}$-I where each $t_{i}$ is a linear $\textup{ACP}_{\epsilon}^{\tau}$-I term, and there does not exist an infinite sequence $i_{0}\;i_{1}\;\ldots\,$ over $I$ such that, for each $k\in\mathbb{N}$, there is an occurrence of $X_{i_{k+1}}$ in $t_{i_{k}}$ that is not guarded.

A linearizable recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I is a recursive specification $\{X_{i}=t_{i}\mathrel{\mid}i\in I\}$ over $\textup{ACP}_{\epsilon}^{\tau}$-I where each $t_{i}$ is rewritable to an $\textup{ACP}_{\epsilon}^{\tau}$-I term $t^{\prime}_{i}$, using the axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I in either direction and the equations in $\{X_{j}=t_{j}\mathrel{\mid}j\in I\land i\neq j\}$ from left to right, such that $\{X_{i}=t^{\prime}_{i}\mathrel{\mid}i\in I\}$ is a guarded linear recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I.

A solution of a guarded linear recursive specification $E$ over $\textup{ACP}_{\epsilon}^{\tau}$-I in some model of $\textup{ACP}_{\epsilon}^{\tau}$-I is a set $\{p_{X}\mathrel{\mid}X\in\mathrm{vars}(E)\}$ of elements of the carrier of that model such that each equation in $E$ holds if, for all $X\in\mathrm{vars}(E)$, $X$ is assigned $p_{X}$. A guarded linear recursive specification has a unique solution under the equivalence defined in Section 5 for $\textup{ACP}_{\epsilon}^{\tau}$-I extended with guarded linear recursion. If $\{p_{X}\mathrel{\mid}X\in\mathrm{vars}(E)\}$ is the unique solution of a guarded linear recursive specification $E$, then, for each $X\in\mathrm{vars}(E)$, $p_{X}$ is called the $X$-component of the unique solution of $E$.

$\textup{ACP}_{\epsilon}^{\tau}$-I is extended with guarded linear recursion by adding constants for solutions of guarded linear recursive specifications over $\textup{ACP}_{\epsilon}^{\tau}$-I and axioms concerning these additional constants. For each guarded linear recursive specification $E$ over $\textup{ACP}_{\epsilon}^{\tau}$-I and each $X\in\mathrm{vars}(E)$, a constant $\langle X|E\rangle$ of sort $\mathbf{P}$, that stands for the $X$-component of the unique solution of $E$, is added to the constants of $\textup{ACP}_{\epsilon}^{\tau}$-I. The equation RDP (Recursive Definition Principle) and the conditional equation RSP (Recursive Specification Principle) given in Table 3 are added to the axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I.

In RDP and RSP, $X$ stands for an arbitrary variable from $\mathcal{X}$, $t$ stands for an arbitrary $\textup{ACP}_{\epsilon}^{\tau}$-I term of sort $\mathbf{P}$,  $E$ stands for an arbitrary guarded linear recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I, and the notation $\langle t|E\rangle$ is used for $t$ with, for all $X\in\mathrm{vars}(E)$, all occurrences of $X$ in $t$ replaced by $\langle X|E\rangle$. Side conditions restrict what $X$, $t$ and $E$ stand for.

We write $\textup{ACP}_{\epsilon}^{\tau}$-I+REC for the resulting theory. Furthermore, we write $\mathcal{P}_{\mathit{rec}}$ for the set of all closed $\textup{ACP}_{\epsilon}^{\tau}\textup{-I}\textup{+REC}$ terms of sort $\mathbf{P}$.

RDP and RSP together postulate that guarded linear recursive specifications over $\textup{ACP}_{\epsilon}^{\tau}$-I have unique solutions: the equations $\langle X|E\rangle=\langle t|E\rangle$ and the conditional equations $E\mathrel{\Rightarrow}X\!=\!\langle X|E\rangle$ for a fixed $E$ express that the constants $\langle X|E\rangle$ make up a solution of $E$ and that this solution is the only one, respectively.

Because conditional equational formulas must be dealt with in $\textup{ACP}_{\epsilon}^{\tau}$-I+REC, it is understood that conditional equational logic is used in deriving equations from the axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I+REC. A complete inference system for conditional equational logic can for example be found in [3, 24].

We write $T\vdash t=t^{\prime}$, where $T$ is $\textup{ACP}_{\epsilon}^{\tau}$-I+REC or $\textup{ACP}_{\epsilon}^{\tau}$-I+REC+CFAR (an extension of $\textup{ACP}_{\epsilon}^{\tau}$-I+REC introduced below), to indicate that the equation $t=t^{\prime}$ is derivable from the axioms of $T$ using a complete inference system for conditional equational logic.

The following closed $\textup{ACP}_{\epsilon}^{\tau}$-I+REC term is reminiscent of a program that computes by repeated subtraction the quotient and remainder of dividing a non-negative integer by a positive integer ($i,j,q,r\in\mathcal{V}$):

$$\begin{array}[]{@{}l@{}}[q\mathbin{{:}{=}}0]\cdot[r\mathbin{{:}{=}}i]\cdot\langle Q|E\rangle\;,\end{array}$$

where $E$ is the guarded linear recursive specification that consists of the following two equations ($Q,R\in\mathcal{X}$):

$$\begin{array}[]{@{}l@{}}Q=(r\geq j=\mathsf{t\!t})\mathbin{:\rightarrow}[q\mathbin{{:}{=}}q+1]\cdot R\mathbin{+}(r\geq j=\mathsf{f\!f})\mathbin{:\rightarrow}\epsilon\;,\\ R={\mathsf{t}}\mathbin{:\rightarrow}[r\mathbin{{:}{=}}r-j]\cdot Q\;.\end{array}$$

The final values of $q$ and $r$ are the quotient and remainder of dividing the initial value of $i$ by the initial value of $j$. An evaluation operator can be used to show that this is the case for given initial values of $i$ and $j$. For example, consider the case where the initial values of $i$ and $j$ are $11$ and $3$, respectively. Let $\sigma$ be an evaluation map such that $\sigma(i)=11$ and $\sigma(j)=3$. Then the following equation can be derived from the axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I+REC:

$$\begin{array}[]{@{}l@{}}{\mathsf{V}_{\sigma}}([q\mathbin{{:}{=}}0]\cdot[r\mathbin{{:}{=}}i]\cdot\langle Q|E\rangle)\\ \;{}=[q\mathbin{{:}{=}}0]\cdot[r\mathbin{{:}{=}}11]\cdot[q\mathbin{{:}{=}}1]\cdot[r\mathbin{{:}{=}}8]\cdot[q\mathbin{{:}{=}}2]\cdot[r\mathbin{{:}{=}}5]\cdot[q\mathbin{{:}{=}}3]\cdot[r\mathbin{{:}{=}}2]\;.\end{array}$$

This equation shows that in the case where the initial values of $i$ and $j$ are $11$ and $3$ the final values of $q$ and $r$ are $3$ and $2$ (which are the quotient and remainder of dividing $11$ by $3$).

Below, use will be made of a reachability notion for the variables occurring in a guarded linear recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I.

Let $E$ be a guarded linear recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I and let $X,Y\in\mathrm{vars}(E)$. Then $Y$ is directly reachable from $X$ in $E$, written $X\stackrel{{\scriptstyle E}}{{\leadsto}}Y$, if $Y$ occurs in the right-hand side of the recursion equation for $X$ in $E$. We write $\mathrel{\stackrel{{\scriptstyle E}}{{\leadsto}}^{*}}$ for the reflexive transitive closure of $\stackrel{{\scriptstyle E}}{{\leadsto}}$.

Processes with one or more cycles of $\tau$ actions are not definable by guarded linear recursion alone, but they are definable by combining guarded linear recursion and abstraction. An example is

$$\begin{array}[]{@{}l@{}}{\tau_{\{a\}}}(\langle X|\{X=a\cdot Y\mathbin{+}b,Y=a\cdot X\mathbin{+}c\}\rangle)\;.\end{array}$$

The semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I+REC presented in Section 5 identifies this with $b\mathbin{+}\tau\cdot(b\mathbin{+}c)$. However, the equation

$$\begin{array}[]{@{}l@{}}{\tau_{\{a\}}}(\langle X|\{X=a\cdot Y\mathbin{+}b,Y=a\cdot X\mathbin{+}c\}\rangle)=b\mathbin{+}\tau\cdot(b\mathbin{+}c)\end{array}$$

is not derivable from the axioms of $\textup{ACP}_{\epsilon}^{\tau}$-I+REC. This is remedied by the addition of the equational axiom schema CFAR (Cluster Fair Abstraction Rule) that will be presented below. This axiom schema makes it possible to abstract from a cycle of actions that are turned into the unobservable action $\tau$, by which only the ways out of the cycle remain. The side condition on the equation concerned requires several notions to be made precise.

Let $E$ be a guarded linear recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I, let $C\subseteq\mathrm{vars}(E)$, and let $I\subseteq\mathcal{A}$. Then:

• •

  $C$ is a cluster for $I$ in $E$ if, for each $\textup{ACP}_{\epsilon}^{\tau}$-I term $\phi\mathbin{:\rightarrow}\alpha\cdot X$ of sort $\mathbf{P}$ that is a summand of the right-hand side of the recursion equation for some $X^{\prime}\in C$ in $E$, $X\in C$ only if $\phi\equiv{\mathsf{t}}$ and $\alpha\in I\cup\{\tau\}$;⁶⁶6We write $\equiv$ for syntactic equality.

• •

  for each cluster $C$ for $I$ in $E$, the exit set of $C$ for $I$ in $E$, written $\mathit{exits}_{I,E}(C)$, is the set of $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort $\mathbf{P}$ defined by $t\in\mathit{exits}_{I,E}(C)$ iff $t$ is a summand of the right-hand side of the recursion equation for some $X^{\prime}\in C$ in $E$ and one of the following holds:

  • –

    $t\equiv\phi\mathbin{:\rightarrow}\alpha\cdot Y$ for some $\phi\in\mathcal{C}$, $\alpha\in\mathcal{A}_{\tau}$, and $Y\in\mathrm{vars}(E)$ such that $\alpha\notin I\cup\{\tau\}$ or $Y\notin C$;

  • –

    $t\equiv\phi\mathbin{:\rightarrow}\epsilon$ for some $\phi\in\mathcal{C}$;

• •

  $C$ is a conservative cluster for $I$ in $E$ if $C$ is a cluster for $I$ in $E$ and, for each $X\in C$ and $Y\in\mathit{exits}_{I,E}(C)$, $X\mathrel{\stackrel{{\scriptstyle E}}{{\leadsto}}^{*}}Y$.

The cluster fair abstraction rule is presented in Table 4.

In this table, $X$ stands for an arbitrary variable from $\mathcal{X}$, $E$ stands for an arbitrary guarded linear recursive specification over $\textup{ACP}_{\epsilon}^{\tau}$-I, $I$ stands for an arbitrary subset of $\mathcal{A}$, and $t_{1},t_{2},\ldots\,$ stand for arbitrary $\textup{ACP}_{\epsilon}^{\tau}$-I terms of sort $\mathbf{P}$. A side condition restricts what $X$, $E$, $I$, and $t_{1},t_{2},\ldots\,$ stand for.

CFAR expresses that every cluster of $\tau$ actions will be exited sooner or later. This is a fairness assumption made in the verification of many properties concerning the external behaviour of systems.

We write $\textup{ACP}_{\epsilon}^{\tau}$-I+REC+CFAR for the theory $\textup{ACP}_{\epsilon}^{\tau}$-I+REC extended with CFAR.

In this section, a structural operational semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I+REC is presented and a notion of branching bisimulation equivalence for $\textup{ACP}_{\epsilon}^{\tau}$-I+REC based on this structural operational semantics is defined.

The structural operational semantics of $\textup{ACP}_{\epsilon}^{\tau}$-I+REC consists of

• •

  a binary conditional transition relation $\buildrel{\ell}\over{\hbox to10.41669pt{\rightarrowfill}}$ on $\mathcal{P}_{\mathit{rec}}$ for each $\ell\in\mathcal{E}\!\mathcal{M}\times\mathcal{A}_{\tau}$;

• •

  a unary successful termination relation $\mathrel{{}^{\{\sigma\}}\!{\downarrow}}$ on $\mathcal{P}_{\mathit{rec}}$ for each $\sigma\in\mathcal{E}\!\mathcal{M}$.

We write $t\buildrel{\{\sigma\}\hskip 1.00006pt\alpha}\over{\hbox to26.67787pt{\rightarrowfill}}t^{\prime}$ instead of $(t,t^{\prime})\in{\buildrel{(\sigma,\alpha)}\over{\hbox to24.47777pt{\rightarrowfill}}}$ and $t\mathrel{{}^{\{\sigma\}}\!{\downarrow}}$ instead of $t\in{\mathrel{{}^{\{\sigma\}}\!{\downarrow}}}$.

The relations from the structural operational semantics describe what the processes denoted by terms from $\mathcal{P}_{\mathit{rec}}$ are capable of doing as follows:

• •

  $t\buildrel{\{\sigma\}\hskip 1.00006pt\alpha}\over{\hbox to26.67787pt{\rightarrowfill}}t^{\prime}$: if the data values assigned to the flexible variables are as defined by $\sigma$, then the process denoted by $t$ has the potential to make a transition to the process denoted by $t^{\prime}$ by performing action $\alpha$;

• •

  $t\mathrel{{}^{\{\sigma\}}\!{\downarrow}}$: if the data values assigned to the flexible variables are as defined by $\sigma$, then the process denoted by $t$ has the potential to terminate successfully.