{'fraction_non_alphanumeric': 0.04099628712871287, 'fraction_numerical': 0.0072400990099009905, 'mean_word_length': 3.95447229248103, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 32, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Imperative process algebra with abstraction

This paper introduces an imperative process algebra based on ACP (Algebra of Communicating Processes). Like other imperative process algebras, this process algebra deals with processes of the kind that arises from the execution of imperative programs. It distinguishes itself from already existing imperative process algebras among other things by supporting abstraction from actions that are considered not to be visible. The support of abstraction of this kind opens interesting application possibilities of the process algebra. This paper goes briefly into the possibility of information-flow security analysis of the kind that is concerned with the leakage of confidential data. For the presented axiomatization, soundness and semi-completeness results with respect to a notion of branching bisimulation equivalence are established.


Introduction
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. 1 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 ACP τ ǫ -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 ACP τ ǫ -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 ACP τ ǫ -I. Other imperative process algebras are VPLA [27], IPAL [33], CSP σ [16], AWN [19], and the unnamed process algebra introduced in [13].
ACP τ ǫ -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). ACP τ ǫ -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 ACP τ ǫ -I. Property (2) is achieved by using a notion of branching bisimulation equivalence [41] for the equivalence of processes in the semantics of ACP τ ǫ -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 ACP τ ǫ -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 ACP τ ǫ -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 ACP τ ǫ -I. This paper also shows how ACP τ ǫ -I can be used for information-flow security analysis of the kind that is concerned with the leakage of confidential data.
The development of ACP τ ǫ -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 ACP τ ǫ -I is ACP τ ǫ [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.
ACP τ ǫ -I is closely related to ACP * ǫ -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 ACP τ ǫ -I, guarded linear recursion in the setting of ACP τ ǫ -I. The set of processes that can be defined by means of the operators of ACP τ ǫ -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 ACP τ ǫ -I. Therefore, (a) should be considered the important difference. However, using the semantics of ACP * ǫ -D as presented in [9] as the starting point of the semantics of ACP τ ǫ -I turned out to result in a semantics that is too complicated to establish the soundness and semicompleteness results.
This paper is organized as follows. First, a survey of the algebraic theory ACP τ ǫ , which is the extension of ACP with the empty process constant ǫ and the silent step constant τ , is given (Section 2). Next, the algebraic theory ACP τ ǫ -I is introduced as an extension of ACP τ ǫ (Section 3) and guarded linear recursion in the setting of ACP τ ǫ -I is treated (Section 4). After that, a structural operational semantics of ACP τ ǫ -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 ACP τ ǫ -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 ACP τ ǫ -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 ACP * ǫ -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.

ACP with Empty Process and Silent Step
In this section, ACP τ ǫ is presented. ACP τ ǫ is ACP [6] extended with the empty process constant ǫ and the silent step constant τ as in [3,Section 5.3]. In ACP τ ǫ , it is assumed that a fixed but arbitrary finite set A of basic actions, with τ, δ, ǫ ∈ A, and a fixed but arbitrary commutative and associative communication function γ:(A∪{τ, δ})×(A∪{τ, δ}) → (A∪{τ, δ}), such that γ(τ, a) = δ and γ(δ, a) = δ for all a ∈ A ∪ {τ, δ}, have been given. Basic actions are taken as atomic processes. The function γ is regarded to give the result of synchronously performing any two basic actions for which this is possible, and to be δ otherwise. Henceforth, we write A τ for A ∪ {τ }.
The algebraic theory ACP τ ǫ has one sort: the sort P of processes. This sort is made explicit to anticipate the need for many-sortedness later on. The algebraic theory ACP τ ǫ has the following constants and operators to build terms of sort P: for each a ∈ A, the basic action constant a : P; -the silent step constant τ : P; -the inaction constant δ : P; -the empty process constant ǫ : P; -the binary alternative composition operator + : P × P → P; -the binary sequential composition operator · : P × P → P; -the binary parallel composition operator : P × P → P; -the binary left merge operator ⌊⌊ : P × P → P; -the binary communication merge operator | : P × P → P; -for each H ⊆ A and for H = A τ , the unary encapsulation operator ∂ H : P → P; -for each I ⊆ A, the unary abstraction operator τ I : P → P.
It is assumed that there is a countably infinite set X of variables of sort 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 · binds stronger than all other binary operators and the operator + binds weaker than all other binary operators.
The constants of ACP τ ǫ can be explained as follows (a ∈ A): a denotes the process that performs the observable action a and after that terminates successfully; -τ denotes the process that performs the unobservable action τ and after that terminates successfully; -ǫ denotes the process that terminates successfully without performing any action; -δ denotes the process that cannot do anything, it cannot even terminate successfully.
Let t and t ′ be closed ACP τ ǫ terms denoting processes p and p ′ , respectively, let H ⊆ A or H = A τ , and let I ⊆ A. Then the operators of ACP τ ǫ can be explained as follows: t + t ′ denotes the process that behaves either as p or as p ′ , 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 · t ′ denotes the process that first behaves as p and following successful termination of p behaves as p ′ ; -t t ′ denotes the process that behaves as p and p ′ 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 ′ is performed or a next action of p and a next action of p ′ are performed synchronously -successful termination may take place at any time that both p and p ′ can terminate successfully; -t ⌊⌊ t ′ denotes the same process as t t ′ , except that it starts with performing an action of p; -t | t ′ denotes the same process as t t ′ , except that it starts with performing an action of p and an action of p ′ synchronously; -∂ H (t) denotes the process that behaves the same as p, except that actions from H are blocked from being performed; -τ I (t) denotes the process that behaves the same as p, except that actions from I are turned into the unobservable action τ .
The operators ⌊⌊ and | are of an auxiliary nature. They make a finite axiomatization of ACP τ ǫ possible. The operator ∂ Aτ can also be explained as follows: ∂ Aτ (t) denotes the process that behaves the same as ǫ if t denotes a process that has the option to behave the same as ǫ and it denotes the process that behaves the same as δ otherwise. In [3,Section 5.3], the symbol √ is used instead of ∂ Aτ .
The axioms of ACP τ ǫ are presented in Table 1. In these equations, a, b, and α stand for arbitrary constants of ACP τ ǫ other than ǫ, H stands for an arbitrary subset of A or the set A τ , and I stands for an arbitrary subset of 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 ∂ Aτ (x) · ∂ Aτ (y) in axiom CM1E deserves some explanation. This term is needed to handle successful termination in the presence of ǫ: it stands for the process that behaves the same as ǫ if both x and y stand for a process that has the option to behave the same as ǫ and it stands for the process that behaves the same as δ otherwise.
Notice that there are no operators ∂ H for H ⊂ A τ with τ ∈ H in ACP τ ǫ . If one or more of them were present, the equation α · δ = α would be derivable from the axioms of ACP τ ǫ . In the sequel, the notation n i=1 t i , where n ≥ 1, will be used for rightnested alternative compositions. For each n ∈ N + , 2 the term n i=1 t i is defined by induction on n as follows: In addition, the convention will be used that 0 i=1 t i = δ. 2 We write N + for the set {n ∈ N | n ≥ 1} of positive natural numbers.
In this section, ACP τ ǫ -I, imperative ACP τ ǫ , is presented. This extension of ACP τ ǫ has been inspired by [8]. It extends ACP τ ǫ 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 ACP τ ǫ -I, it is assumed that the following has been given with respect to data: a many-sorted signature Σ D that includes: • a sort D of data and a sort B of booleans; • constants of sort D and/or operators with result sort D; • constants tt and ff of sort B and operators with result sort B; -a minimal algebra D of the signature Σ D in which the carrier of sort B has cardinality 2 and the equation tt = ff does not hold.
We write D for the set of all closed terms over the signature Σ D that are of sort D. The sort 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 V of flexible variables has been given. A flexible variable is a variable whose value may change in the course of a process. 3 Typical examples of flexible variables are the program variables known from imperative programming. An evaluation map is a function from V to D. We write EM for the set of all evaluation maps.
The algebraic theory ACP τ ǫ -I has the following sorts: the sort P of processes, the sort C of conditions, and the sorts from Σ D .
It is assumed that there are countably infinite sets of variables of sort C and D and that the sets of variables of sort P, C, and D are mutually disjoint and disjoint from V.
Below, the constants and operators of ACP τ ǫ -I are introduced. The operators of ACP τ ǫ -I include two variable-binding operators. The formation rules for ACP τ ǫ -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 : S 1 × . . .× S n → S that binds a variable of sort S ′ , t 1 , . . . , t n are terms of sorts S 1 , . . . , S n , respectively, and X is a variable of sort S ′ , then OX(t 1 , . . . , t n ) is a term of sort S.
An extensive formal treatment of the phenomenon of variable-binding operators can be found in [35]. ACP τ ǫ -I has the constants and operators from Σ D to build terms of the sorts from Σ D -which include the sort B and the sort D -and in addition the following constants to build terms of sort D: We write D for the set of all closed ACP τ ǫ -I terms of sort D. Evaluation maps are intended to provide the data values assigned to flexible variables when an ACP τ ǫ -I term of sort D is evaluated. However, in order to fit better in an algebraic setting, they provide closed terms over the signature Σ D that denote those data values instead. The requirement that D is a minimal algebra guarantees that each data value can be represented by a closed term.
ACP τ ǫ -I has the following constants and operators to build terms of sort C: the binary equality operator = : B × B → C; -the binary equality operator = : D × D → C; 4 -the truth constant t : C; -the falsity constant f : C; -the unary negation operator ¬ : C → C; -the binary conjunction operator ∧ : C × C → C; -the binary disjunction operator ∨ : C × C → C; -the binary implication operator ⇒ : C × C → C; -the unary variable-binding universal quantification operator ∀ : C → C that binds a variable of sort D; -the unary variable-binding existential quantification operator ∃:C → C that binds a variable of sort D.
We write C for the set of all closed ACP τ ǫ -I terms of sort C. Each term from C can be taken as a formula of a first-order language with equality of D by taking the flexible variable constants as additional variables of sort D. The flexible variable constants are implicitly taken as additional variables of sort D wherever the context asks for a formula. In this way, each term from C can be interpreted as a formula in D.
ACP τ ǫ -I has the constants and operators of ACP τ ǫ and in addition the following operators to build terms of sort P: the binary guarded command operator :→ : C × P → P; -for each n ∈ N, for each a ∈ A, the n-ary data parameterized action operator a : D × · · · × D n times → P; for each v ∈ V, a unary assignment action operator v:= : D → P; -for each σ ∈ EM, a unary evaluation operator V σ : P → P.
We write P for the set of all closed ACP τ ǫ -I terms of sort P. The same notational conventions are used as before. Infix notation is also used for the additional binary operators. Moreover, the notation [v := e], where v ∈ V and e is a ACP τ ǫ -I term of sort D, is used for the term v := (e). The notation φ ⇔ ψ, where φ and ψ are ACP τ ǫ -I terms of sort C, is used for the term (φ ⇒ ψ) ∧ (ψ ⇒ φ). The axioms of ACP τ ǫ -I (given below) include an equation φ = ψ for each two terms φ and ψ from C for which the formula φ ⇔ ψ holds in D.
Let t be a term from P, φ be a term from C, e 1 , . . . , e n and e be terms from D, and a be a basic action from A. Then the additional operators to build terms of sort P can be explained as follows: the term φ :→ t denotes the process that behaves as the process denoted by t if condition φ holds and as δ otherwise; -the term a(e 1 , . . . , e n ) denotes the process that performs the data parameterized action a(e 1 , . . . , e n ) and after that terminates successfully; the term [v := e] denotes the process that performs the assignment action [v := e], whose intended effect is the assignment of the result of evaluating e to flexible variable v, and after that terminates successfully; -the term V σ (t) denotes the process that behaves the same as the process denoted by t except that each subterm of t that belongs to D is evaluated using the evaluation map σ 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 ACP τ ǫ -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 ∈ V): 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 σ be an evaluation map such that σ(i) = 11 and σ(j) = 3. Then the following equation can be derived from the axioms of ACP τ ǫ -I given below: 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 σ can be extended homomorphically from flexible variables to ACP τ ǫ -I terms of sort D and ACP τ ǫ -I terms of sort C. These extensions are denoted by σ as well. Below, we write σ{e/v} for the evaluation map σ ′ defined by Three subsets of P are defined: In ACP τ ǫ -I, the elements of A are the terms from P that denote the processes that are considered to be atomic. Henceforth, we write A τ for A ∪ {τ } and A τ δ for A ∪ {τ, δ}.
The axioms of ACP τ ǫ -I are the axioms presented in Table 1, on the understanding that α now stands for an arbitrary term from A τ δ , H now stands for an arbitrary subset of A or the set A τ , and I now stands for an arbitrary subset of A, and in addition the axioms presented in Table 2. In the latter table, φ and ψ stand for arbitrary terms from C, e, e 1 , e 2 , . . ., and e ′ , e ′ 1 , e ′ 2 , . . . stand for arbitrary terms from D, v stands for an arbitrary flexible variable from V, σ stands for an arbitrary evaluation map from EM, a, b, and c stand for arbitrary basic actions from A, and α stands for an arbitrary term from A τ δ .
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 gener-alized to the current setting. An equivalent axiomatization is obtained if axiom BED is replaced by the equation α · (φ :→ τ · x) = α · (φ :→ 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 ⊳ u ⊲ y = u :→ x + (¬ u) :→ y. From this defining equation, it follows that u :→ x = x ⊳ u ⊲ δ. In [25], a unary counterpart of the binary guarded command operator is used. This operator can be defined by the equation {u} = u :→ ǫ. From this defining equation, it follows that u :→ x = {u} · x and also that {t} = ǫ and {f} = δ.

ACP τ ǫ -I with Recursion
A closed ACP τ ǫ -I term of sort 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 ACP τ , where E is a recursive specification over ACP τ ǫ -I, for the set of all variables that occur in E. Let E be a recursive specification and let X ∈ vars(E). Then the unique equation Below, recursive specifications over ACP τ ǫ -I are introduced in which the righthand sides of the recursion equations are linear ACP τ ǫ -I terms. The set L of linear ACP τ ǫ -I terms is inductively defined by the following rules: Let t ∈ L. Then we refer to the subterms of t that have the form φ :→ ǫ or the form φ :→ α · X as the summands of t. Let X be a variable from X and let t be an ACP τ ǫ -I term in which X occurs. Then an occurrence of X in t is guarded if t has a subterm of the form α · t ′ where α ∈ A and t ′ contains this occurrence of X. An occurrence of a variable X in a linear ACP τ ǫ -I term may not be guarded because a linear ACP τ ǫ -I term may have summands of the form φ :→ τ · X.
A guarded linear recursive specification over ACP τ ǫ -I is a recursive specification {X i = t i | i ∈ I} over ACP τ ǫ -I where each t i is a linear ACP τ ǫ -I term, and there does not exist an infinite sequence i 0 i 1 . . . over I such that, for each k ∈ N, there is an occurrence of X i k+1 in t i k that is not guarded.
A linearizable recursive specification over ACP τ ǫ -I is a recursive specification {X i = t i | i ∈ I} over ACP τ ǫ -I where each t i is rewritable to an ACP τ ǫ -I term t ′ i , using the axioms of ACP τ ǫ -I in either direction and the equations in {X j = t j | Table 3. Axioms for guarded linear recursion is a guarded linear recursive specification over ACP τ ǫ -I. A solution of a guarded linear recursive specification E over ACP τ ǫ -I in some model of ACP τ ǫ -I is a set {p X | X ∈ vars(E)} of elements of the carrier of that model such that each equation in E holds if, for all X ∈ vars(E), X is assigned p X . A guarded linear recursive specification has a unique solution under the equivalence defined in Section 5 for ACP τ ǫ -I extended with guarded linear recursion. If {p X | X ∈ vars(E)} is the unique solution of a guarded linear recursive specification E, then, for each X ∈ vars(E), p X is called the X-component of the unique solution of E.
ACP τ ǫ -I is extended with guarded linear recursion by adding constants for solutions of guarded linear recursive specifications over ACP τ ǫ -I and axioms concerning these additional constants. For each guarded linear recursive specification E over ACP τ ǫ -I and each X ∈ vars(E), a constant X|E of sort P, that stands for the X-component of the unique solution of E, is added to the constants of ACP τ ǫ -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 ACP τ ǫ -I. In RDP and RSP, X stands for an arbitrary variable from X , t stands for an arbitrary ACP τ ǫ -I term of sort P, E stands for an arbitrary guarded linear recursive specification over ACP τ ǫ -I, and the notation t|E is used for t with, for all X ∈ vars(E), all occurrences of X in t replaced by X|E .
Side conditions restrict what X, t and E stand for.
We write ACP τ ǫ -I+REC for the resulting theory. Furthermore, we write P rec for the set of all closed ACP τ ǫ -I+REC terms of sort P. RDP and RSP together postulate that guarded linear recursive specifications over ACP τ ǫ -I have unique solutions: the equations X|E = t|E and the conditional equations E ⇒ X = X|E for a fixed E express that the constants X|E make up a solution of E and that this solution is the only one, respectively.
Because conditional equational formulas must be dealt with in ACP τ ǫ -I+REC, it is understood that conditional equational logic is used in deriving equations from the axioms of ACP τ ǫ -I+REC. A complete inference system for conditional equational logic can for example be found in [3,24].
We write , to indicate that the equation t = t ′ is derivable from the axioms of T using a complete inference system for conditional equational logic.
The following closed ACP τ ǫ -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 ∈ V): where E is the guarded linear recursive specification that consists of the following two equations (Q, R ∈ X ): 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 σ be an evaluation map such that σ(i) = 11 and σ(j) = 3. Then the following equation can be derived from the axioms of ACP τ ǫ -I+REC: 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 ACP τ ǫ -I. Let E be a guarded linear recursive specification over ACP τ ǫ -I and let X, Y ∈ vars(E). Then Y is directly reachable from X in E, written X E Y , if Y occurs in the right-hand side of the recursion equation for X in E. We write E * for the reflexive transitive closure of E .
Processes with one or more cycles of τ actions are not definable by guarded linear recursion alone, but they are definable by combining guarded linear recursion and abstraction. An example is The semantics of ACP τ ǫ -I+REC presented in Section 5 identifies this with b + τ · (b + c). However, the equation is not derivable from the axioms of ACP τ ǫ -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 τ , 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 ACP τ ǫ -I, let C ⊆ vars(E), and let I ⊆ A. Then: Table 4. Cluster fair abstraction rule is the set of ACP τ ǫ -I terms of sort P defined by t ∈ exits I,E (C) iff t is a summand of the right-hand side of the recursion equation for some X ′ ∈ C in E and one of the following holds: The cluster fair abstraction rule is presented in Table 4. In this table, X stands for an arbitrary variable from X , E stands for an arbitrary guarded linear recursive specification over ACP τ ǫ -I, I stands for an arbitrary subset of A, and t 1 , t 2 , . . . stand for arbitrary ACP τ ǫ -I terms of sort P. A side condition restricts what X, E, I, and t 1 , t 2 , . . . stand for.
CFAR expresses that every cluster of τ 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 ACP τ ǫ -I+REC+CFAR for the theory ACP τ ǫ -I+REC extended with CFAR.

Bisimulation Semantics
In this section, a structural operational semantics of ACP τ ǫ -I+REC is presented and a notion of branching bisimulation equivalence for ACP τ ǫ -I+REC based on this structural operational semantics is defined.
The structural operational semantics of ACP τ ǫ -I+REC consists of a binary conditional transition relation ℓ − → on P rec for each ℓ ∈ EM × A τ ; -a unary successful termination relation {σ} ↓ on P rec for each σ ∈ EM.
The relations from the structural operational semantics describe what the processes denoted by terms from P rec are capable of doing as follows: if the data values assigned to the flexible variables are as defined by σ, then the process denoted by t has the potential to make a transition to the process denoted by t ′ by performing action α; -t {σ} ↓: if the data values assigned to the flexible variables are as defined by σ, then the process denoted by t has the potential to terminate successfully.
The relations from the structural operational semantics of ACP τ ǫ -I+REC are the smallest relations satisfying the rules given in Table 5. In this table, σ and σ ′ stand for arbitrary evaluation maps from EM, α stands for an arbitrary action from A τ , a, b, and c stand for arbitrary actions from A, e, e 1 , e 2 , . . . and e ′ 1 , e ′ 2 , . . . stand for arbitrary terms from D, H stands for an arbitrary subset of A or the set A τ , I stands for an arbitrary subset of A, φ stands for an arbitrary term from C, v stands for an arbitrary flexible variable from V, X stands for an arbitrary variable from X , t stands for an arbitrary ACP τ ǫ -I term of sort P, and E stands for an arbitrary guarded linear recursive specification over ACP τ ǫ -I. The rules in Table 5 have the form p1, . . . , pn c s, where s is optional. They are to be read as "if p 1 and . . . and p n then c, provided s". As usual, p 1 , . . . , p n are called the premises and c is called the conclusion. A side condition s, if present, serves to restrict the applicability of a rule. If a rule has no premises, then nothing is displayed above the horizontal bar.
Because the rules in Table 5 constitute an inductive definition, t can be inferred by applying the first rule, the third rule for +, the second rule for :→, and the third rule for · in that order.
Two processes are considered equal if they can simulate each other insofar as their observable potentials to make transitions and to terminate successfully are concerned, taking into account the assigments of data values to flexible variables under which the potentials are available. This can be dealt with by means of the notion of branching bisimulation equivalence introduced in [41] adapted to the conditionality of transitions in which the unobservable action τ is performed.
For each σ ∈ EM, the binary relation {σ} −−→ → on P rec defined as the reflexive transitive closure of A branching bisimulation is a binary relation R on P rec such that, for all terms t 1 , t 2 ∈ P rec with (t 1 , t 2 ) ∈ R, the following transfer conditions hold: If R is a branching bisimulation, then a pair (t 1 , t 2 ) is said to satisfy the root condition in R if the following conditions hold: Two terms t 1 , t 2 ∈ P rec are rooted branching bisimulation equivalent, written t 1 ↔ rb t 2 , if there exists a branching bisimulation R such that (t 1 , t 2 ) ∈ R and (t 1 , t 2 ) satisfies the root condition in R.
In Section 7, it is proved that ↔ rb is a congruence with respect to the operators of ACP τ ǫ -I+REC of which the result sort and at least one argument sort is P. Without the root condition, ↔ rb would not be a congruence with respect to the operator +. For example, it would be the case that τ · a ↔ rb a and not τ · a + b ↔ rb a + b.
Let R be a branching bisimulation such that (t 1 , t 2 ) ∈ R and the pair (t 1 , t 2 ) satisfies the root condition in R. Then we say that R is a branching bisimulation witnessing t 1 ↔ rb t 2 .

Interlude
In the preceding sections, two relatively uncommon choices have been made: the choice to include the rather unusual evaluation operators, i.e. V σ for each σ ∈ EM, in the operators of ACP τ ǫ -I+REC; -the choice for a structural operational semantics of ACP τ ǫ -I+REC with a transition relation ℓ − → on P rec for each ℓ ∈ EM × A τ , while a transition relation ℓ − → on P rec × EM for each ℓ ∈ A τ is arguably more common.
In this short section, the reasons for these choices are clarified.
The issues which influenced the above-mentioned choices most are: the need for a variant of rooted branching bisimulation equivalence that is a congruence with respect to all operators of ACP τ ǫ -I+REC; the need for a coarser equivalence in cases where parallel composition, left merge, and communication merge are not involved.
With the chosen kind of transition relations, the first need can be fulfilled with a simple and natural generalization of rooted branching bisimulation equivalence as originally introduced in [41], but with the more common kind of transition relations a less obvious variant of rooted branching bisimulation equivalence, a 'stateless' variant in the terminology of [32], has to be devised. As a consequence, with the chosen kind of transition relations, generalizations of existing proof techniques and proof ideas could be used in establishing the soundness and semi-completeness results presented in Section 7, whereas this would not be the case with the more common kind of transition relations.
The variant of rooted branching bisimulation equivalence referred to at the beginning of the previous paragraph is the equivalence ↔ rb introduced at the end of Section 5. In order to be a congruence with respect to parallel composition, left merge, and communication merge, ↔ rb identifies two terms from P rec if the processes denoted by them can simulate each other even in the case where the data values assigned to flexible variables may change after each transitionthrough assignment actions performed by parallel processes. The second need mentioned above is the need for an equivalence that does not takes such changes into account in cases where parallel composition, left merge, and communication merge are not involved. Two terms t, t ′ ∈ P rec are equivalent according to this coarser equivalence iff V σ (t) ↔ rb V σ (t ′ ) for all σ ∈ EM. This means that the coarser equivalence is covered in the semantics of ACP τ ǫ -I+REC by the choice to include the evaluation operators in the operators of ACP τ ǫ -I+REC. We have that, for all t, t ′ ∈ P rec and σ ∈ EM, ACP τ ǫ -I+REC+CFAR ⊢ V σ (t) = V σ (t ′ ) iff V σ (t) ↔ rb V σ (t ′ ) (see Corollary 1 below). So the axioms of ACP τ ǫ -I+REC+CFAR, which constitute an equational axiomatization of ↔ rb , are also adequate for equational verification of the coarser equivalence.
In [25], an extension of ACP with the empty process constant, the unary counterpart of the binary guarded command operator, and actions to change a data-state is presented. Evaluation maps can be taken as special cases of datastates. For similar reasons as in the case of ACP τ ǫ -I+REC, there is a need for two equivalences. This is not dealt with by the inclusion of evaluation operators. Instead, in equational reasoning, certain axioms may only be applied to terms in which the parallel composition, left merge, and communication merge operators do not occur.
In an appendix, a structural operational semantics of ACP τ ǫ -I+REC is presented which is reminiscent of a symbolic operational semantics in the sense of [28]. It is a structural operational semantics with a transition relation ℓ − → on P rec for each ℓ ∈ C sat × A τ , where C sat is the set of all terms φ ∈ C for which D |= φ ⇔ f. In my opinion, this structural operational semantics is intuitively more appealing than the one presented in Section 5, but the definition of the variant of rooted branching bisimulation equivalence based on it is quite unintelligible.

Soundness and Completeness
In this section, soundness and (semi-)completeness results with respect to branching bisimulation equivalence for the axioms of ACP τ ǫ -I+REC+CFAR are presented.
Firstly, rooted branching bisimulation equivalence is an equivalence relation indeed.
Proposition 1 (Equivalence). The relation ↔ rb is an equivalence relation.
Proof. It must be shown that ↔ rb is reflexive, symmetric, and transitive.
Let t ∈ P rec . Then the identity relation I on P rec is a branching bisimulation such that (t, t) ∈ I and (t, t) satisfies the root condition in I. Hence, t ↔ rb t, which proves that ↔ rb is reflexive.
Let t 1 , t 2 ∈ P rec be such that t 1 ↔ rb t 2 , and let R be a branching bisimulation such that (t 1 , t 2 ) ∈ R and (t 1 , t 2 ) satisfies the root condition in R. Then R −1 is a branching bisimulation such that (t 2 , t 1 ) ∈ R −1 and (t 2 , t 1 ) satisfies the root condition in R −1 . Hence, t 2 ↔ rb t 1 , which proves that ↔ rb is symmetric.
Let t 1 , t 2 , t 3 ∈ P rec be such that t 1 ↔ rb t 2 and t 2 ↔ rb t 3 , let R be a branching bisimulation such that (t 1 , t 2 ) ∈ R and (t 1 , t 2 ) satisfies the root condition in R, and let S be a branching bisimulation such that (t 2 , t 3 ) ∈ S and (t 2 , t 3 ) satisfies the root condition in S. Then R • S is a branching bisimulation such that (t 1 , t 3 ) ∈ R • S and (t 1 , t 3 ) satisfies the root condition in R • S. 7 That R • S is a branching bisimulation is proved in the same way as Proposition 7 in [4]. Hence, t 1 ↔ rb t 3 , which proves that ↔ rb is transitive.
⊓ ⊔ Moreover, rooted branching bisimulation equivalence is a congruence with respect to the operators of ACP τ ǫ -I+REC of which the result sort and at least one argument sort is P. Proposition 2 (Congruence). For all terms t 1 , t ′ 1 , t 2 , t ′ 2 ∈ P rec and all terms φ ∈ C, t 1 ↔ rb t 2 and t ′ 1 Proof. A detailed proof would contain an adapted copy of at least ten pages from [23]. Therefore, only an outline of the proof is given here. In order to fully understand the outline, the above-mentioned paper must be consulted.
In [23], an SOS rule format is presented which guarantees that the 'standard' version of branching bisimulation equivalence is a congruence. The format concerned is called the RBB safe format. Below, this format is adapted in order to deal with a set of transition labels that contains a special element {σ} τ for each σ ∈ EM instead of a single special element τ and with a slightly different version of branching bisimulation equivalence. A definition of a patience rule is needed that differs from the one given in [23]: a patience rule for the ith argument of an n-ary operator f is a path rule of the form where σ ∈ EM. The RBB safe format is adapted by making the following changes to the definition of the RBB safe format as given in [23]: in the two syntactic restrictions of the RBB safe format that concern wild arguments, the phrase "a patience rule" is changed to "a patience rule for each σ ∈ EM"; -in the second syntactic restrictions of the RBB safe format that concern wild arguments, the phrase "the relation τ − →" is changed to "the relation It is straightforward to check that the proof of Theorem 3.4 from [23] goes through for the adapted RBB safe format and the version of branching bisimulation equivalence considered in this paper. This means that the proposition holds if the rules in Table 5 are in the adapted RBB safe format with respect to some tame/wild labeling of arguments of operators. It is easy to verify that this is the case with the following tame/wild labeling: both arguments of + are tame, the first argument of · is wild and the second argument of · is tame, both arguments of are wild, both arguments of ⌊⌊ and | are tame, the argument of ∂ H and τ I is wild, the second argument of :→ is tame, and the argument of V σ is wild.

⊓ ⊔
The tame/wild labeling given at the end of the proof of Proposition 2 is provided so that the reader who consults [23] can easily check that the rules in Table 5 are in the adapted RBB safe format. Below, the soundness of the axiom system of ACP τ ǫ -I+REC+CFAR with respect to ↔ rb for equations between terms from P rec will be established.
The following terminology will be used in the soundness proof: (a) an equation eq of ACP τ ǫ -I+REC terms of sort P is said to be valid with respect to ↔ rb if, for each closed substitution instance t = t ′ of eq, t ↔ rb t ′ and (b) a conditional equation ceq of ACP τ ǫ -I+REC terms of sort P is said to be valid with respect to ↔ rb if, for each closed substitution instance Theorem 1 (Soundness). For all terms t, t ′ ∈ P rec , t = t ′ is derivable from the axioms of ACP τ ǫ -I+REC+CFAR only if t ↔ rb t ′ .
Proof. Because ↔ rb is a congruence with respect to all operators from the signature of ACP τ ǫ -I+REC+CFAR, only the validity of each axiom of ACP τ ǫ -I+REC+CFAR has to be proved.
Below, we write csi (eq), where eq is an equation of ACP τ ǫ -I+REC terms of sort P, for the set of all closed substitution instances of eq. Moreover, we write R id for the identity relation on P rec .
For each axiom ax of ACP τ ǫ -I+REC+CFAR, a rooted branching bisimulation R ax witnessing the validity of ax can be constructed as follows: if ax is one of the axioms A7, CM2E, CM5E, CM6E, GC2 or an instance of one of the axiom schemas D0, D2, T0, GC3, V0, CM7Db-CM7Df: if ax is one of the axioms A1-A6, A8, A9, CM4, CM8-CM9, GC1 or an instance of one of the axiom schemas CM3, CM7, D1, D3, D4, T1-T4, GC4-GC12, V1-V6, CM7Da, RDP: if ax is CM1E: if ax is an instance of BE: where C is the finite conservative cluster for I in E such that X ∈ C and exits I, of RSP: where Θ is the set of all functions from X to P rec and θ(t), where θ ∈ Θ and t ∈ P rec , stands for t with, for all X ∈ X , all occurrences of X replaced by θ(X).
For each equational axiom ax of ACP τ ǫ -I+REC+CFAR, it is straightforward to check that the constructed relation R ax is a branching bisimulation witnessing, for each closed substitution instance t = t ′ of ax , t ↔ rb t ′ . For each conditional equational axiom ax of ACP τ ǫ -I+REC+CFAR, i.e. for each instance of RSP, it is straightforward to check that the constructed relation R ax is a branching bisimulation witnessing, for each closed substitution instance The axioms of ACP τ ǫ -I+REC+CFAR are incomplete with respect to ↔ rb for equations between terms from P rec and there is no straightforward way to rectify this. Below two semi-completeness results are presented. The next two lemmas are used in the proofs of those results.
A term t ∈ P rec is called abstraction-free if no abstraction operator occurs in t. A term t ∈ P rec is called bool-conditional if, for each φ ∈ C that occurs in t,

Lemma 1.
For all abstraction-free t ∈ P rec , there exists a guarded linear recursive specification E and X ∈ vars(E) such that ACP τ ǫ -I+REC ⊢ t = X|E .
Proof. This is easily proved by structural induction on t. The proof involves constructions of guarded linear recursive specifications from guarded linear recursive specifications for the operators of ACP τ ǫ -I other than the abstraction operators. For the greater part, the constructions are reminiscent of operations on process graphs defined in Sections 2.7 and 4.5.5 from [3].
⊓ ⊔ Lemma 2. For all bool-conditional t ∈ P rec , there exists a guarded linear recursive specification E and X ∈ vars(E) such that ACP τ ǫ -I+REC+CFAR ⊢ t = X|E .
Proof. This is also proved by structural induction on t. The cases other than the case where t is of the form τ I (t ′ ) are as in the proof of Lemma 1. The case where t is of the form τ I (t ′ ) is the difficult one. It is proved in the same way as it is done for ACP τ +REC+CFAR in the proof of Theorem 5.6.2 from [22]. ⊓ ⊔ The difficult case of the proof of Lemma 2 is the only case in which an application of CFAR is involved.
The following two theorems are the semi-completeness results referred to above.
Theorem 2 (Semi-completeness I). For all abstraction-free t, t ′ ∈ P rec , Proof. Because of Lemma 1, Theorem 1, and Proposition 1, it suffices to prove that, for all guarded linear recursive specifications E and E ′ with X ∈ vars(E) and X ′ ∈ vars(E ′ ), ACP τ ǫ -I+REC ⊢ X|E = X ′ |E ′ if X|E ↔ rb X ′ |E ′ . This is proved in the same way as it is done for ACP τ +REC in the proof of Theorem 5.3.2 from [22]. ⊓ ⊔ Theorem 3 (Semi-completeness II). For all bool-conditional t, t ′ ∈ P rec , Proof. Because of Lemma 2, Theorem 1, and Proposition 1, it suffices to prove that, for all guarded linear recursive specifications E and E ′ with X ∈ vars(E) and X ′ ∈ vars(E ′ ), ACP τ ǫ -I+REC+CFAR ⊢ X|E = X ′ |E ′ if X|E ↔ rb X ′ |E ′ . This is proved in the same way as it is done for ACP τ +REC in the proof of Theorem 5.3.2 from [22].
⊓ ⊔ It is due to sufficiently similar shapes of linear ACP τ ǫ -I terms and linear ACP τ terms that parts of the proof of Theorems 2 and 3 go in the same way as parts of proofs from [22]. It needs mentioning here that, the body of the proof of Theorem 5.3.2 from [22] is restricted to constants X|E where E does not contain equations Y = τ + . . . + τ with Y ≡ X. The corresponding part of the proof of Theorems 2 and 3 is likewise restricted to constants X|E where E does not contain equations Y = φ 1 :→ τ + . . . + φ n :→ τ with Y ≡ X. This is not because such an equation can be eliminated, but because it can be replaced by The following is a corollary of Theorems 1 and 3.

Information-Flow Security
In this section, it will be explained how ACP τ ǫ -I can be used for information-flow security analysis of the kind that is concerned with the leakage of confidential data. However, first, a general idea is given of what information-flow security is about and what results have been produced by research on this subject.
Consider a program whose variables are partitioned into high-security variables and low-security variables. High-security variables are considered to contain confidential data and low-security variables are considered to contain nonconfidential data. The information flow in the program is called secure if information derivable from data contained in the high-security variables cannot be inferred from data contained in the low-security variables. Secure information flow means that no confidential data is leaked. A well-known program property that guarantees secure information flow is non-interference. In the case where the program is a deterministic sequential program, non-interference is the property that the data initially contained in high security variables has no effect on the data finally contained in low security variables.
Theoretical work on information-flow security is already done since the 1970s (see e.g. [5,17,18,14,15]). A great part of the work done until now has been done in a programming-language setting. This work has among other things led to security-type systems for programming languages. The languages concerned vary from languages supporting sequential programming to languages supporting concurrent programming and from languages for programming transformational systems to languages for programming reactive systems (see e.g. [42,40,12,34,10]).
However, work on information-flow security has also been done in a processalgebra setting. In such a setting, the information flow in a process is generally called secure if information derivable from confidential actions cannot be inferred from non-confidential actions (see e.g. [20,36,11,31]). So, in a process-algebra setting, secure information flow usually means that no confidential action is revealed. Moreover, in such a setting, non-interference is the property that the confidential actions have no effect on the non-confidential actions. Recently, 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]). ACP τ ǫ -I obviates the need to mimic program variables.
In the rest of this section, the interest is in processes that are carried out by systems that have a state comprising a number of data-containing components whose content can be looked up and changed. Moreover, the attention is focussed on processes, not necessarily arising from the execution of a program, in which (a) confidential and non-confidential data contained in the state components of the system in question are looked up and changed and (b) an ongoing interaction with the environment of the system in question is maintained where data are communicated in either direction. In the terminology of ACP τ ǫ -I, the state components are called flexible variables. From now on, processes of the kind described above are referred to as processes of the type of interest. The processes that are carried out by many contemporary systems are covered by the processes of the type of interest.
The point of view is taken that the information flow in a process of the type of interest is secure if information derivable from the confidential data contained in state components cannot be inferred from its interaction with the environment. A process property that guarantees secure information flow in this sense is the property that the confidential data contained in state components has no effect on the interaction with the environment. This property, which will be made more precise below, is called the DNII (Data Non-Interference with Interactions) property. For a process with this property, differences in the confidential data contained in state components cannot be observed in (a) what remains of the process in the case where only the actions that are performed to interact with the environment are visible and (b) consequently in the data communicated with the environment.
For each closed ACP τ ǫ -I+REC term P of sort P that denotes a process of the type of interest, it is assumed that the following has been given: a set Low P ⊆ V of low-security flexible variables of P ; -a set Ext P ⊆ A ∪ n∈N + {a(e 1 , . . . , e n ) | a ∈ A ∧ e 1 , . . . , e n ∈ D} of external actions of P .
For each closed ACP τ ǫ -I+REC term P of sort P that denotes a process of the type of interest, we define the following sets: High P is called the set of high-security flexible variables of P and Int P is called the set of internal actions of P . The flexible variables in Low P are the flexible variables of P that contain non-confidential data and the flexible variables in High P are the flexible variables of P that contain confidential data. The actions in Ext P are the actions that are performed by P to interact with the environment and the actions in Int P are the actions that are performed by P to do something else than to interact with the environment. The actions in Int P are considered to be invisible in the environment. In earlier work based on a purely action-oriented notion of secure information flow, the actions in Ext P and Int P are called low-security actions and high-security actions, respectively, or something similar.
For each closed ACP τ ǫ -I+REC term P of sort P that denotes a process of the type of interest, P has the DNII property iff for all evaluation maps σ and σ ′ such that σ(v) = σ ′ (v) for all v ∈ Low P . This definition is justified by the fact, which follows from Corollary 1, that The left-hand side and the right-hand side of the equation in the above definition denote the processes that remain of the process denoted by P in the case that the data values assigned to the flexible variables are initially as defined by σ and σ ′ , respectively, and moreover all internal actions of P are not visible. The condition imposed on the evaluation maps σ and σ ′ tells us that the equation must always hold if, for each low-security flexible variable of P , the data values assigned to it according to σ and σ ′ are the same. This corresponds to the intuitive idea mentioned above that, for a process with the DNII property, differences in the confidential data cannot be observed in what remains of the process in the case where only the actions that are performed to interact with the environment are visible.
Assume that h, l ∈ V and a, b ∈ A. Let P be the closed ACP τ ǫ -I+REC term of sort P with Low P = {l} and Ext P = {a, b}. P is a very simple example of a term of which it may not be immediately clear that it denotes a process that does not have the DNII property. Notice that, by definition, h ∈ High P and [l := l + 1] ∈ Int P . When [l := l + 1] is performed, this cannot be observed in the externally observable process because [l := l + 1] is an internal action. This means that, irrespective of the value that is initially assigned to h, the externally observable process performs either a or b and after that terminates successfully. This is why the process denoted by P may seem to have the DNII property. However, at the point that the externally observable process has the option to perform a, it has also the option to perform b in the case where the value initially assigned to h is not 0, while it does not have also the option to perform b in the case where the value initially assigned to h is 0. In other words, the externally observable process in the former case differs from the externally observable process in the latter case. This means that, whether or not 0 is initially assigned to h can be inferred from the externally observable process. Hence, the informal conclusion is that P denotes a process that does not have the DNII property. More formally, this conclusion follows from the definition of the DNII property: we have for all evaluation maps σ such that σ(h) = 0 and we have for all evaluation maps σ ′ such that σ ′ (h) = 0, but we do not have In CSP σ [16], presumably the only imperative process algebra that supports abstraction from actions that are considered not to be visible, the DNII property cannot be defined. The cause of this is that abstraction from actions that are considered not to be visible means in CSP σ that these actions are simply removed. Because of that processes such as τ Int P (V σ (P )) and τ Int P (V σ ′ (P )) from the example given above are equated.
Assume that h, l ∈ V and a, b ∈ A. Let Q be the closed ACP τ ǫ -I+REC term of sort P with Low Q = {l} and Ext Q = {a, b}. Q is a very simple example of a term that denotes a process that has the DNII property. This follows from the definition of the DNII property: we have for all evaluation maps σ such that σ(h) = 0, we have for all evaluation maps σ ′ such that σ ′ (h) = 0, and we trivially have The DNII property is only one of the process properties related to information flow security that can be defined and verified in ACP τ ǫ -I+REC+CFAR. Insofar as information flow security of contemporary systems is concerned, it seems to be an essential property. The DNII property is also one of the process properties related to information flow security that cannot be defined naturally in the process algebras used in earlier work on information flow security (cf. [20,36,11,31]). The problem with those process algebras is that state components must be mimicked by processes in them.
The DNII property concerns the non-disclosure of confidential data, contained in state components of a system, through the possibly ongoing interaction of the system concerned with its environment. To my knowledge, such a property has not been proposed in the literature on information-flow security before. However, the DNII property is reminiscent of the combination of data non-interference and event non-interference as defined in [37], but a comparison is difficult to make because of rather different semantical bases.

Concluding Remarks
I have introduced an ACP-based imperative process algebra. This process algebra distinguishes itself from imperative process algebras such as VPLA [27], IPAL [33], CSP σ [16], AWN [19], and the process algebra proposed in [13] by 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; (3) it offers the possibility of equational verification of process equivalence.
Properties (1)-(3) have been achieved by the inclusion of the silent step constant τ and the abstraction operators τ I in the constants and operators of the process algebra, the use of the rooted branching bisimulation equivalence relation ↔ rb for the equivalence of processes in its semantics, and the provision of the equational axiomatization of ↔ rb .
The axioms of the presented imperative process algebra are not complete with respect to the equivalence of processes in its semantics. There is no straightforward way to rectify this. However, two semi-completeness results that may be relevant to various applications of this imperative process algebra have been established. One of those results is at least relevant to information-flow security analysis. The finiteness and linearity restrictions on guarded recursive specifications are not needed for the uniqueness of solutions. However, there would be no semi-completeness results without these restrictions.
In this paper, I build on earlier work on ACP. The axioms of ACP τ ǫ have been taken from Section 5.3 of [3] and the axioms for the guarded command operator have been taken from [2]. The evaluation operators have been inspired by [7] and the data parameterized action operators have been inspired by [8].

Appendix: Alternative Bisimulation Semantics
In this appendix, an alternative to the structural operational semantics of ACP τ ǫ -I+REC is presented and a definition of rooted branching bisimulation equivalence for ACP τ ǫ -I+REC based on this alternative structural operational semantics is given. This appendix is strongly based on Section 4 of [9].
We write C sat for the set of all terms φ ∈ C for which D |= φ ⇔ f. As formulas of a first-order language with equality of D, the terms from C sat are the formulas that are satisfiable in D.
The alternative structural operational semantics of ACP τ ǫ -I+REC consists of a binary conditional transition relation ℓ − → on P rec for each ℓ ∈ C sat × A τ ; -a unary successful termination relation {φ} ↓ on P rec for each φ ∈ C sat .
The relations from this structural operational semantics describe what the processes denoted by terms from P rec are capable of doing as follows: if condition φ holds for the process denoted by t, then this process has the potential to make a transition to the process denoted by t ′ by performing action α; -t {φ} ↓: if condition φ holds for the process denoted by t, then this process has the potential to terminate successfully.
The relations from this structural operational semantics of ACP τ ǫ -I+REC are the smallest relations satisfying the rules given in Table 6. In this table, α stands for an arbitrary action from A τ , φ and ψ stand for arbitrary terms from C sat , a, b, and c stand for arbitrary basic actions from A, e, e 1 , e 2 , . . . and e ′ 1 , e ′ 2 , . . . stand for arbitrary terms from D, H stands for an arbitrary subset of A or the set A τ , I stands for an arbitrary subset of A, σ stands for an arbitrary evaluation map from EM, v stands for an arbitrary flexible variable from V, X stands for an arbitrary variable from X , t stands for an arbitrary ACP τ ǫ -I term of sort P, and E stands for an arbitrary guarded linear recursive specification over ACP τ ǫ -I. The alternative structural operational semantics is such that the structural operational semantics presented in Section 5 can be obtained by replacing each transition t Two processes are considered equal if they can simulate each other insofar as their observable potentials to make transitions and to terminate successfully are concerned. In the case of the alternative structural operational semantics, there are two issues that together complicate matters: simply relating a single transition of one of the processes to a single transition of the other process does not work because a transition of one process may be simulated by a set of transitions of another process; Table 6. Transition rules for ACP τ ǫ -I simply ignoring all transitions in which the unobservable action τ is performed does not work because the observable potentials to make transitions and to terminate successfully may change by such transitions.
The first issue is illustrated by the processes denoted by φ ∨ ψ :→ a and φ :→ a + ψ :→ a: the only transition of the former process is simulated by the two transitions of the latter process. The second issue is illustrated by the processes denoted by a + τ · b and a + b: by making the transition in which the unobservable action τ is performed, the former process loses the potential to make the transition in which the observable action a is performed before anything has been observed, whereas this potential is a potential of the latter process so long as nothing has been observed. The first issue alone can be dealt with by means of the notion of splitting bisimulation equivalence introduced in [7] and the second issue alone can be dealt with by means of the notion of branching bisimulation equivalence introduced in [41] adapted to the conditionality of transitions in which the unobservable action τ is performed. In order to deal with both issues, the two notions are combined.
In the absence of the constant τ , rooted ab-bisimulation equivalence is essentially the same as splitting bisimulation equivalence as defined in [7]. In the absence of all terms of sort C other than the constants t and f, rooted abbisimulation equivalence is essentially the same as rooted branching bisimulation equivalence as defined in [41].
I conjecture that, for all terms t 1 , t 2 ∈ P rec , t 1 ↔ rb t 2 iff t 1 ↔ rab t 2 .