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?

An extended abstract of this paper appears as [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, w, 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 axiomatization 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. We shorten “A1-4+WF1-3 ⊢” to “⊢”.

1. By WF3, ⊢ x ≼ τx, and thus ⊢ τx + x ≼ τx. Moreover, by WF2, ⊢ τ(x + x) ≼ τx + x, hence ⊢ τx ≼ τx + x. In summary, ⊢ τx ≈ τx + x. So ⊢ τ(x + y) ≈ τ(x + y) + x + y + x ≈ τ(x + y) + x.

2. By WF2, ⊢ τ(x + τx) ≼ τx + τx = τx, so by D1, ⊢ ττx ≼ τx. Hence, by WF2, ⊢ τ(τx + y) ≼ ττx + y ≼ τx + y. Moreover, by WF3, ⊢ τx + y ≼ τ(τx + y).

3. 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).

4. By WF3 and D2, ⊢ τx ≼ ττx + y ≈ τx + y.

5. By induction on |I|, using WF1 and D2.

6. By D4 and D1, ⊢ τx + y ≼ τx + τ(x + y) + y ≈ τx + τ(x + y).

Moreover, by WF2, ⊢ τx + τ(x + y) ≼ τx + τx + y = τx + y.

7. By D4 in one direction; by D6 and D1 in the other.

8. By D4 in one direction; by D6 and D1 in the other.

9. By D1, ⊢ ∑_{i∈I} τ(at_{i} + y_{i}) ≈ ∑_{i∈I} τ(at_{i} + y_{i}) + u, where u = ∑_{i∈I} at_{i}. Thus, by repeated application of D3, ⊢ ∑_{i∈I} τ(at_{i} + y_{i}) ≈ ∑_{i∈I} τ(at_{i} + u + y_{i}) = ∑_{i∈I} τ(u + y_{i}). By D5 we have u = at. ⊓ ⊔

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. We start with an example.

Example 1. Suppose t = τ(at_{1} + τ(bt_{2} + ct_{3}) + x) + τ(at_{4} + τx + τy) + z. Then t can be equated to a τ normal form with L = {{a, b, c, x}, {a, x, y}, {a, b, c, x, y, z},

{a, b, c, x, y},{a, b, c, x, z},{a, b, x, y},{a, c, x, y},{a, x, y, z},{a, b, x, y, z},{a, c, x, y, z}}.

We give a detailed derivation. By D2,

⊢ t ≈ τ(at_{1} + bt_{2} + ct_{3} + x) + τ(at_{4} + x + y) + z

By D6,

⊢ t ≈ τ(at_{1} + bt_{2} + ct_{3} + x) + τ(at_{4} + x + y) + τ(at_{4} + x + y + z)

Let u_{a} = τt_{1} + τt_{4}, u_{b} = t_{2} and u_{c} = t_{3}. By D9,

⊢ t ≈ τ(au_{a} + bu_{b} + cu_{c} + x) + τ(au_{a} + x + y) + τ(au_{a} + x + y + z)

By induction, u_{a} can be brought into a normal form t_{a}, and likewise for u_{b} and u_{v}. So

⊢ t ≈ τ(tu_{a} + bt_{b} + ct_{c} + x) + τ(at_{a} + x + y) + τ(at_{a} + x + y + z)

By D7,

⊢ t ≈ \begin{matrix}τ(at_{a} + bt_{b} + ct_{c} + x) + τ(at_{a} + x + y) \\ +τ(at_{a} + x + y + z) + τ(at_{a} + bt_{b} + ct_{c} + x + y + z) \end{matrix}

Finally, by D8,

⊢ t \begin{matrix}≈ \begin{matrix}τ(at_{a} + bt_{b} + ct_{c} + x) + τ(at_{a} + x + y) + τ(at_{a} + x + y + z) \\ +τ(at_{a} + bt_{b} + ct_{c} + x + y + z) + τ(at_{a} + bt_{b} + ct_{c} + x + y) \\ +τ(at_{a} + bt_{b} + ct_{c} + x + z) + τ(at_{a} + bt_{b} + x + y) + τ(at_{a} + ct_{c} + x + y) \\ +τ(at_{a} + bt_{b} + x + y + z) + τ(at_{a} + ct_{c} + x + y + z) \end{matrix} \\ = ∑_{L∈L} τ(∑_{a∈A_{L}} at_{a} + V_{L}) \end{matrix}

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

Proof. By induction on |t|. We 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. Suppose t ⊑_{WF} u and t ⇒→^{a} t_{a}. Let σ be the closed substitution given by σ(x) = 0 for all x ∈ V. As (a, ∅) is a weak failure pair of σ(t) and σ(t) ⊑_{WF} σ(u), it is also a weak failure pair of u. Thus there exists a term u_{a} such that u ⇒→^{a} u_{a}. By the definition of a normal form, this term is unique. (*)

We now show that t_{a} ≤_{WF} u_{a}. Let ρ be a closed substitution. Consider a weak failure pair (a_{1} ⋯ a_{k}, B) of ρ(t_{a}). Then (aa_{1} ⋯ a_{k}, B) is a weak failure pair of ρ(t), and hence also of ρ(u). It suffices to conclude that (a_{1} ⋯ a_{k}, B) is a weak failure pair of ρ(u_{a}). However, we can not conclude this directly, as possibly u ⇒ x + u′ where (aa_{1} ⋯ a_{k}, B) is a weak failure pair of ρ(x). To ascertain that nevertheless (a_{1} ⋯ a_{k}, B) is a weak failure pair of ρ(u_{a}), we define a modification ρ′ of ρ such that for all ℓ ≤ k and for all terms v, ρ(v) and ρ′(v) have the same weak failure pairs (c_{1} ⋯ c_{ℓ}, B), while for all x ∈ V, (aa_{1} ⋯ a_{k}, B) is not a weak failure pair of ρ′(x).

We obtain ρ′(x) from ρ(x) by replacing subterms bp at depth k by 0 if b ∉ B and by bb0 if b ∈ B. That is,

ρ′(x) = chop_{k}(ρ(x))

with chop_{m} for all m ≥ 0 inductively defined by

chop_{m}(0) = 0
chop_{m}(p + q) = chop_{m}(p) + chop_{m}(q)
chop_{m}(τp) = τ chop_{m}(p)
chop_{0}(bp) = \{ \begin{matrix}0 & if b ∉ B \\ bb0 & if b ∈ B \end{matrix}
chop_{m+1}(bp) = b chop_{m}(p)

We proceed to prove that ρ′ has the desired properties mentioned above.

A. For all ℓ ≤ k and c_{1}, …, c_{ℓ} ∈ A and for all terms v, ρ(v) and ρ′(v) have the same weak failure pairs (c_{1} ⋯ c_{ℓ}, B), The difference between ρ(v) and ρ′(v) only appears within subterms of depth k, that is for terms p such that ρ(v) ⇒→^{c_{1}}⇒ ⋯ ⇒→^{c_{k}}⇒ p for certain c_{1}, …, c_{k} ∈ A. Such a subterm p of ρ(v) corresponds to a subterm p′ of ρ′(v)—still satisfying ρ′(v) ⇒→^{c_{1}}⇒ ⋯ ⇒→^{c_{k}}⇒ p′—in which certain subterms bq are replaced by 0 if b ∉ B and by bb0 if b ∈ B. For such corresponding subterms p and p′ we have I(p)∩B = ∅ if and only if I(p′)∩B = ∅. From this the claim follows immediately.

B. For all x ∈ V, (aa_{1} ⋯ a_{k}, B) is not a weak failure pair of ρ′(x).

To this end we show that for all closed terms p, chop_{m}(p) does not have any weak failure pair (c_{0} ⋯ c_{m}, B) with c_{0}, …, c_{m} ∈ A. We apply induction on m. Base case: Since the summands of chop_{0}(p), when skipping over initial τ-steps, are bb0 with b ∈ I(p) ∩ B, chop_{0}(p) does not have a weak failure pair (c_{0}, B). Induction step: Let m > 0. By induction, for closed terms q, chop_{m−1}(q) does not have weak failure pairs (c_{1} ⋯ c_{m}, B). Since the transitions of chop_{m}(p) are chop_{m}(p) →^{c} chop_{m−1}(q) for p →^{c} q, it follows that chop_{m}(p) does not have weak failure pairs (c_{0} ⋯ c_{m}, B).

Now, since (a_{1} ⋯ a_{k}, B) is a weak failure pair of ρ(t_{a}), by property (A) it is also a weak failure pair of ρ′(t_{a}), Therefore (aa_{1} ⋯ a_{k}, B) is a weak failure pair of ρ′(t), and hence also of ρ′(u). Since according to property (B) it is not the case that u ⇒ x + u′ with (aa_{1} ⋯ a_{k}, B) a weak failure pair of ρ′(x), it must be the case that u ⇒→^{a} u′′ such that (a_{1} ⋯ a_{k}, B) is a weak failure pair of ρ′(u′′). By (*), u′′ = u_{a}. Again by property (A), (a_{1} ⋯ a_{k}, B) is a weak failure pair of ρ(u_{a}). ⊓ ⊔

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).

Moreover, if E contains an equation (formally abbreviating two inequations), this equation is logically equivalent to the four equations in A(E) that are derived from it, and hence can be incorporated in the equational axiomatization unmodified.

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 obtain the axiomatization in Tab. 3 for weak failures equivalence. After simplification and omission of redundant axioms, we obtain the axiomatization in Tab. 4.

Lemma 4. The axioms in Tab. 3 are derivable from the axioms in Tab. 4 together with A1-4.

Proof. WF1 is unmodified. WF2^{a} and WF3^{a} can be trivially derived from WFE2. WF_{A}^{a} is derivable using A3.

To proceed, we have that WFE2 ⊢ ττx ≈ τx (namely by substituting τx for y and invoking D1, which is also derivable from WFE2) and hence also WFE2 ⊢ D2 (namely by substituting τx for x in WFE2 and invoking D1); using D2, the instances of WF2^{b}

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 ⇒→^{α}}

WF1  ax + ay ≈ a(τx + τy)
WF2^{a}  τ(x + y) + τx + y ≈ τx + y
WF2^{b}  α(τ(x + y) + z) + α(τx + y + z) ≈ α(τx + y + z)
WF3^{a}  x + τx + y ≈ τx + y
WF3^{b}  α(x + z) + α(τx + y + z) ≈ α(τx + y + z)
RS  β(αx + z) + β(αx + αy + z) ≈ β(αx + αy + z)
WF_{A}^{a}  ∑_{a∈A} ax_{a} + ∑_{a∈A} ax_{a} + y ≈ ∑_{a∈A} ax_{a} + y
WF_{A}^{b}  β(∑_{a∈A} ax_{a} + z) + β(∑_{a∈A} ax_{a} + y + z) ≈ β(∑_{a∈A} ax_{a} + y + z)

Table 3. Axiomatization generated by the algorithm

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 4. Axiomatization for weak failures equivalence

and WF3^{b} with α = τ, as well as the instance of RS with β = α = τ, are derivable from WFE2.

The instances of WF2^{b} and WF3^{b} with α ≠ τ, are derivable from WF1 and the instances with α = τ; the same holds for the instances of RS and WF_{A}^{b} with β ≠ τ.

Finally in the remaining instances of RS (with β = τ and α = a ∈ A), we have WFE2 ⊢ τ(ax + z) + τ(ax + ay + z) ≈ τ(ax + z) + ay, and thus they can be derived from WFE3. The instance of WF_{A}^{b} with β = τ is exactly WFE_{A}. ⊓ ⊔

The axioms WF1, WFE2-3 already appeared in [13]. A1-4+WF1+WFE2-3 is sound and ground-complete for BCCS modulo ≡_{WF} (see also [13, 6]). By Theo. 2 and Theo. 3 (together with Lem. 4), 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}.

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.

In Sec. 4.2 we establish that the sound and ground-complete axiomatization for BCCS modulo ⊑_{WIF} is ω-complete in case |A| = ∞, and in Sec. 4.3 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.

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 5. 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 6. 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 7. 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. 5, 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. 6, 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 8. 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. 7.

– 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. 5, 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. 5. In the second, by induction, there is a q′ such that q_{1} ⇒→^{τ} q′ and CT (q′) = {a^{2m}}.

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

Theorem 5. 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. 8, 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.

4.2 A Finite Basis for Preorder if |A| = ∞

In this section, we show that A1-4+WF1-2+WIF3 is ω-complete in case |A| = ∞. Note that this result was originally obtained in [22]. However, our proof is much simpler. First, let us note that A1-4+WF1-2+WIF3 ⊢ D1, D2, D5.

Lemma 9. For any closed terms p, q, if p ⊑_{WIF} q, then A1-4+WF1-2+WIF3 ⊢ p ≼ q.

Proof. Let p ⊑_{WIF} q. We prove ⊢ p ≼ q by induction on |p| + |q|. We distinguish two cases:

– q ↛^{τ}. Then p ↛^{τ} since p ⊑_{WIF} q. Suppose p = ∑_{i∈I} a_{i}p_{i} and q = ∑_{j∈J} b_{j}q_{j}. Clearly, we have I(p) = I(q). By D5, we have

⊢ p ≈ ∑_{a∈I(p)} a( ∑_{a_{i}=a,i∈I} τp_{i})

and

⊢ q ≈ ∑_{a∈I(p)} a( ∑_{b_{j}=a,j∈J} τq_{j})

Since p ⊑_{WIF} q, for each a ∈ I(p), the following relation holds:

∑_{a_{i}=a,i∈I} τp_{i} ⊑ ∑_{b_{j}=a,j∈J} τq_{j}

By induction,

⊢ ∑_{a_{i}=a,i∈I} τp_{i} ≼ ∑_{b_{j}=a,j∈J} τq_{j}

and thus

⊢ a( ∑_{a_{i}=a,i∈I} τp_{i}) ≼ a( ∑_{b_{j}=a,j∈J} τq_{j})

Summing these up for a ∈ I(p), we obtain that

⊢ p ≼ q

– q →^{τ}. By D2, we can write p ≈ ∑_{i∈I} α_{i}p_{i} and q ≈ ∑_{j∈J} β_{j}q_{j} such that for each α_{i} = τ (resp. β_{j} = τ), p_{i} ↛^{τ} (resp. q_{j} ↛^{τ}). Applying D1, for each i ∈ I with α_{i} = τ, the summands of p_{i} are also made summands of p, and likewise for q. (*)

For each i ∈ I with α_{i} = τ we have p →^{τ} p_{i}. Since p ⊑_{WIF} q and no q_{j} with β_{j} = τ contains a τ-summand, either T (q) ⊆ T (p_{i}) or there exists q →^{τ} q_{j} such that T (q_{j}) ⊆ T (p_{i}). Since q →^{τ}, in either case there exists some j_{i} ∈ J such that b_{j_{i}} = τ and T (q_{j_{i}}) ⊆ T (p_{i}). It follows that

p_{i} ⊑_{WIF} p_{i} + q_{j_{i}}

Since p_{i} ↛^{τ} and q_{j_{i}} ↛^{τ}, by the previous case,

⊢ p_{i} ≼ p_{i} + q_{j_{i}}

Hence by WF2,

⊢ τp_{i} ≼ τ(p_{i} + q_{j_{i}}) ≼ p_{i} + τq_{j_{i}}

and thus

⊢ p = ∑_{α_{i}=τ} τp_{i} + ∑_{a∈I(p)} ∑_{α_{i}=a,i∈I} ap_{i} ≼ ∑_{α_{i}=τ}(p_{i} + τq_{j_{i}}) + ∑_{a∈I(p)} ∑_{α_{i}=a,i∈I} ap_{i}

By (*),

⊢ ∑_{α_{i}=τ} p_{i} + ∑_{a∈I(p)} ∑_{α_{i}=a,i∈I} ap_{i} ≈ ∑_{a∈I(p)} ∑_{α_{i}=a,i∈I} ap_{i}

Since p ⊑_{WIF} q, I(p) = I(q). Using (*), it is easy to see that for each a ∈ I(p),

∑_{α_{i}=a,i∈I} ap_{i} ⊑_{WIF} ∑_{β_{j}=a,j∈J} aq_{j}

So by the previous case,

⊢ ∑_{α_{i}=a,i∈I} ap_{i} ≼ ∑_{β_{j}=a,j∈J} aq_{j}

It follows that

⊢ p ≼ ∑_{α_{i}=τ} τq_{j_{i}} + ∑_{a∈I(p)} ∑_{α_{i}=a,i∈I} ap_{i} ≼ ∑_{α_{i}=τ} τq_{j} + ∑_{a∈I(p)} ∑_{β_{j}=a,j∈J} aq_{j}

By WIF3,

⊢ ∑_{α_{i}=τ} τq_{j} + ∑_{a∈I(p)} ∑_{β_{j}=a,j∈J} aq_{j} ≼ q

Hence  ⊢ p ≼ q  ⊓ ⊔

With this ground-completeness result at hand, it is straightforward to apply the inverted substitution technique of Groote [16] to derive:

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

Proof. Given an inequational axiomatization E and open terms t, u such that E ⊢ σ(t) ≼ σ(u) for all closed substitutions σ, the technique of inverted substitutions is a method to prove E ⊢ t ≼ u. It does so by means of a closed substitution ρ encoding open terms into closed terms, and an decoding operation R that turns closed terms back into open terms. By assumption we have E ⊢ ρ(t) ≼ ρ(u). The pair (ρ, R) should be chosen in such a way that, in essence, applying R to all terms occurring in a proof of ρ(t) ≼ ρ(u) yields a proof of t ≼ u. As observed in [16], this technique is applicable when three conditions are met, one of which being that R(ρ(t)) = t and R(ρ(u)) = u. In fact, [16] dealt with equational logic only, but the very same reasoning applies to inequational logic [4].

Here we use the same pair (ρ, R) that was used by Groote to obtain most of the applications of the technique in [16]—it could be called the default (inverted) substitution. It is obtained by selecting for each variable x ∈ V an action a_{x} ∈ A, not occurring in t or u. This is possible because |A| = ∞. Now the default substitution ρ is given by ρ(x) = a_{x}0 and the default inverted substitution R replaces any maximal subterm of the form a_{x}p into the variable x. Groote showed that with this particular (inverted) substitution, 2 out of his 3 conditions are always met, and the third one simply says that for each axiom t ≼ u in E we should have that E ⊢ R(t) ≼ R(u). This condition is clearly met for the axioms A1-4+WF1-2+WIF3, and hence this axiomatization is ωcomplete. ⊓ ⊔

Note that we could have used the same method to obtain Theo. 2, but not Theo. 3.

4.3 Nonexistence of a Finite Basis for Preorder if |A| < ∞

1 < |A| < ∞. We prove that the inequational theory of BCCS(A) modulo ⊑_{WIF} does not have a finite basis in case of a finite alphabet with at least two elements. The cornerstone for this negative result is the following infinite family of inequations, for m ≥ 0:

τ(a^{m}x) + Φ_{m} ≼ Φ_{m}

with

Φ_{m} = τ(a^{m}x + x) + ∑_{b∈A} τ(a^{m}x + a^{m}b0)

It is not hard to see that these inequations are sound modulo ⊑_{WIF}. Namely, given a closed substitution ρ, we have T (ρ(τ(a^{m}x))) ⊆ T (ρ(Φ_{m})) and ρ(Φ_{m}) →^{τ}. To argue that ρ(τ(a^{m}x) + Φ_{m}) and ρ(Φ_{m}) have the same impossible futures, we only need to consider the transition ρ(τ(a^{m}x) + Φ_{m}) →^{τ} a^{m}ρ(x) (all other cases being trivial). If ρ(x) = 0, then ρ(Φ_{m}) →^{τ} a^{m}0 + 0 generates the same impossible futures (ε, B). If, on the other hand, b ∈ I(ρ(x)) for some b ∈ A, then T (a^{m}ρ(x) + a^{m}b0) = T (a^{m}ρ(x)), so ρ(Φ_{m}) →^{τ} a^{m}ρ(x) + a^{m}b0 generates the same impossible futures (ε, B).

We have already defined the traces and completed traces of closed terms. Now we extend these definitions to open terms by allowing (completed) traces of the form a_{1} ⋯ a_{k}x ∈ A^{∗}V. We do this by treating each variable occurrence x in a term as if it were a subterm x0 with x a visible action, and then apply Def. 5. Under this convention, CT (Φ_{m}) = {a^{m}x, x, a^{m}b | b ∈ A}. We write T_{V} (t) for the set of traces of t that end in a variable, and T_{A}(t) for ones that end in an action.

Observation 1. Let m > |t| or a_{m} ∈ V. Then a_{1} ⋯ a_{m} ∈ T (σ(t)) iff there is a k < m and y ∈ V such that a_{1} ⋯ a_{k}y ∈ T_{V} (t) and a_{k+1} ⋯ a_{m} ∈ T (σ(y)).

Lemma 10. If |A| > 1 and t ⊑_{WIF} u then T_{A}(t) = T_{A}(u) and T_{V} (t) = T_{V} (u).

Proof. Let σ be the closed substitution defined by σ(x)=0 for all x∈V. Then t ⊑_{WIF} u implies σ(t) ⊑_{WIF} σ(u) and hence T_{A}(t) = T (σ(t)) = T (σ(u)) = T_{A}(u) by Def. 5.

For the second statement fix distinct actions a, b ∈ A and an injection ⌜·⌝ : V → ℤ_{>0} (which exists because V is countable). Let m = |u| + 1 = |t| + 1. Define the closed substitution ρ by ρ(z) = a^{⌜z⌝·m}b0 for all z ∈ V. Again, by Def. 5, t ⊑_{WIF} u implies T (ρ(t)) = T (ρ(u)). By Obs. 1, for all terms v we have a_{1} ⋯ a_{k}y ∈ T_{V} (v) iff a_{1} ⋯ a_{k}a^{⌜y⌝·m}b ∈ T (ρ(v)) with k < m. Hence T_{V} (v) is completely determined by T (ρ(v)) and thus T_{V} (t) = T_{V} (u). ⊓ ⊔

Lemma 11. Let |A| > 1. Suppose t ⊑_{WIF} u and t ⇒→^{τ} t′. Then there is a term u′ such that u ⇒→^{τ} u′ and T_{V} (u′) ⊆ T_{V} (t′).

Proof. Define ρ exactly as in the previous proof. Since ρ(t) ⇒ ρ(t′) and t ⊑_{WIF} u there must be a u′ with ρ(u) ⇒ q and T (q) ⊆ T (ρ(t′)). Since ρ(x) is τ-free for x ∈ V it must be that q = ρ(u′) for some term u′ with u ⇒ u′. Given the relationship between T_{V} (v) and T (ρ(v)) for terms v observed in the previous proof, it follows that T_{V} (u′) ⊆ T_{V} (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 T_{V} (u′′) ⊆ T_{V} (u) = T_{V} (u′) ⊆ T_{V} (t′). ⊓ ⊔

Lemma 12. Let |A| > 1. Assume that, for some terms t, u, substitution σ, action a and integer m:

1. t ⊑_{WIF} u;

2. m ≥ |u|; and 3. σ(t) ⇒→^{τ} t̂for a term t̂without traces ax for x ∈ V or a^{m}b for b ∈ A.

Then σ(u) ⇒→^{τ} û for a term û without traces ax for x ∈ V or a^{m}b for b ∈ A.

Proof. Based on proviso (3) there are two cases to consider.

– y ∈ T_{V} (t) for some y ∈ V and σ(y) ⇒→^{τ} t̂. In that case y ∈ T_{V} (u) by Lem. 10, so

σ(u) ⇒→^{τ} t̂.

– t ⇒→^{τ} t′ for some term t′ such that t̂ = σ(t). By Lem. 11 there is a term u′ with u ⇒→^{τ} u′ and T_{V} (u′) ⊆ T_{V} (t′). Take û = σ(u′). Clearly σ(u) ⇒→^{τ} σ(u′). Suppose σ(u′) would have a trace a^{m}b. Then, by Obs. 1, there is a k ≤ m and y ∈ V such that a^{k}y ∈ T_{V} (u′) and a^{m−k}b ∈ T (σ(y)). Since T_{V} (u′) ⊆ T_{V} (t′) we have a^{m}b ∈ T (σ(t′)), which is a contradiction. The case ax ∈ T (σ(u)) is dealt with in the same way. ⊓ ⊔

Lemma 13. Let |A| > 1 and let E be an axiomatization sound for ⊑_{WIF}. Assume that, for some terms v, w, action a and integer m:

1. E ⊢ v ≼ w;

2. m ≥ max{|u| | t ≼ u ∈ E}; and

3. v ⇒→^{τ} v̂ for a term v̂ without traces ax for x ∈ V or a^{m}b for b ∈ A. Then w ⇒→^{τ} ŵ for a term ŵ without traces ax for x ∈ V or a^{m}b for b ∈ A.

Proof. By induction on the derivation of E ⊢ v ≼ w.

– Suppose E ⊢ v ≼ w because σ(t) = v and σ(u) = w for some t ≼ u ∈ E and substitution σ. The claim then follows by Lem. 12.

– Suppose E ⊢ v ≼ w because E ⊢ v ≼ u and E ⊢ u ≼ w for some u. By induction, u ⇒→^{τ} û for a term û without traces ax or a^{m}b. Hence, again by induction, w ⇒→^{τ} ŵ for a term ŵ without traces ax or a^{m}b.

– Suppose E ⊢ v ≼ w because v = v_{1} +v_{2} and w = w_{1} +w_{2} with E ⊢ v_{1} ≼ w_{1} and E ⊢ v_{2} ≼ w_{2}. Since v ⇒→^{τ} v̂, either v_{1} ⇒→^{τ} v̂ or v_{2} ⇒→^{τ} v̂. Assume, without loss of generality, that v_{1} ⇒→^{τ} v̂. By induction, w_{1} ⇒→^{τ} ŵ for a term ŵ without traces ax or a^{m}b. Now w ⇒→^{τ} ŵ.

– Suppose E ⊢ v ≼ w because v = cv_{1} and w = cw_{1} with c ∈ A and E ⊢ v_{1} ≈ w_{1}. In this case, proviso (3) of the lemma can not be met.

– Suppose E ⊢ v ≼ w because v = τv_{1} and w = τw_{1} with E ⊢ v_{1} ≈ w_{1}. Then either v_{1} = v̂ or v_{1} ⇒→^{τ} v̂. In the first case, w_{1} has no traces ax or a^{m}b by Lem. 10 and proviso (3) of the lemma; hence w has no such traces either. In the second case, by induction, w_{1} ⇒→^{τ} ŵ for a term ŵ without traces ax or a^{m}b. Again w ⇒→^{τ} ŵ.

⊓ ⊔

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

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. According to Lem. 13, the inequation τ(a^{m}x) + Φ_{m} ≼ Φ_{m} cannot be derived from E. Yet it is sound modulo ⊑_{WIF}. ⊓ ⊔ |A| = 1. We prove that the inequational theory of BCCS(A) modulo ⊑_{WIF} does not have a finite basis in case of a singleton alphabet. The cornerstone for this negative result is the following infinite family of inequations, for m ≥ 0:

a^{m}x ≼ a^{m}x + x

If |A| = 1, then these inequations are clearly sound modulo ⊑_{WIF}. Note that given a closed substitution ρ, T (ρ(x)) ⊆ T (ρ(a^{m}x)).

Lemma 14. If t ⊑_{WIF} u then T_{V} (t) ⊆ T_{V} (u).

Proof. Fix a ∈ A and an injection ⌜·⌝ : V → ℤ_{>0}. Let m = |u| + 1. Define the closed substitution ρ by ρ(z) = a^{⌜z⌝·m}0 for all z ∈ V. By Lem. 5, CT (ρ(t)) ⊆ CT (ρ(u)). Now suppose a_{1} ⋯ a_{k}y ∈ T_{V} (t). Then a_{1} ⋯ a_{k}a^{⌜y⌝·m} ∈ CT (ρ(t)) ⊆ CT (ρ(u)) and k < m. This is only possible if a_{1} ⋯ a_{k}y ∈ T_{V} (u). ⊓ ⊔

Lemma 15. Assume that, for terms t, u, substitution σ, action a, variable x, integer m:

1. t ⊑_{WIF} u;

2. m > |u|; and

3. x ∈ T_{V} (σ(u)) and a^{k}x ∉ T_{V} (σ(u)) for 1 ≤ k < m.

Then x ∈ T_{V} (σ(t)) and a^{k}x ∉ T_{V} (σ(t)) for 1 ≤ k < m.

Proof. Since x ∈ T_{V} (σ(u)), by Obs. 1 there is a variable y with y ∈ T_{V} (u) and x ∈ T_{V} (σ(y)). Consider the closed substitution ρ given by ρ(y) = a^{m}0 and ρ(z) = 0 for z ≠ y. Then m > |u| = |t|, and y ∈ T_{V} (u) implies a^{m} ∈ T (ρ(u)) = T (ρ(t)), so by Obs. 1 there is some k < m and z ∈ V such that a^{k}z ∈ T_{V} (t) and a^{m−k} ∈ T (ρ(z)). As k < m it must be that z = y. Since a^{k}y ∈ T_{V} (t) and x ∈ T_{V} (σ(y)), Obs. 1 implies that a^{k}x ∈ T_{V} (σ(t)). By Lem. 14, a^{k}x ∉ T_{V} (σ(t)) for 1 ≤ k < m. Hence we obtain k = 0. ⊓ ⊔

Lemma 16. Assume that, for E an axiomatization sound for ⊑_{WIF} and for terms v, w, action a, variable x and integer m:

1. E ⊢ v ≼ w;

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

3. x ∈ T_{V} (w) and a^{k}x ∉ T_{V} (w) for 1 ≤ k < m.

Then x ∈ T_{V} (v) and a^{k}x ∉ T_{V} (v) for 1 ≤ k < m.

Proof. By induction on the derivation of E ⊢ v ≼ w.

– Suppose E ⊢ v ≼ w because σ(t) = v and σ(u) = w for some t ≼ u ∈ E and substitution σ. The claim then follows by Lem. 15.

– Suppose E ⊢ v ≼ w because E ⊢ v ≼ u and E ⊢ u ≼ w for some u. By induction, x ∈ T_{V} (u) and a^{k}x ∉ T_{V} (u) for 1 ≤ k < m. Hence, again by induction, x ∈ T_{V} (v) and a^{k}x ∉ T_{V} (v) for 1 ≤ k < m.

– Suppose E ⊢ v ≼ w because v = v_{1} + v_{2} and w = w_{1} + w_{2} with E ⊢ v_{1} ≼ w_{1} and E ⊢ v_{2} ≼ w_{2}. Since x ∈ T_{V} (w), either x ∈ T_{V} (w_{1}) or x ∈ T_{V} (w_{2}). Assume, without loss of generality, that x ∈ T_{V} (w_{1}). Since a^{k}x ∉ T_{V} (w) for 1 ≤ k < m, surely a^{k}x ∉ T_{V} (w_{1}) for 1 ≤ k < m. By induction, x ∈ T_{V} (v_{1}), and hence x ∈ T_{V} (v). For 1 ≤ k < m we have a^{k}x ∉ T_{V} (w) and hence a^{k}x ∉ T_{V} (v), by Lem. 14.

– Suppose E ⊢ v ≼ w because v = cv_{1} and w = cw_{1} with c ∈ A and E ⊢ v_{1} ≈ w_{1}. In this case, proviso (3) of the lemma can not be met.

– Suppose E ⊢ v ≼ w because v = τv_{1} and w = τw_{1} with E ⊢ v_{1} ≈ w_{1}. Then, by proviso (3) of the lemma, x ∈ T_{V} (w_{1}) and a^{k}x ∉ T_{V} (w_{1}) for 1 ≤ k < m. By induction, x ∈ T_{V} (v_{1}) and a^{k}x ∉ T_{V} (v_{1}) for 1 ≤ k < m. Hence x ∈ T_{V} (v) and a^{k}x ∉ T_{V} (v) for 1 ≤ k < m. ⊓ ⊔

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

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. According to Lem. 16, the inequation a^{m}x ≼ a^{m}x + x cannot be derived from E. Yet, since |A| = 1, it is sound modulo ⊑_{WIF}. ⊓ ⊔

To conclude this subsection, we have

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

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

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. Extended abstract of this current paper. To appear in Proc. SOFSEM’09, LNCS, Springer.

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.