On Finite Bases for Weak Semantics: Failures versus Impossible Futures^{⋆}

Taolue Chen^{1}, Wan Fokkink^{1,2} & Rob van Glabbeek^{3,4}

1 CWI, Department of Software Engineering, PO Box 94079, 1090 GB Amsterdam, The Netherlands 2 Vrije Universiteit Amsterdam, Department of Theoretical Computer Science, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands 3 National ICT Australia, Locked Bag 6016, Sydney, NSW 1466, Australia 4 The University of New South Wales, School of Computer Science and Engineering, Sydney, NSW 2052, Australia

Abstract. We provide a finite basis for the (in)equational theory of the process algebra BCCS modulo the weak failures preorder and equivalence. We also give positive and negative results regarding the axiomatizability of BCCS modulo weak impossible futures semantics.

1 Introduction

Labeled transition systems constitute a widely used model of concurrent computation. They model processes by explicitly describing their states and their transitions from state to state, together with the actions that produce these transitions. Several notions of behavioral semantics have been proposed, with the aim to identify those states that afford the same observations [14, 12]. For equational reasoning about processes, one needs to find an axiomatization that is sound and ground-complete modulo the semantics under consideration, meaning that all equivalent closed terms can be equated. Ideally, such an axiomatization is also ω-complete, meaning that all equivalent open terms can be equated. If such a finite axiomatization exists, it is said that there is a finite basis for the equational theory.

For concrete semantics, so in the absence of the silent action τ, the existence of finite bases is well-studied [16, 14, 7], in the context of the process algebra BCCSP, containing the basic process algebraic operators from CCS and CSP. However, for weak semantics, that take into account the τ, hardly anything is known on finite bases. In [12], Van Glabbeek presented a spectrum of weak semantics. For several of the semantics in this spectrum, a sound and ground-complete axiomatization has been given, in the setting of the process algebra BCCS (BCCSP extended by τ), see, e.g., [13]. But a finite basis has been given only for weak, delay, η- and branching bisimulation semantics [18, 11], and in case of an infinite alphabet of actions also for weak impossible futures semantics [22]. The reason for this lack of results on finite bases, apart from the inherent difficulties arising with weak semantics, may be that it is usually not so straightforward

⋆ This work is partially supported by the Dutch Bsik project BRICKS.

to define a notion of unique normal form for open terms in a weak semantics. Here we will employ a saturation technique, in which normal forms are saturated with subterms.

In this paper, we focus on two closely related weak semantics, based on failures and impossible futures. A weak failure consists of a trace a_{1} ⋯ a_{n} and a set A, both of concrete actions. A state exhibits this weak failure pair if it can perform the trace a_{1} ⋯ a_{n} (possibly intertwined with τ’s) to a state that cannot perform any action in A (even after performing τ’s). In a weak impossible future, A can be a set of traces. Weak failures semantics plays an essential role for the process algebra CSP [3]. For convergent processes, it coincides with testing semantics [8, 19], and thus is the coarsest congruence for the CCS parallel composition that respects deadlock behavior. Weak impossible futures semantics [21] is a natural variant of possible futures semantics [20]. In [15] it is shown that weak impossible futures semantics, with an additional root condition, is the coarsest congruence containing weak bisimilarity with explicit divergence that respects deadlock/livelock traces (or fair testing, or any liveness property under a global fairness assumption) and assigns unique solutions to recursive equations.

The heart of our paper is a finite basis for the inequational theory of BCCS modulo the weak failures preorder. The axiomatization consists of the standard axioms A1-4 for bisimulation, three extra axioms WF1-3 for failures semantics, and in case of a finite alphabet A, an extra axiom WF_{A}. The proof that A1-4 and WF1-3 are a finite basis in case of an infinite alphabet is a sub-proof of the proof that A1-4, WF1-3 and WF_{A} are a finite basis in case of a finite alphabet. Our proof has the same general structure as the beautiful proof for testing equivalences given in [8] and further developed in [17]. Pivotal to this is the construction of “saturated” sets of actions within a term [8]. Since here we want to obtain an ω-completeness result, we extend this notion to variables. Moreover, to deal with ω-completeness, we adopt the same general proof structure as in the strong case [9]. In this sense, our proof strategy can be viewed as a combination of the strategies proposed in [8] and [9]. Furthermore, we apply an algorithm from [2, 10, 6] to obtain a finite basis for BCCS modulo weak failures equivalence for free.

At the end, we investigate the equational theory of BCCS modulo weak impossible futures semantics. This shows a remarkable difference with weak failures semantics, in spite of the strong similarity between the definitions of these semantics (and between their ground-complete axiomatizations). As said, in case of an infinite alphabet, BCCS modulo the weak impossible futures preorder has a finite basis [22]. However, we show that in case of a finite alphabet, such a finite basis does not exist. Moreover, in case of weak impossible futures equivalence, there is no finite ground-complete axiomatization, regardless of the cardinality of the alphabet.

A finite basis for the equational theory of BCCSP modulo (concrete) failures semantics was given in [9]. The equational theory of BCCSP modulo (concrete) impossible futures semantics is studied in [4]. It is interesting to see that our results for weak semantics agree with their concrete counterparts, with very similar proofs. This raises a challenging open question: can one establish a general theorem to link the axiomatizability (or nonaxiomatizability) of concrete and weak semantics?

Due to space restriction, some proofs, remarks and examples are omitted in the current paper. These include, in particular, proofs of Lemmas 1 and 3 and Theorems 5 and 6. However, they can be found in the full version of this paper [5].

2 Preliminaries

BCCS(A) is a basic process algebra for expressing finite process behavior. Its signature consists of the constant 0, the binary operator + , and unary prefix operators τ and a , where a is taken from a nonempty set A of visible actions, called the alphabet, ranged over by a, b, c. We assume that τ ∉ A and write A_{τ} for A ∪ {τ}, ranged over by α, β.

t ::= 0 | at | τt | t + t | x

Closed BCCS(A) terms, ranged over by p, q, represent finite process behaviors, where 0 does not exhibit any behavior, p + q offers a choice between the behaviors of p and q, and αp executes action α to transform into p. This intuition is captured by the transition rules below. They give rise to A_{τ} -labeled transitions between closed BCCS terms.

\overline{αx →^{α} x}  \frac{x →^{α} x′}{x + y →^{α} x′}  \frac{y →^{α} y′}{x + y →^{α} y′}

We assume a countably infinite set V of variables; x, y, z denote elements of V. Open BCCS terms, denoted by t, u, v, may contain variables from V. Write var (t) for the set of variables occurring in t. The operational semantics is extended verbatim to open terms; variables generate no transition. We write t ⇒ u if there is a sequence of τtransitions t →^{τ} ⋯ →^{τ} u; furthermore t →^{α} denotes that there is a term u with t →^{α} u, and likewise t ⇒→^{α} denotes that there are a terms u, v with t ⇒ u →^{α} v.

The depth of a term t, denoted by |t|, is the length of the longest trace of t, not counting τ-transitions. It is defined inductively as follows: |0| = |x| = 0; |at| = 1+|t|; |τt| = |t|; |t + u| = max{|t|, |u|}.

A (closed) substitution, ranged over by σ, ρ, maps variables in V to (closed) terms. For open terms t and u, and a preorder ⊑ (or equivalence ≡) on closed terms, we define t ⊑ u (or t ≡ u) if σ(t) ⊑ σ(u) (resp. σ(t) ≡ σ(u)) for all closed substitutions σ. Clearly, t →^{a} t′ implies that σ(t) →^{a} σ(t′) for all substitutions σ.

An axiomatization is a collection of equations t ≈ u or of inequations t ≼ u. The (in)equations in an axiomatization E are referred to as axioms. If E is an equational axiomatization, we write E ⊢ t ≈ u if the equation t ≈ u is derivable from the axioms in E using the rules of equational logic (reflexivity, symmetry, transitivity, substitution, and closure under BCCS contexts). For the derivation of an inequation t ≼ u from an inequational axiomatization E, denoted by E ⊢ t ≼ u, the rule for symmetry is omitted. We will also allow equations t ≈ u in inequational axiomatizations, as an abbreviation of t ≼ u ∧ u ≼ t.

An axiomatization E is sound modulo a preorder ⊑ (or equivalence ≡) if for all terms t, u, from E ⊢ t ≼ u (or E ⊢ t ≈ u) it follows that t ⊑ u (or t ≡ u). E is groundcomplete for ⊑ (or ≡) if p ⊑ q (or p ≡ q) implies E ⊢ p ≼ q (or E ⊢ p ≈ q) for all closed terms p, q. Moreover, E is ω-complete if for all terms t, u with E ⊢ σ(t) ≼ σ(u) (or E ⊢ σ(t) ≈ σ(u)) for all closed substitutions σ, we have E ⊢ t ≼ u (or E ⊢ t ≈ u). When E is ω-complete as well as ground-complete, it is complete for ⊑ (or ≡) in the sense that t ⊑ u (or t ≡ u) implies E ⊢ t ≼ u (or E ⊢ t ≈ u) for all terms t, u. The equational theory of BCCS modulo a preorder ⊑ (or equivalence ≡) is said to be finitely based if there exists a finite, ω-complete axiomatization that is sound and ground-complete for BCCS modulo ⊑ (or ≡).

A1-4 below are the core axioms for BCCS modulo bisimulation semantics. We write t = u if A1-4 ⊢ t ≈ u.

\begin{aligned}A1 & x + y & ≈ & y + x \\ A2 & (x + y) + z & ≈ & x + (y + z) \\ A3 & x + x & ≈ & x \\ A4 & x + 0 & ≈ & x \end{aligned}

Summation ∑_{i∈{1,...,n}} t_{i} denotes t_{1} + ⋯ + t_{n}, where summation over the empty set denotes 0. As binding convention, + and summation bind weaker than α . For every term t there exists a finite set {α_{i}t_{i} | i ∈ I} of terms and a finite set Y of variables such that t = ∑_{i∈I} α_{i}t_{i} + ∑_{y∈Y} y. The α_{i}t_{i} for i ∈ I and the y ∈ Y are called the summands of t. For a set of variables Y, we will often denote the term ∑_{y∈Y} y by Y.

Definition 1 (Initial actions). For any term t, the set I(t) of initial actions is defined

as I(t) = {a ∈ A | t ⇒→^{a}}.

Definition 2 (Weak failures).

– A pair (a_{1} ⋯ a_{k}, B), with k ≥ 0 and B ⊆ A, is a weak failure pair of a process p_{0}

if there is a path p_{0} ⇒→^{a_{1}}⇒ ⋯ ⇒→^{a_{k}}⇒ p_{k} with I(p_{k}) ∩ B = ∅.

– Write p ≤_{WF} q if the weak failure pairs of p are also weak failure pairs of q.

– The weak failures preorder ⊑_{WF} is given by p ⊑_{WF} q iff (1) p ≤_{WF} q and (2) p →^{τ} implies that q →^{τ}.

– Weak failures equivalence ≡_{WF} is defined as ⊑_{WF} ∩ ⊑_{WF}^{−1}.

It is well-known that p ≤_{WF} q is not a precongruence for BCCS: e.g., τ0 ≤_{WF} 0 but τ0 + a0 ≰_{WF} 0 + a0. However, ⊑_{WF} is, meaning that p_{1} ⊑_{WF} q_{1} and p_{2} ⊑_{WF} q_{2} implies p_{1} + p_{2} ⊑_{WF} q_{1} + q_{2} and αp_{1} ⊑_{WF} αq_{1} for α ∈ A_{τ}. In fact, ⊑_{WF} is the coarsest precongruence contained in ≤_{WF}. Likewise, ≡_{WF} is a congruence for BCCS.

3 A Finite Basis for Weak Failures Semantics

3.1 Axioms for the Weak Failures Preorder

On BCCS processes, the weak failures preorder as defined above coincides with the inverse of the must-testing preorder of [8]. A sound and ground-complete axiomatization of the must-testing preorder preorder has been given in [8], in terms of a language richer than BCCS. After restriction to BCCS processes, and reversing the axioms, it consists of A1-4 together with the axioms:

\begin{matrix}N1 & αx + αy & ≈ & α(τx + τy) \\ N2 & τ(x + y) & ≼ & x + τy \\ N3 & αx + τ(αy + z) & ≈ & τ(αx + αy + z) \\ E1 & x & ≼ & τx + τy \end{matrix}

Here we simplify this axiomatisation to A1-4 and WF1-3 from Tab. 1. In fact it is an easy exercise to derive WF1-3 from N1, N2 and E1, and N1, N2 and E1 from WF1-3. It is a little harder to check that N3 is derivable from the other three axioms (cf. Lem. 1).

\begin{matrix}WF1 & ax + ay & ≈ & a(τx + τy) \\ WF2 & τ(x + y) & ≼ & τx + y \\ WF3 & x & ≼ & τx + y \end{matrix}

Table 1. Axiomatization for the weak failures preorder

Theorem 1. A1-4+WF1-3 is sound and ground-complete for BCCS(A) modulo ⊑_{WF}.

In this section, we extend this ground-completeness result with two ω-completeness results. The first one says, in combination with Theo. 1, that as long as our alphabet of actions is infinite, the axioms A1-4+WF1-3 constitute a finite basis for the inequational theory of BCCS(A) modulo ⊑_{WF}.

Theorem 2. If |A|=∞, then A1-4+WF1-3 is ω-complete for BCCS(A) modulo ⊑_{WF}.

To get a finite basis for the inequational theory of BCCS modulo ⊑_{WF} in case |A| < ∞, we need to add the following axiom:

WF_{A}  ∑_{a∈A} ax_{a} ≼ ∑_{a∈A} ax_{a} + y

where the x_{a} for a ∈ A and y are distinct variables.

Theorem 3. If |A| < ∞, then A1-4+WF1-3+WF_{A} is ω-complete for BCCS(A) modulo ⊑_{WF}.

The rest of this section up to Sec. 3.4 is devoted to the proofs of Theorems 1–3. For a start, the inequations in Tab. 2 can be derived from A1-4+WF1-3:

D1  τ(x + y) + x ≈ τ(x + y)
D2  τ(τx + y) ≈ τx + y
D3  ax + τ(ay + z) ≈ τ(ax + ay + z)
D4  τx ≼ τx + y
D5  ∑_{i∈I} ax_{i} ≈ a(∑_{i∈I} τx_{i}) for finite nonempty index setsI
D6  τx + y ≈ τx + τ(x + y)
D7  τx + τy ≈ τx + τ(x + y) + τy
D8  τx + τ(x + y + z) ≈ τx + τ(x + y) + τ(x + y + z)
D9  ∑_{i∈I} τ(at_{i} + y_{i}) ≈ ∑_{i∈I} τ(at + y_{i}) for finite I, where t = ∑_{i∈I} τt_{i}.

Table 2. Derived inequations

Lemma 1. D1-9 are derivable from A1-4+WF1-3.

Proof. Here we derive D3 only. The other proofs can be found in [5].

By WF3, ⊢ y ≼ τy + τx. So by WF1, ⊢ ay ≼ a(τx + τy) ≈ ax + ay. This implies ⊢ τ(ay+z) ≼ τ(ax+ay+z). Hence, by D1, ⊢ ax+τ(ay+z) ≼ ax+τ(ax+ay+z) ≈ τ(ax + ay + z).

Moreover, by WF2, ⊢ τ(ax + ay + z) ≼ ax + τ(ay + z). ⊓ ⊔ 3.2 Normal Forms

The notion of a normal form, which is formulated in the following two definitions, will play a key role in the forthcoming proofs. For any set L ⊆ A ∪ V of actions and variables let A_{L} = L ∩ A, the set of actions in L, and V_{L} = L ∩ V, the set of variables in L.

Definition 3 (Saturated family). Suppose L is a finite family of finite sets of actions and variables. We say L is saturated if it is nonempty and

– L_{1}, L_{2} ∈ L implies that L_{1} ∪ L_{2} ∈ L; and

– L_{1}, L_{2} ∈ L and L_{1} ⊆ L_{3} ⊆ L_{2} imply that L_{3} ∈ L.

Definition 4 (Normal form).

(i) A term t is in τ normal form if

t = ∑_{L∈L} τ ( ∑_{a∈A_{L}} at_{a} + V_{L})

where the t_{a} are in normal form and L is a saturated family of sets of actions and variables. We write L(t) for ⋃_{L∈L} L; note that L(t) ∈ L.

(ii) t is in action normal form if

t = ∑_{a∈A_{L}} at_{a} + V_{L}

where the t_{a} are in normal form and L ⊆ A ∪ V. We write L(t) for L.

(iii) t is in normal form if it is either in τ normal form or in action normal form.

Note that the definition of a normal form requires that for any a ∈ A, if t ⇒→^{a} t_{1} and t ⇒→^{a} t_{2}, then t_{1} and t_{2} are syntactically identical.

We prove that every term can be equated to a normal form.

Lemma 2. For any term t, A1-4+WF1-3 ⊢ t ≈ t′ for some normal form t′.

Proof. By induction on |t|. We shorten “A1-4+WF1-3 ⊢” to “⊢” and distinguish two cases.

– t ↛^{τ}. Let t = ∑_{i∈I} a_{i}t_{i} + Y. By D5,

⊢ t ≈ ∑_{a∈I(t)} a( ∑_{i∈I,a_{i}=a}τt_{i}) + Y .

By induction, for each a ∈ I(t),

⊢ ∑_{i∈I,a_{i}=a}τt_{i} ≈ t_{a}

for some normal form t_{a}. So we are done.

– t →^{τ}. By D6, t can be brought in the form ∑_{i∈I} τt_{i} with I ≠ ∅, and using D2 one can even make sure that t_{i} ↛^{τ} for i ∈ I. Using the first case in this proof, we obtain, for each i ∈ I,

⊢ t_{i} ≈ ∑_{a∈A_{L(i)}} at_{a,i} + V_{L(i)}

for some L(i) ⊆ A ∪ V. Thus

⊢ t ≈ ∑_{i∈I} τ ( ∑_{a∈A_{L(i)}} at_{a,i} + V_{L(i)}) .

For each a ∈ I(t), we define u_{a} = ∑_{i∈I, a∈A_{L(i)}}τt_{a,i} .

Then |u_{a}| < |t|. By induction, ⊢ u_{a} ≈ t_{a} for some normal form t_{a}. Define L = {L(i) | i ∈ I}. By repeated application of D9 we obtain

⊢ t ≈ ∑_{i∈I} τ ( ∑_{a∈A_{L(i)}}au_{a} + V_{L(i)}) ≈ ∑_{L∈L} τ ( ∑_{a∈A_{L}} at_{a} + V_{L}) .

The latter term has the required form, except that the family L need not be saturated. However, it is straightforward to saturate L by application of D7 and D8. ⊓ ⊔

Lemma 3. Suppose t and u are both in normal forms and t ⊑_{WF} u. If t ⇒→^{a} t_{a}, then there exists a term u_{a} such that u ⇒→^{a} u_{a} and t_{a} ≤_{WF} u_{a}.

Proof. Cf. [5]. ⊓ ⊔

3.3 ω-Completeness Proof

We are now in a position to prove Theo. 2 (ω-completeness in case of an infinite alphabet) and Theo. 3 (ω-completeness in case of a finite alphabet), along with Theo. 1 (ground completeness). We will prove these three theorems in one go. Namely, in the proof, two cases are distinguished; only in the second case (I(t) = A), in which the A is guaranteed to be finite, will the axiom WF_{A} play a role.

Proof. Let t ⊑_{WF} u. We need to show that ⊢ t ≼ u. We apply induction on |t| + |u|. By Lem. 2, we can write t and u in normal form.

We first prove that L(t) ⊆ L(u). Suppose this is not the case. Then there exists some a ∈ A_{L(t)} \ A_{L(u)} or some x ∈ V_{L(t)} \ V_{L(u)}. In the first case, let σ be the closed substitution with σ(z) = 0 for all z ∈ V; we find that (a, ∅) is a weak failure pair of σ(t) but not of σ(u), which contradicts the fact that σ(t) ⊑_{WF} σ(u). In the second case, pick some d > max{|t|, |u|}, and consider the closed substitution σ(x) = a^{d}0 and σ(z) = 0 for z ≠ x. Then (a^{d}, ∅) is weak failure pair of σ(t). However, it can not be a weak failure pair of σ(u), again contradicting σ(t) ⊑_{WF} σ(u).

We distinguish two cases, depending on whether I(t) = A or not.

1. I(t) ≠ A. We distinguish three cases. Due to the condition that t →^{τ} implies u →^{τ}, it cannot be the case that t is an action normal form and u a τ normal form.

(a) t and u are both action normal forms. So t = ∑_{a∈A_{L}} at_{a} + V_{L} and u = ∑_{a∈A_{M}} au_{a} +V_{M}. We show that L(t) = L(u). Namely, pick b ∈ A\A_{L}, and let σ be the closed substitution with σ(z) = 0 for any z ∈ V_{L}, and σ(z) = b0 for z ∉ V_{L}. As (ε, A \ I(t)) is a weak failure pair of t, and hence of u, it must be that L(u) ⊆ L(t). Together with L(t) ⊆ L(u) this gives L(t) = L(u). By Lem. 3, for each a ∈ I(t), t_{a} ≤_{WF} u_{a}, and thus clearly t_{a} ⊑_{WF} τu_{a}. By induction, ⊢ t_{a} ≼ τu_{a} and hence ⊢ at_{a} ≼ au_{a}. It follows that

⊢ t = ∑_{a∈A_{L}} at_{a} + V_{L} ≼ ∑_{a∈A_{L}} au_{a} + V_{L} = ∑_{a∈A_{M}} au_{a} + V_{M} = u

(b) Both t and u are τ normal forms:

t = ∑_{L∈L} τ( ∑_{a∈A_{L}} at_{a} + V_{L})

and

u = ∑_{M∈M} τ( ∑_{a∈A_{M}} au_{a} + V_{M})

By Lem. 3, for each a ∈ I(t), t_{a} ≤_{WF} u_{a}, and thus clearly t_{a} ⊑_{WF} τu_{a}. By induction, ⊢ t_{a} ≼ τu_{a}. By these inequalities, together with D4,

⊢ t ≼ ∑_{L∈L} τ( ∑_{a∈A_{L}} au_{a} + V_{L}) + u  (1)

We now show that L ⊆ M. Take any L ∈ L, pick b ∈ A \ A_{L}, and consider the closed substitution σ(z) = 0 for any z ∈ V_{L}, and σ(z) = b0 for z ∉ V_{L}. Since σ(t) →^{τ} σ(∑_{a∈L} at_{a}) and σ(t) ⊑_{WF} σ(u), there exists an M ∈ M with A_{M} ⊆ A_{L} and V_{M} ⊆ V_{L}. Since also L ⊆ L(t) ⊆ L(u), and M is saturated, it follows that L ∈ M. Hence, L ⊆ M.

Since L ⊆ M,

∑_{L∈L} τ( ∑_{a∈A_{L}} au_{a} + V_{L}) + u = u  (2)

By (1) and (2), ⊢ t ≼ u.

(c) t is an action normal form and u is a τ normal form. Then τt ⊑_{WF} u. Note that τt is a τ normal form, so according to the previous case,

⊢ τt ≼ u

By WF3,

⊢ t ≼ τt ≼ u

2. I(t) = A. Note that in this case, |A| < ∞. So, according to Theo. 3, axiom WF_{A} is at our disposal. As before, we distinguish three cases.

(a) Both t and u are action normal forms. Since L(t) ⊆ L(u) we have t = ∑_{a∈A} at_{a} + W and u = ∑_{a∈A} au_{a} + X with W ⊆ X. By WF_{A},

⊢ ∑_{a∈A} at_{a} ≼ ∑_{a∈A} at_{a} + u

By Lem. 3, for each a ∈ A, t_{a} ≤_{WF} u_{a}, and thus clearly t_{a} ⊑_{WF} τu_{a}. By induction, ⊢ t_{a} ≼ τu_{a}. It follows, using W ⊆ X, that

⊢ t = ∑_{a∈A} at_{a} + W ≼ ∑_{a∈A} au_{a} + u + W = u

(b) Both t and u are τ normal forms.

t = ∑_{L∈L} τ( ∑_{a∈A_{L}} at_{a} + V_{L})

and

u = ∑_{M∈M} τ( ∑_{a∈A_{M}} au_{a} + V_{M})

By D1 and WF_{A} (clearly, in this case A_{L(t)} = A),

⊢ t ≈ t + ∑_{a∈A} at_{a} ≼ t + ∑_{a∈A} at_{a} + u  (3)

By Lem. 3, for each a ∈ A, t_{a} ≤_{WF} u_{a}, and thus clearly t_{a} ⊑_{WF} τu_{a}. By induction, ⊢ t_{a} ≼ τu_{a}. By these inequalities, together with (3),

⊢ t ≼ ∑_{L∈L} τ( ∑_{a∈A_{L}} au_{a} + V_{L}) + ∑_{a∈A} au_{a} + u

So by D1,

⊢ t ≼ ∑_{L∈L} τ( ∑_{a∈A_{L}} au_{a} + V_{L}) + u  (4)

Now for L ∈ L with A_{L} ≠ A we have L ∈ M using the same reasoning as in 1(b). For L ∈ L with A_{L} = A we have V_{L} ⊆ V_{L(t)} ⊆ V_{L(u)}. By WF_{A} we have

⊢ τ( ∑_{a∈A_{L}} au_{a} + V_{L}) ≼ τ(∑_{a∈A} au_{a} + V_{L(u)})  (5)

As the latter is a summand of u we obtain t ≼ u.

(c) t is an action normal form and u is a τ normal form. This can be dealt with as in case 1(c).

This completes the proof. ⊓ ⊔ 3.4 Weak Failures Equivalence

In [2, 10] an algorithm is presented which takes as input a sound and ground-complete inequational axiomatization E for BCCSP modulo a preorder ⊑ which includes the ready simulation preorder and is initials preserving,^{1} and generates as output an equational axiomatization A(E) which is sound and ground-complete for BCCSP modulo the corresponding equivalence—its kernel: ⊑ ∩ ⊑^{−1}. Moreover, if the original axiomatization E is ω-complete, so is the resulting axiomatization. The axiomatization A(E) generated by the algorithm from E contains the axioms A1-4 for bisimulation equivalence and the axioms β(αx + z) + β(αx + αy + z) ≈ β(αx + αy + z) for α, β ∈ A_{τ} that are valid in ready simulation semantics, together with the following equations, for each inequational axiom t ≼ u in E:

– t + u ≈ u; and

– α(t + x) + α(u + x) ≈ α(u + x) (for each α ∈ A_{τ}, and some variable x that does not occur in t + u).

Recently, we lifted this result to weak semantics [6], which makes the aforementioned algorithm applicable to all 87 preorders surveyed in [12] that are at least as coarse as the ready simulation preorder. Namely, among others, we show that

Theorem 4. Let ⊑ be a weak initials preserving precongruence^{2} that contains the strong ready simulation preorder ⊑_{RS} and satisfies T2 (the second τ-law of CCS: τx ≈ τx + x), and let E be a sound and ground-complete axiomatization of ⊑. Then A(E) is a sound and ground-complete axiomatization of the kernel of ⊑. Moreover, if E is ω-complete, then so is A(E).

It is straightforward to check that weak failures meets the prerequisites of Theo. 4, and thus we can run the algorithm, and after simplification and omission of redundant axioms obtain the axiomatization for weak failures equivalence in Tab. 3. The axioms

WF1  ax + ay ≈ a(τx + τy)
WFE2  τ(x + y) + τx ≈ τx + y
WFE3  ax + τ(ay + z) ≈ τ(ax + ay + z)
WFE_{A}  τ(∑_{a∈A} ax_{a} + z) + τ(∑_{a∈A} ax_{a} + y + z) ≈ τ(∑_{a∈A} ax_{a} + y + z)

Table 3. Axiomatization for weak failures equivalence

WF1, WFE2-3 already appeared in [13]. A1-4+WF1+WFE2-3 is sound and groundcomplete for BCCS modulo ≡_{WF} (see also [13, 6]). By Theo. 2 and Theo. 3, we have:

Corollary 1. If |A| = ∞, then the axiomatization A1-4+WF1+WFE2-3 is ω-complete for BCCS(A) modulo ≡_{WF}.

Corollary 2. If |A| < ∞, then the axiomatization A1-4+WF1+WFE2-3+WFE_{A} is ωcomplete for BCCS(A) modulo ≡_{WF}.

1 meaning that p ⊑ q implies that I(p) ⊆ I(q), where the set I(p) of strongly initial actions is

I(p) = {α ∈ A_{τ} | p →^{α}}

2 meaning that p ⊑ q implies that I_{τ} (p) ⊆ I_{τ} (q), where the set I_{τ} (p) of weak initial actions is

I_{τ} (p) = {α ∈ A_{τ} | p ⇒→^{α}}

4 Weak Impossible Futures Semantics

Weak impossible futures semantics is closely related to weak failures semantics. Only, instead of the set of actions in the second argument of a weak failure pair (see Def. 2), an impossible future pair contains a set of traces.

Definition 5 (Weak impossible futures).

– A sequence a_{1} ⋯ a_{k} ∈ A^{∗}, with k ≥ 0, is a trace of a process p_{0} if there is a path p_{0} ⇒→^{a_{1}}⇒ ⋯ ⇒→^{a_{k}}⇒ p_{k}; it is a completed trace of p_{0} if moreover I(p_{k}) = ∅. Let T (p) denote the set of traces of process p, and CT (p) its set of completed traces.

– A pair (a_{1} ⋯ a_{k}, B), with k ≥ 0 and B ⊆ A^{∗}, is a weak impossible future of a process p_{0} if there is a path p_{0} ⇒→^{a_{1}}⇒ ⋯ ⇒→^{a_{k}}⇒ p_{k} with T (p_{k}) ∩ B = ∅.

– The weak impossible futures preorder ⊑_{WIF} is given by p ⊑_{WIF} q iff (1) the weak impossible futures of p are also weak impossible futures of q, (2) T (p) = T (q) and (3) p →^{τ} implies that q →^{τ}.

– Weak impossible futures equivalence ≡_{WIF} is defined as ⊑_{WIF} ∩ ⊑_{WIF}^{−1}.

⊑_{WIF} is a precongruence, and ≡_{WF} a congruence, for BCCS [22]. The requirement (2) T (p) = T (q) is necessary for this precongruence property. Without it we would have τa0 ⊑ τa0 + b0 but c(τa0) ⋢ c(τa0 + b0).

A sound and ground-complete axiomatization for ⊑_{WIF} is obtained by replacing axiom WF3 in Tab. 1 by the following axiom (cf. [22], where a slightly more complicated, but equivalent, axiomatization is given):

WIF3 x ≼ τx

However, surprisingly, there is no finite sound and ground-complete axiomatization for ≡_{WIF}. We will show this in Sec. 4.1. A similar difference between the impossible futures preorder and equivalence in the concrete case (so in the absence of τ) was found earlier in [4]. We note that, since weak impossible futures semantics is not coarser than ready simulation semantics, the algorithm from [2, 10, 6] to generate an axiomatization for the equivalence from the one for the preorder, does not work in this case.

We also established that the sound and ground-complete axiomatization for BCCS modulo ⊑_{WIF} is ω-complete in case |A| = ∞, and that there is no such finite basis for the inequational theory of BCCS modulo ⊑_{WIF} in case |A| < ∞. Again, these results correspond to (in)axiomatizability results for the impossible futures preorder in the concrete case [4], with very similar proofs.

Theorem 5. If |A| = ∞, then A1-4+WF1-2+WIF3 is ω-complete for BCCS(A) modulo ⊑_{WIF}.

Proof. In [22]. A somewhat simpler proof can be found in [5].

Theorem 6. If |A| < ∞, then the inequational theory of BCCS(A) modulo ⊑_{WIF} does not have a finite basis.

Proof. In the full version of this paper [5].

Concluding, in spite of the close resemblance between weak failures and weak impossible futures semantics, there is a striking difference between their axiomatizability properties.

4.1 Nonexistence of an Axiomatization for Equivalence

We now prove that for any (nonempty) A there does not exist any finite, sound, groundcomplete axiomatization for BCCS(A) modulo ≡_{WIF}. The cornerstone for this negative result is the following infinite family of closed equations, for m ≥ 0:

τa^{2m}0 + τ(a^{m}0 + a^{2m}0) ≈ τ(a^{m}0 + a^{2m}0)

It is not hard to see that they are sound modulo ≡_{WIF}. We start with a few lemmas.

Lemma 4. If p ≡_{WIF} q then CT (p) = CT (q).

Proof. A process p has a completed trace a_{1} ⋯ a_{k} iff it has a weak impossible future (a_{1} ⋯ a_{k}, A). ⊓ ⊔

Lemma 5. Suppose t ⊑_{WIF} u. Then for any t′ with t ⇒→^{τ} t′ there is some u′ with u ⇒→^{τ} u′ such that var (u′) ⊆ var (t′).

Proof. Let t ⇒→^{τ} t′. Fix some m > |t|, and consider the closed substitution ρ defined by ρ(x) = 0 if x ∈ var (t′) and ρ(x) = a^{m}0 if x ∉ var (t′). Since ρ(t) ⇒ ρ(t′) with |ρ(t′)| = |t′| < m, and ρ(t) ⊑_{WIF} ρ(u), clearly ρ(u) ⇒ q for some q with |q| < m. From the definition of ρ it then follows that there must exist u ⇒ u′ with var (u′) ⊆ var (t′). In case u ⇒→^{τ} u′ we are done, so assume u′ = u. Let σ be the substitution with σ(x) = 0 for all x ∈ V. Since σ(t) →^{τ} and t ⊑_{WIF} u we have σ(u) →^{τ}, so u →^{τ} u′′ for some u′′. Now var (u′′) ⊆ var (u) = var (u′) ⊆ var (t′). ⊓ ⊔

Lemma 6. Assume that, for terms t, u, closed substitution σ, action a and integer m:

1. t ≡_{WIF} u;

2. m > |u|;

3. CT (σ(u)) ⊆ {a^{m}, a^{2m}}; and

4. there is a closed term p′ such that σ(t) ⇒→^{τ} p′ and CT (p′) = {a^{2m}}.

Then there is a closed term q′ such that σ(u) ⇒→^{τ} q′ and CT (q′) = {a^{2m}}.

Proof. According to proviso (4) of the lemma, we can distinguish two cases.

– There exists some x ∈ V such that t ⇒ t′ with t′ = t′′ +x and σ(x) ⇒→^{τ} p′ where CT (p′) = {a^{2m}}. Consider the closed substitution ρ defined by ρ(x) = a^{m}0 and ρ(y) = 0 for any y ≠ x. Then a^{m} ∈ CT (ρ(t)) = CT (ρ(u)), using Lem. 4, and this is only possible if u ⇒ u′ for some u′ = u′′ + x. Hence σ(u) ⇒→^{τ} p′.

– t ⇒→^{τ} t′ with CT (σ(t′)) = {a^{2m}}. Since |t′| ≤ |t| = |u| < m, clearly, for

any x ∈ var (t′), either |σ(x)| = 0 or norm(σ(x)) > m, where norm(p) denotes the length of the shortest completed trace of p. Since t ≡_{WIF} u, by Lem. 5, u⇒ →^{u} u′ with var (u′) ⊆ var (t′). Hence, for any x ∈ var (u′), either |σ(x)| = 0 or norm(σ(x)) > m. Since |u′| < m, a^{m} ∉ CT (σ(u′)). It follows from CT (σ(u)) ⊆

{a^{m}, a^{2m}} that CT (σ(u′)) = {a^{2m}}. And u ⇒→^{τ} u′ implies σ(u) ⇒→^{τ} σ(u′). □

Lemma 7. Assume that, for E an axiomatization sound for ⊑_{WIF}, closed terms p, q, closed substitution σ, action a and integer m:

1. E ⊢ p ≈ q;

2. m > max{|u| | t ≈ u ∈ E};

3. CT (q) ⊆ {a^{m}, a^{2m}}; and

4. there is a closed term p′ such that p ⇒→^{τ} p′ and CT (p′) = {a^{2m}}.

Then there is a closed term q′ such that q ⇒→^{τ} q′ and CT (q′) = {a^{2m}}.

Proof. By induction on the derivation of E ⊢ p ≈ q.

– Suppose E ⊢ p ≈ q because σ(t) = p and σ(u) = q for some t ≈ u ∈ E or u ≈ t ∈ E and closed substitution σ. The claim then follows by Lem. 6.

– Suppose E ⊢ p ≈ q because E ⊢ p ≈ r and E ⊢ r ≈ q for some r. Since r ≡_{WIF} q, by proviso (3) of the lemma and Lem. 4, CT (r) ⊆ {a^{m}, a^{2m}}. Since there is a p′ such that p ⇒→^{τ} p′ with CT (p′) = {a^{2m}}, by induction, there is an r′ such that r ⇒→^{τ} r′ and CT (r′) = {a^{2m}}. Hence, again by induction, there is a q′

such that q ⇒→^{τ} q′ and CT (q′) = {a^{2m}}.

– Suppose E ⊢ p ≈ q because p = p_{1} + p_{2} and q = q_{1} + q_{2} with E ⊢ p_{1} ≈ q_{1} and E ⊢ p_{2} ≈ q_{2}. Since there is a p′ such that p ⇒→^{τ} p′ and CT (p′) = {a^{2m}}, either p_{1} ⇒→^{τ} p′ or p_{2} ⇒→^{τ} p′. Assume, without loss of generality, that p_{1} ⇒→^{τ} p′. By induction, there is a q′ such that q_{1} ⇒→^{τ} q′ and CT (q′) = {a^{2m}}. Now q ⇒→^{τ} q′.

– Suppose E ⊢ p ≈ q because p = cp_{1} and q = cq_{1} with c ∈ A and E ⊢ p_{1} ≈ q_{1}. In this case, proviso (4) of the lemma can not be met.

– Suppose E ⊢ p ≈ q because p = τp_{1} and q = τq_{1} with E ⊢ p_{1} ≈ q_{1}. By proviso (4) of the lemma, either CT (p_{1}) = {a^{2m}} or there is a p′ such that p_{1} ⇒→^{τ} p′ and CT (p′) = {a^{2m}}. In the first case, q ⇒→^{τ} q_{1} and CT (q_{1}) = {a^{2m}} by Lem. 4. In the second, by induction, there is a q′ such that q_{1} ⇒→^{τ} q′ and CT (q′) = {a^{2m}}.

Again q ⇒→^{τ} q′. ⊓ ⊔

Theorem 7. There is no finite, sound, ground-complete axiomatization for BCCS(A) modulo ≡_{WIF}.

Proof. Let E be a finite axiomatization over BCCS(A) that is sound modulo ≡_{WIF}. Let m be greater than the depth of any term in E. Clearly, there is no term r such that τ(a^{m}0 + a^{2m}0) ⇒→^{τ} r and CT (r) = {a^{2m}}. So according to Lem. 7, the closed equation τa^{2m}0 + τ(a^{m}0 + a^{2m}0) ≈ τ(a^{m}0 + a^{2m}0) cannot be derived from E. Nevertheless, it is valid modulo ≡_{WIF}. ⊓ ⊔

In the same way as above, one can establish the nonderivability of the equations a^{2m+1}0 + a(a^{m}0 + a^{2m}0) ≈ a(a^{m}0 + a^{2m}0) from any given finite equational axiomatization sound for ≡_{WIF}. As these equations are valid modulo (strong) 2-nested simulation equivalence, this negative result applies to all BCCS-congruences that are at least as fine as weak impossible futures equivalence and at least as coarse as strong 2nested simulation equivalence. Note that the corresponding result of [1] can be inferred.

References

1. L. Aceto, W.J. Fokkink, R.J. van Glabbeek & A. Ingólfsdóttir (2004): Nested semantics over finite trees are equationally hard. Information and Computation 191(2), pp. 203–232.

2. L. Aceto, W.J. Fokkink and A. Ingólfsdóttir (2007): Ready to preorder: Get your BCCSP axiomatization for free! In Proc. CALCO’07, LNCS 4624, Springer, pp. 65–79.

3. S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599.

4. T. Chen and W.J. Fokkink (2008): On the axiomatizability of impossible futures: Preorder versus equivalence. In Proc. LICS’08, IEEE, pp. 156–165.

5. T. Chen, W.J. Fokkink and R.J. van Glabbeek (2008): On finite bases for weak semantics: Failures versus Impossible futures. Full version of current paper. Available at http://

arxiv.org/abs/0810.4904.

6. T. Chen, W.J. Fokkink and R.J. van Glabbeek (2008): Ready to preorder: The case of weak process semantics. To appear in Information Processing Letters. Available at http:

//www.cwi.nl/^{∼}chen/Papers/equational.pdf

7. T. Chen, W.J. Fokkink, B. Luttik and S. Nain (2008): On finite alphabets and infinite bases. Information and Computation 206(5), pp. 492-519.

8. R. De Nicola & M. Hennessy (1984): Testing equivalences for processes. Theoretical Computer Science 34, pp. 83–133.

9. W.J. Fokkink and S. Nain (2005): A finite basis for failure semantics. In Proc. ICALP’05, LNCS 3580, Springer, pp. 755–765.

10. D. de Frutos-Escrig, C. Gregorio-Rodriguez and M. Palomino (2008): Ready to preorder: an algebraic and general proof. To appear in the Journal of Logic and Algebraic Programming.

Available at http://maude.sip.ucm.es/^{∼}miguelpt/.

11. R.J. van Glabbeek (1993): A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In Proc. MFCS ’93, LNCS 711, pp. 473–484.

12. R.J. van Glabbeek (1993): The linear time – branching time spectrum II. The semantics of sequential systems with silent moves. In Proc. CONCUR’93, LNCS 715, Springer, pp. 66–81.

13. R.J. van Glabbeek (1997): Notes on the methodology of CCS and CSP. Theoretical Computer Science 177(2), pp. 329–349.

14. R.J. van Glabbeek (2001): The linear time – branching time spectrum I. The semantics of concrete, sequential processes. In Handbook of Process Algebra, Elsevier, pp. 3–99.

15. R.J. van Glabbeek and M. Voorhoeve (2006): Liveness, fairness and impossible futures. In Proc. CONCUR’06, LNCS 4137, Springer, pp. 126-141.

16. J.F. Groote (1990): A new strategy for proving ω-completeness with applications in process algebra. In Proc. CONCUR’90, LNCS 458, Springer, pp. 314–331.

17. M. Hennessy (1988): Algebraic Theory of Processes. MIT Press.

18. R. Milner (1989): A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation 81, pp. 227–247.

19. A. Rensink and W. Vogler (2007): Fair testing. Information and Computation 205(2), pp. 125–198.

20. W.C. Rounds & S.D. Brookes (1981): Possible futures, acceptances, refusals and communicating processes. In Proc. FOCS’81, IEEE, pp. 140–149.

21. W. Vogler (1992): Modular construction and partial order semantics of Petri nets. LNCS 625, Springer.

22. M. Voorhoeve and S. Mauw (2001): Impossible futures and determinism. Information Processing Letters 80(1), pp. 51–58.