Axiomatizing Flat Iteration

R.J. van Glabbeek^{∗}

Computer Science Department, Stanford University Stanford, CA 94305-9045, USA.

                          rvg@cs.stanford.edu

Flat iteration is a variation on the original binary version of the Kleene star operation P^{∗}Q, obtained by restricting the first argument to be a sum of atomic actions. It generalizes prefix iteration, in which the first argument is a single action. Complete finite equational axiomatizations are given for five notions of bisimulation congruence over basic CCS with flat iteration, viz. strong congruence, branching congruence, η-congruence, delay congruence and weak congruence. Such axiomatizations were already known for prefix iteration and are known not to exist for general iteration. The use of flat iteration has two main advantages over prefix iteration:

1. The current axiomatizations generalize to full CCS, whereas the prefix iteration approach does not allow an elimination theorem for an asynchronous parallel composition operator.

2. The greater expressiveness of flat iteration allows for much shorter completeness proofs.

In the setting of prefix iteration, the most convenient way to obtain the completeness theorems for η-, delay, and weak congruence was by reduction to the completeness theorem for branching congruence. In the case of weak congruence this turned out to be much simpler than the only direct proof found. In the setting of flat iteration on the other hand, the completeness theorems for delay and weak (but not η-) congruence can equally well be obtained by reduction to the one for strong congruence, without using branching congruence as an intermediate step. Moreover, the completeness results for prefix iteration can be retrieved from those for flat iteration, thus obtaining a second indirect approach for proving completeness for delay and weak congruence in the setting of prefix iteration.

1 Introduction

The research literature on process theory has recently witnessed a resurgence of interest in Kleene star-like operations [6, 11, 9, 19, 8, 3, 10, 1, 2]. In [8] treebased models for theories involving Kleene’s star operation ^{∗} [15] are studied. [6] investigates the expressive power of variations on standard process description languages in which infinite behaviours are defined by means of ^{∗} rather than by means of systems of recursion equations. The papers [11, 19, 9, 3, 10, 1, 2] study the possibility of giving finite equational axiomatizations of bisimulation-like equivalences over fragments of such languages. This study is continued here.

∗This work was supported by ONR under grant number N00014-92-J-1974.

In [11] a complete finite equational axiomatization of strong bisimulation equivalence was given for a process algebra featuring choice, sequential composition, and the original binary version of the Kleene star operation P^{∗}Q [15].

[19] shows that such an axiomatization does not exists in the presence of the process 0 denoting inaction, or a process denoting successful termination. The same proof strategy can be adopted to conclude that there is no finite equational axiomatization for weak or branching bisimulation over an enrichment of this basic process algebra with an internal action.

For this reason restrictions of the Kleene star have been investigated. [9] presents a finite, complete equational axiomatization of strong bisimulation equivalence for Basic CCS (the fragment of Milner’s CCS [16] containing the operations needed to express finite synchronization trees) with prefix iteration. Prefix iteration is a variation on the binary Kleene star operation P^{∗}Q, obtained by restricting the first argument to be an atomic action. The same is done in [1] for string iteration. The work of [9] has been extended in [2] and its predecessors [3, 10, 12] to cope with weak, delay, eta- and branching bisimulation congruence in a setting with the unobservable action τ. Motivation and background material on these behavioural congruences can be found, e.g., in [16] and [13]. The strategy adopted in [2] in establishing the completeness results is based upon the use of branching equivalence in the analysis of weak, delay and η-equivalence, advocated in [12]. Following [12], complete axiomatizations for weak, delay and η-congruence were obtained from one for branching congruence by:

1. identifying a collection of process terms on which branching congruence coincides with the congruence one aims at axiomatizing, and

2. finding an axiom system that allows for the reduction of every process term to one of the required form.

Perhaps surprisingly, the proof for weak congruence so obtained is simpler than the one given in [3] which only uses properties of weak congruence. The direct proof method employed in [3] yields a long proof with many case distinctions, while the indirect proof via branching congruence in [2] is considerably shorter, and relies on a general relationship between the two congruences. Moreover, attempts to obtain a direct proof of the completeness theorem for weak congruence which is simpler than the one presented in [3] have been to no avail.

Results The present paper extends the results from [9] and [2] from prefix iteration to flat iteration. Flat iteration was first mentioned in the technical report version of [6]; it allows the first argument P of P^{∗}Q to be a (possibly empty) sum of actions. For convenience, the CCS operator of action-prefixing is also generalized to prefixing with sums of actions.

My completeness proofs are considerably shorter than the ones in [2]. This is mostly a result of the presence of expressions of the form 0^{∗}P in the language, which allows a collapse of several cases in the case distinction in [2]. In addition, the results for weak and delay congruence can be obtained without using branching congruence as an intermediate step. Thanks to the greater expressiveness of flat iteration, these results can be reduced to the one for strong congruence, using the same proof strategy as outlined above. However, the proposed reduction to strong congruence does not work for η- and branching congruence.

In addition I derive the existing axiomatizations for prefix iteration from the ones for flat iteration. In the case of weak congruence one finds therefore that although a direct proof is cumbersome, there is a choice between two attractive indirect proofs. One of them involves first establishing the result for branching congruence; the other involves first establishing the result for a richer language.

Finally, extending a result from [6], I derive an expansion theorem for the CCS parallel composition operator in the setting of flat iteration. This is the key to extending the complete axiomatizations of this paper to full CCS. I show that such a theorem does not exist in the setting of prefix iteration.

As in [2], my completeness proofs apply to open terms directly, and thus yield the ω-completeness of the axiomatizations as well as their completeness for closed terms. However, the generalization to full CCS applies to closed terms only.

Outline of the paper Section 2 introduces the language of basic CCS with flat iteration, BCCS^{f∗}, and its operational semantics. It also recalls the definitions of strong, branching, η-, delay and weak congruence. The axiom systems that will be shown to completely characterize the aforementioned congruences over BCCS^{f∗} are presented in Section 3, and Section 4 contains the proofs of their completeness. In Section 5 the existing axiomatizations for prefix iteration are derived from the ones for flat iteration. Finally, Section 6 indicates how the completeness results of this paper, unlike the ones for prefix iteration, can, at least for closed terms, be extended to full CCS.

2 Basic CCS with Flat Iteration

Assume a set A of observable actions. Let τ ∉ A denote a special invisible action and write A_{τ} := A ∪ {τ}. Also assume an infinite set Var of variables, disjoint with A_{τ}. Let x, y, ... range over Var, a, b, ... over A, α, β, γ, ... over A_{τ} and ξ over A_{τ} ∪ Var.

The two-sorted language BCCS^{f∗} of basic CCS with flat iteration is given by the BNF grammar:

S ::= 0 | α | S + S
P ::= x | 0 | S.P | P + P | S^{∗}P

Terms of sort S are called sumforms, whereas terms of sort P are called process expressions. The set of sumforms is denoted by SF and the set of (open) process expressions by . Let s, t, u range over SF and P, Q, R, S, T over . In writing terms over the above syntax one may leave out redundant brackets, assuming that + binds weaker than . and ^{∗}. For I = {i_{1}, …, i_{n}} a finite index set, ∑_{i∈I} P_{i} or ∑ {P_{i} | i ∈ I} denotes P_{i_{1}} + ⋯ + P_{i_{n}}. By convention, ∑_{i∈∅} P_{i} stands for 0.

The transition relations →^{ξ} are the least subsets of ( × ) ∪ SF satisfying the rules in Fig. 1. These determine the operational semantics of BCCS^{f∗}. A transition P →^{α} Q (α ∈ A_{τ}) indicates that the system represented by the term P can perform the action α, thereby evolving into Q, whereas P →^{x} P′ means that the initial behaviour of P may depend on the term that is substituted for the process variable x. It is not hard to see that if P →^{x} P′ then P′ = x. A transition s →^{α} just says that α is one of the actions in the sumform s.

\overline{α →^{α}}  \frac{s →^{α}}{s + t →^{α}}  \frac{t →^{α}}{s + t →^{α}}

\overline{x →^{x} x}  \frac{s →^{α}}{s.P →^{α} P}  \frac{P →^{ξ} P′}{P + Q →^{ξ} P′}  \frac{Q →^{ξ} Q′}{P + Q →^{ξ} Q′}

\frac{s →^{α}}{s^{∗}P →^{α} s^{∗}P}  \frac{P →^{ξ} P′}{s^{∗}P →^{ξ} P′}

Fig. 1: Transition rules for BCCS^{f∗}

The set der(P) of derivatives of P is the least set containing P that is closed under action-transitions. Formally, pder(P) is the least set satisfying:

if Q ∈ {P } ∪ pder(P) and Q →^{α} Q′ for some α ∈ A_{τ}, then Q′ ∈ pder(P),

and der(P) = {P } ∪ pder(P). Members of pder(P) are called proper derivatives.

Definition 2.1 Write p ⇒ q for ∃n≥0: ∃p_{0}, ..., p_{n}: p=p_{0} →^{τ} p_{1} →^{τ} ... →^{τ} p_{n} =q,

i.e. a (possibly empty) path of τ-steps from p to q. Furthermore, for ξ ∈ A_{τ} ∪Var,

write p →^{(ξ)} q for p →^{ξ} q∨(ξ = τ ∧p = q). Thus →^{(ξ)} is the same as →^{ξ} for ξ ∈ A∪Var,

and →^{(τ)} denotes zero or one τ-steps.

A weak bisimulation is a symmetric binary relation R on , such that

sRt ∧ s →^{ξ} s′ implies ∃t_{1}, t_{2}, t′ : t ⇒ t_{1} →^{(ξ)} t_{2} ⇒ t′ ∧ s′Rt′.  (1)

A weak bisimulation is a delay bisimulation if in the conclusion of (1) one has t_{2} = t′. It is an η-bisimulation if one has sRt_{1}, and it is a branching bisimulation if one has both t_{2} = t′ and sRt_{1}. Finally, it is a strong bisimulation if one has

sRt ∧ s →^{ξ} s′ implies ∃t′ : t →^{ξ} t′ ∧ s′Rt′.

Let s, w, d, b be abbreviations for strong, weak, delay and branching, and let ℵ range over {s, w, d, η, b}. Then two processes P, Q ∈ are ℵ(-bisimulation) equivalent—notation P \underline{↔}_{ℵ} Q—if there is a ℵ-bisimulation R with P RQ.

Following [17, 2], the above definitions depart from the standard approach followed in, e.g., [16] in that notions of bisimulation equivalence are defined that apply to open terms directly. Usually, bisimulation equivalences like those presented in Def. 2.1 are defined explicitly for closed process expressions only. Open process expressions are then regarded equivalent iff they are equivalent under any closed substitution of their (free) variables. In [2] it has been shown, for the language BCCS with prefix iteration, that both approaches yield the same equivalence relation over open terms. The same proof applies to BCCS^{f∗}. For this result it is essential that the set A of observable actions is nonempty.

The following lemma will be of use in the completeness proof for branching congruence (cf. the proof of Propn. 4.2). It is a standard result for branching bisimulation equivalence.

Lemma 2.2 (Stuttering Lemma [13]) If P_{0} →^{τ} ⋯ →^{τ} P_{n} and P_{n} \underline{↔}_{b} P_{0}, then P_{i} \underline{↔}_{b} P_{0} for i = 1, ..., n − 1.

The definition of \underline{↔}_{b} is equivalent to the one in [13], as follows immediately from the proof of the stuttering lemma in [13]. However, what is here introduced as a branching bisimulation was there called a semi branching bisimulation, whereas “branching bisimulation” was the name of a slightly more restrictive type of relation. The advantages of the current setup have been pointed out in [5].

Proposition 2.3 Each of the relations \underline{↔}_{ℵ} (ℵ ∈ \{s, b, η, d, w\}) is an equivalence relation and the largest ℵ-bisimulation. Furthermore, for all P, Q,

P \underline{↔}_{s} Q ⇒ P \underline{↔}_{b} Q ⇒ P \underline{↔}_{d} Q
⇓  ⇓
P \underline{↔}_{η} Q ⇒ P \underline{↔}_{w} Q.

Proof: For ℵ ∈ {s, b, η, d, w}, the identity relation, the converse of a ℵ-bisimulation and the symmetric closure of the composition of two ℵ-bisimulations are all ℵ-bisimu-lations. Hence \underline{↔}_{ℵ} is an equivalence relation. As pointed out in [5], for this argument to apply to branching bisimulations it is essential that the definition of a branching bisimulation is relaxed to that of a semi branching bisimulation.

That \underline{↔}_{ℵ} is the largest ℵ-bisimulation follows immediately from the observation that the set of ℵ-bisimulations is closed under arbitrary unions. The implications hold by definition. □

For s, t ∈ SF write s ≤ t if ∀α(s →^{α} ⇒ t →^{α}), and s \underline{↔} t if s ≤ t and t ≤ s.

It is easily checked that \underline{↔} is a congruence on sumforms in the sense that

if s\underline{↔} t then s + u\underline{↔} t + u, u + s\underline{↔} u + t, s.P \underline{↔}_{s} t.P, and s^{∗}P \underline{↔}_{s} t^{∗}P.

Likewise, \underline{↔}_{s} turns out to be a congruence on in the sense that

if P \underline{↔}_{s} Q then P +R \underline{↔}_{s} Q+R, R+P \underline{↔}_{s} R+Q, s.P \underline{↔}_{s} s.Q and s^{∗}P \underline{↔}_{s} s^{∗}Q.

However, for the standard reasons explained in, e.g., [16], none of the equivalences \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b} is a congruence with respect to +. In fact, also none of these equivalences is preserved by ^{∗} [2]. Following Milner [16], the solution to these congruence problems is by now standard; it is sufficient to consider, for each equivalence \underline{↔}_{ℵ}, the largest congruence over contained in it. These largest congruences can be explicitly characterized as follows.

Definition 2.4

• P and Q are branching congruent, written P \underline{↔}_{b}^{c} Q, iff for all ξ ∈ A_{τ} ∪ Var,

1. if P →^{ξ} P′, then Q →^{ξ} Q′ for some Q′ such that P′ \underline{↔}_{b} Q′;

2. if Q →^{ξ} Q′, then P →^{ξ} P′ for some P′ such that P′ \underline{↔}_{b} Q′.

• P and Q are η-congruent, written P \underline{↔}_{η}^{c} Q, iff for all ξ ∈ A_{τ} ∪ Var,

1. if P →^{ξ} P′, then Q →^{ξ} Q_{1} ⇒ Q′ for some Q_{1}, Q′ such that P′ \underline{↔}_{η} Q′;

2. if Q →^{ξ} Q′, then P →^{ξ} P_{1} ⇒ P′ for some P_{1}, P′ such that P′ \underline{↔}_{η} Q′.

• P and Q are delay congruent, written P \underline{↔}_{d}^{c} Q, iff for all ξ ∈ A_{τ} ∪ Var,

1. if P →^{ξ} P′, then Q ⇒ Q_{1} →^{ξ} Q′ for some Q_{1}, Q′ such that P′ \underline{↔}_{d} Q′;

2. if Q →^{ξ} Q′, then P ⇒ P_{1} →^{ξ} P′ for some P_{1}, P′ such that P′ \underline{↔}_{d} Q′.

• P and Q are weakly congruent, written P \underline{↔}_{w}^{c} Q, iff for all ξ ∈ A_{τ} ∪ Var,

1. if P →^{ξ} P′, then Q ⇒→^{ξ}⇒ Q′ for some Q′ such that P′ \underline{↔}_{w} Q′;

2. if Q →^{ξ} Q′, then P ⇒→^{ξ}⇒ P′ for some P′ such that P′ \underline{↔}_{w} Q′.

• Finally, strong congruence, denoted \underline{↔}_{s}^{c}, is the same as \underline{↔}_{s}.

Proposition 2.5 For every ℵ ∈ \{s, b, η, d, w\}, the relation \underline{↔}_{ℵ}^{c} is the largest congruence over contained in \underline{↔}_{ℵ}.

Proof: Exactly as in [2]. □

3 Axiom Systems

Table 1 presents the axiom system E_{s}, which will be shown to completely characterize strong congruence over BCCS^{f∗}. The entries in this table are axiom schemes in the sense that there is one axiom for every choice of the sumforms s, t, u. For an axiom system T , one writes T ⊢ P = Q iff the equation P = Q is provable from the axiom system T using the rules of equational logic. For a collection of equations X over the signature of BCCS^{f∗}, P =^{X} Q is used as a short-hand for A1–A4,X ⊢ P = Q. The axioms A1–4 are known to completely characterize the operator + of CCS. As this operator occurs both in sumforms and in process expressions, these axioms appear for each of the two sorts. It is easily checked that they are sound and complete for \underline{↔} on sumforms:

Proposition 3.1 s \underline{↔} t ⇔ A1–4 ⊢ s = t. Moreover, s ≤ t ⇔ A1–4 ⊢ t = t + s.

The axioms A5 and A6 are inspired by the ACP axioms for sequential composition [7], and the axiom FA1 stems from [10], where a form of iteration P^{∗}Q was used in which P had to be either an action, or a process (like 0) that cannot perform any actions. In [6] three axioms for general iteration in a process

A1  x + y = y + x  s + t = t + s
A2 (x + y) + z = x + (y + z)  (s + t) + u = s + (t + u)
A3  x + x = x  s + s = s
A4  x + 0 = x  s + 0 = s
A5  (s + t).x = s.x + t.x
A6  0.x = 0
FA1  0^{∗}x = x
FA2  s^{∗}(t.(s + t)^{∗}x + x) = (s + t)^{∗}x

Table 1: The axiom system E_{s}

algebra without 0 where proposed, called BKS1–3. These axioms where shown to be complete in [11]. The axiom BKS2 deals with the interaction between iteration and general sequential composition, and therefore has no counterpart in BCCS^{f∗}. My axiom FA2 is obtained from BKS3 by requiring the first argument in an expression P^{∗}Q to be a sumform. In the same spirit, the axiom BKS1 could be modified to t.(t^{∗}x) + x = t^{∗}x. This law is derivable from E_{s} by setting s = 0 in FA2. The remaining axiom a^{∗}(a^{∗}x) = a^{∗}x of [9] is derivable as well: take s = t in FA2 and apply BKS1 to the left-hand side.

In addition to the axioms in E_{s}, the axiom systems E_{ℵ} (ℵ ∈ {b, η, d, w}) include equations describing the various ways in which the congruences \underline{↔}_{ℵ}^{c} abstract away from internal actions τ. These equations are presented in Table 2. The axiom system E_{b} is obtained by adding the axioms FT1–2 to E_{s}, and E_{η} extends E_{b} with the equations T3 and FT3. The set of axioms E_{d} consists of the axioms of E_{s} together with T1 and FFIR. Finally, E_{w} extends E_{d} with T3 and FT3.

The equations T1 and T3 are standard laws for the silent action τ in weak congruence. Together with T2: τ.x = τ.x+x and the laws for strong congruence,

FT1  (s + τ)^{∗}x = τ.(s^{∗}x) + (s^{∗}x)
E_{b} FT2 α.s^{∗}(τ.s^{∗}(x + y) + x) = α.s^{∗}(x + y)

E_{η}

T3  α.(x + τ.y) = α.(x + τ.y) + α.y
FT3  s^{∗}(x + τ.y) = s^{∗}(x + τ.y + s.y)
E_{w}
T1  α.τ.x = α.x
FFIR  (s + τ)^{∗}x = τ.(s^{∗}x)  E_{d}

Table 2: Extra axioms for E_{η}, E_{b}, E_{d} and E_{w}

they are known to completely characterize weak congruence in the absence of iteration. Here T2 is derivable from E_{s} and FFIR (set s = 0 in FFIR and apply BKS1 on τ^{∗}x). Also the law α.(τ.(x + y) + x) = α.(x + y), which together with the laws for strong congruence characterizes branching bisimulation for BCCS without iteration, is derivable: just take s = 0 in FT2.

The four remaining axioms, which describe the interplay between τ and prefix iteration, are new here. The law FFIR is a generalization of the Fair Iteration Rule τ^{∗}x = τ.x (FIR_{1}) of [6], which is an equational formulation of Koomen’s Fair Abstraction Rule [4]. Like FIR, FFIR expresses that modulo weak (or delay) congruence a process remains the same if τ-loops are added (or deleted) in (or from) its proper derivatives. The law FT1 has the same function in branching (or η-)bisimulation semantics, but has to be formulated more carefully because T2 is not valid there. Note that FT1 can be reformulated as α.(s+τ)^{∗}x = α.s^{∗}x. The laws FT2 and FT3 are straightforward generalizations of the laws PB2 and PT3 of [2]. The remaining law PT2 of [2] is (by the forthcoming completeness theorem for \underline{↔}_{d}^{c}) derivable from the ones given here.

Note that even over a finite alphabet A there exist infinitely many sumforms. Hence the axiomatizations as given here are infinite. However, for each axiom scheme only the instantiations are needed in which the sumforms have the form ∑_{i=1}^{n} α_{i} in which all the α_{i}’s are different. With this modification each of the axiom systems E_{ℵ} (ℵ ∈ {s, b, η, d, w}) is finite if so is the set of actions A. If A is not finite, the axiomatizations can still be interpreted as finite ones, namely by replacing the actions α in FT2 and T2,3 by sumforms t, introducing variables that range over sumforms, and interpreting each entry in the resulting Tables 1–4 as a single axiom in which s, t and u are such variables.

The following states the soundness of the axiom systems.

Proposition 3.2 Let ℵ ∈ \{s, b, η, d, w\}. If E_{ℵ} ⊢ P = Q, then P \underline{↔}_{ℵ}^{c} Q.

Proof: As \underline{↔}_{ℵ}^{c} is a congruence, it is sufficient to show that each equation in E_{ℵ} is sound with respect to it. This is rather straightforward and left to the reader. □

As in [2], it can be shown that E_{w} ⊢ E_{d} ⊢ E_{b} ⊢ E_{s} and E_{w} ⊢ E_{η} ⊢ E_{b}, where T ⊢ T′ denotes that T ⊢ P = Q for every equation (P = Q) ∈ T′.

4 Completeness

This section is entirely devoted to detailed proofs of the completeness of the axiom systems E_{ℵ} (ℵ ∈ \{s, b, η, d, w\}) with respect to \underline{↔}_{ℵ}^{c} over the language of open terms . The first subsection contains the completeness proof for branching congruence. Its contents also apply to strong congruence if you read E_{s} for E_{b}, \underline{↔}_{s} for \underline{↔}_{b}, α for a, and α for (α) and skip the underlined and sidelined parts.

4.1 Completeness for strong \underline{and branching} congruence

First I identify a subset of process expressions of a special form, which will be convenient in the proof of the completeness result. Following a long-established tradition in the literature on process theory, these terms are referred to as normal forms. The set of normal forms is the smallest set of process expressions of the form

s^{∗}(∑_{i∈I} α_{i}.P_{i} + ∑_{j∈J} x_{j}),

where \underline{s ↛^{τ},} the terms P_{i} are themselves normal forms, and I, J are finite index sets. (Recall that the empty sum represents 0.)

Lemma 4.1 Each term in can be proven equal to a normal form using equations A1–6, FA1,2 \underline{and FT1}.

Proof: A straightforward induction on the structure of process expressions. The expressions x and 0 can be brought in the required form by a single application of FA1. Now suppose P and Q have the required form. Then s.P can be brought in normal form using A5 or A6 (possibly after applying A4 on s), followed by FA1. P +Q can be brought in normal form by first applying the derivable law t^{∗}x = t.(t^{∗}x) + x (BKS1) on each of P and Q, then A4–6 to rewrite the subterms t.(t^{∗}x), and concluding with FA1. Finally s^{∗}P is dealt with by applying BKS1 on P, again followed by A4–6. \underline{In case s →^{τ}, apply FT1, followed by another round of BKS1, A4–6 and FA1.} □

Note that this is the only place in the completeness proof where the axioms FA1 \underline{and FT1} are used. The following result is \underline{the key to} the completeness theorem.

Proposition 4.2 For all P, Q ∈ , if P \underline{↔}_{b} Q, then, \underline{∀γ ∈ A_{τ} :}E_{b} ⊢ \underline{γ.}P = \underline{γ.}Q.

Proof: First of all, note that, as the equations in E_{b} are sound with respect to \underline{↔}_{b}^{c}, and, a fortiori, with respect to \underline{↔}_{b}, by Lem. 4.1 it is sufficient to prove that the statement of the proposition holds for \underline{branching} equivalent normal forms P and Q. I do so by complete induction on the sum of the sizes of P and Q.

Let P = s^{∗}(∑_{i} α_{i}.P_{i} + ∑_{k} x_{k}) and Q = t^{∗}(∑_{j} β_{j}.Q_{j} + ∑_{l} y_{l}). Write P′ for ∑_{i} α_{i}.P_{i} +∑_{k} x_{k} and Q′ for ∑_{j} β_{j}.Q_{j} +∑_{l} y_{l}. Consider the following two conditions:

A. P_{i} \underline{↔}_{b} Q for some i; B. Q_{j} \underline{↔}_{b} P for some j.

I distinguish two cases in the proof, depending on which of these conditions hold.

I Suppose that both of A and B hold. In this case, there exist i and j such that P_{i} \underline{↔}_{b} Q \underline{↔}_{b} P \underline{↔}_{b} Q_{j}. Applying the inductive hypothesis to the equivalences P \underline{↔}_{b} Q_{j}, Q_{j} \underline{↔}_{b} P_{i} and P_{i} \underline{↔}_{b} Q, one infers that\underline{, for all γ ∈ A_{τ},}

E_{b} ⊢ \underline{γ.}P = \underline{γ.}Q_{j} = \underline{γ.}P_{i} = \underline{γ.}Q

II Suppose that at most one of A and B holds. Assume, without loss of generality, that B does not hold. Suppose s →^{a}. As P \underline{↔}_{b} Q, the transition P →^{a} P must be matched by a sequence

of transitions Q\underline{= Q_{0} →^{τ} Q_{1} →^{τ} ⋯ →^{τ} Q_{n}} →^{a} Q′′ with \underline{P \underline{↔}_{b} Q_{n} and} P \underline{↔}_{b} Q′′. As

condition B does not hold, \underline{using Lem. 2.2} it follows that \underline{n = 0,} Q′′ = Q and t →^{a}. Hence E_{b} ⊢ t = t + s by Prop. 3.1.

Let u = ∑ \{α_{i} | P_{i} \underline{↔}_{b} Q ∧ (t →^{α_{i}} \underline{∨α_{i} = τ})\} and v = ∑ \{α_{i} | P_{i} \underline{↔}_{b} Q ∧ t →^{α_{i}}\}.

Then E_{b} ⊢ t = t + v = t + s + v. For every summand α_{i}.P_{i} of P′ with P_{i} \underline{↔}_{b} Q, induction yields E_{b} ⊢ α_{i}.P_{i} = α_{i}.Q. Hence, using axiom A5 to assemble all such summands with u →^{α_{i}}, and possibly using A4 and/or A6 if there are no or only such summands, one infers that

E_{b} ⊢ P = s^{∗}(u.Q + S)

where S = ∑ \{α_{i}.P_{i} | P_{i}\underline{↮}_{b} Q ∨ (t ↛^{α_{i}} \underline{∧α_{i} ≠ τ})\} + ∑_{k} x_{k}.

Consider now a summand α_{i}.P_{i} of S. As P \underline{↔}_{b} Q, the transition P →^{α_{i}} P_{i} must

be matched by a sequence Q\underline{= Q_{0} →^{τ} Q_{1} →^{τ} ⋯ →^{τ} Q_{n}} →^{(α_{i})} Q′′ with \underline{P \underline{↔}_{b} Q_{n} and}

P_{i} \underline{↔}_{b} Q′′. \underline{As condition B does not hold, using Lem. 2.2 it follows that n = 0.}

Furthermore, the possibility Q →^{(α_{i})} Q \underline{↔}_{b} P_{i} is ruled out by the construction of S. Hence, each summand α_{i}.P_{i} of S matches with a summand β_{j}.Q_{j} of Q′, in the sense that α_{i} = β_{j} and P_{i} \underline{↔}_{b} Q_{j}. For each such pair of related summands, induction yields

E_{b} ⊢ α_{i}.P_{i} = α_{i}.Q_{j} = β_{j}.Q_{j} .

Moreover, each summand x_{k} of S must be a summand of Q′. Hence, possibly using axiom A3, it follows that E_{b} ⊢ Q′ = Q′+ S. \underline{Now I distinguish two sub-cases.}

IIa \underline{Suppose that A does not hold for an index i with α_{i} = τ.} Again \underline{using Lem. 2.2,} it follows that every summand β_{j}.Q_{j} of Q′ matches with a summand α_{i}.P_{i} of S (since also B does not hold, the cases Q_{j} \underline{↔}_{b} P and Q_{j} \underline{↔}_{b} Q \underline{↔}_{b} P do not apply), and every y_{l} is equal to an x_{k}. Possibly using axiom A3, it follows that E_{b} ⊢ S = Q′ + S = Q′. Moreover, whenever t →^{a} then Q →^{a} Q, so P →^{a} P′′ \underline{↔}_{b} Q and hence either s →^{a} or v →^{a}. It follows that E_{b} ⊢ t = s + v. Finally u = v, so

\underline{γ.}P = \underline{γ.}s^{∗}(v.Q + S) = \underline{γ.}s^{∗}(v.(s + v)^{∗}S + S) =^{FA2} \underline{γ.}(s + v)^{∗}S = \underline{γ.}Q.

IIb Suppose that A holds for an index i with α_{i} = τ. Then E_{b} ⊢ u = τ + v, so

γ.P =^{A5} γ.s^{∗}(τ.Q + v.Q + S)
= γ.s^{∗}(τ.t^{∗}(Q′ + S) + v.t^{∗}(Q′ + S) + S)
=^{FA2} γ.s^{∗}(τ.s^{∗}(t.(s + t)^{∗}(Q′ + S) + Q′ + S) + v.t^{∗}(Q′ + S) + S)
= γ.s^{∗}(τ.s^{∗}(Q′ + (t + v).t^{∗}(Q′ + S) + S) + v.t^{∗}(Q′ + S) + S)
=^{FT2, A5} γ.s^{∗}(Q′ + (t + v).t^{∗}(Q′ + S) + S)
=^{FA2} γ.t^{∗}(Q′ + S) = γ.Q.

The proof of the inductive step is now complete. □

Theorem 4.3 Let P, Q ∈ . If P \underline{↔}_{b}^{c} Q, then E_{b} ⊢ P = Q.

Proof: Consider two process expressions P and Q that are branching congruent. Using the same technique as in the proof of Lem. 4.1, one may derive that

\begin{matrix}E_{b} ⊢ P = ∑ \{α_{i}.P_{i} | i ∈ I\} + ∑ \{x_{j} | j ∈ J\} and \\ E_{b} ⊢ Q = ∑ \{β_{k}.Q_{k} | k ∈ K\} + ∑ \{y_{l} | l ∈ L\} \end{matrix}

for some finite index sets I, J, K, L. As P \underline{↔}_{b}^{c} Q, it follows that 1. for every i ∈ I there exists an index k_{i} ∈ K such that α_{i} = β_{k_{i}} and P_{i} \underline{↔}_{b} Q_{k_{i}},

2. and for every j ∈ J there exists an index l_{j} ∈ L such that x_{j} = y_{l_{j}}. By Propn. 4.2, for every i ∈ I one may infer that

E_{b} ⊢ α_{i}.P_{i} = α_{i}.Q_{k_{i}} = β_{k_{i}}.Q_{k_{i}} .

Using A3 it follows immediately that E_{b} ⊢ Q = P + Q. By symmetry one obtains E_{b} ⊢ P = P + Q = Q. □

4.2 Completeness for η-, delay, and weak congruence

I now proceed to derive completeness results for η-, delay, and weak congruence from the ones for strong and branching congruence. The key to this derivation is the observation that, for certain classes of process expressions, these congruence relations coincide with \underline{↔}_{s} or \underline{↔}_{b}^{c}. These classes of process expressions are defined below.

Definition 4.4 A term P is:

• η-saturated iff for each of its derivatives Q, R and S and ξ ∈ A_{τ} ∪ Var one

has that:

Q →^{ξ} R →^{τ} S implies Q →^{ξ} S.

• d-saturated iff for each of its derivatives Q, R and S and ξ ∈ A_{τ} ∪ Var one

has that:

Q →^{τ} R →^{ξ} S implies Q →^{ξ} S.

• w-saturated iff it is both η- and d-saturated.

• strongly ℵ-saturated (for ℵ ∈ {η, d, w}) if it is ℵ-saturated and for each of its proper derivatives Q ∈ pder(P) there is a τ-loop Q →^{τ} Q.

The following was first observed in [13] for process graphs.

Theorem 4.5

1. If P and Q are ℵ-saturated, ℵ ∈ \{η, d, w\}, and P \underline{↔}_{ℵ}^{c} Q, then P \underline{↔}_{b}^{c} Q.

2. If P and Q are strongly ℵ-saturated, ℵ∈\{d, w\}, and P \underline{↔}_{ℵ}^{c} Q, then P \underline{↔}_{s} Q.

Proof: In case 1, the relation

B =^{def} \{(S, T) | S \underline{↔}_{ℵ} T, S, T ℵ-saturated\}

is a branching bisimulation. From this it follows easily (as shown in [2]) that P \underline{↔}_{ℵ}^{c} Q implies P \underline{↔}_{b}^{c} Q. In case 2, B is a strong bisimulation. □

Note that the second statement does not apply to \underline{↔}_{η}^{c}. A counterexample concerns the terms P = a.τ^{∗}τ.τ^{∗}b.τ^{∗}0 + a.τ^{∗}b.τ^{∗}0 and Q = a.τ^{∗}b.τ^{∗}0. These terms are strongly η-saturated and P \underline{↔}_{η}^{c} Q, but P \underline{↮}_{s} Q.

Theorem 4.6 Let ℵ ∈ {η, d, w}.

1. For each term P, E_{ℵ} ⊢ P = P′ for some ℵ-saturated term P′.

2. For each term P, E_{ℵ} ⊢ P = P′′ for some strongly ℵ-saturated term P′′.

Proof: The first statement has been shown in [2] for the language BCCS^{p∗}. The resulting term P′ has the form P′ = ∑_{i∈I} α_{i}.P_{i} + ∑_{j∈J} x_{j}. The same proof applies here.

For the second result, first prove P equal to a term P′ as above, and bring the subterms P_{i} for i ∈ I in normal form, using Lem. 4.1. Now each proper derivative of the resulting term has the form s^{∗}Q, and appears in a subterm of the form α.s^{∗}Q. In combination with T1, the axiom FFIR derives α.s^{∗}x = α.(s + τ)^{∗}x. As mentioned before, this law is also derivable from E_{b}. Applying this law to all subterms of the form α.s^{∗}Q results in a term P′′ that is still ℵ-saturated, and for which each proper derivative Q has a τ-loop Q →^{τ} Q. □

The results in Thms. 4.5.1 and 4.6.1 effectively reduce the completeness problem for η-, delay, and weak congruence over to that for branching congruence.

Corollary 4.7 Let ℵ ∈ \{η, d, w\}. If P \underline{↔}_{ℵ}^{c} Q, then E_{ℵ} ⊢ P = Q.

Proof (for the case ℵ = η): Suppose that P \underline{↔}_{ℵ}^{c} Q. Prove P and Q equal to ℵ-saturated processes P′ and Q′, respectively (Thm. 4.6.1). By the soundness of the axiom system E_{ℵ} (Propn. 3.2), P′ and Q′ are ℵ-congruent. It follows that P′ and Q′ are branching congruent (Thm. 4.5.1). Hence, by Thm. 4.3, E_{b} ⊢ P′ = Q′. The claim now follows because E_{b} ⊂ E_{η}. □

The cases ℵ = d and ℵ = w can be proved in the same way, using in the last step that E_{w} ⊢ E_{d} ⊢ E_{b} ⊢ P = Q (cf. the last sentence of Section 3). However, Thms. 4.5.2 and 4.6.2 allow a simpler proof that doesn’t need the completeness result for branching bisimulation as an intermediate step, but instead reduces the problem to the completeness for strong congruence.

Proof of Corollary 4.7 (for the cases ℵ ∈ \{d, w\}): Suppose that P \underline{↔}_{ℵ}^{c} Q. Prove P and Q equal to strongly ℵ-saturated processes P′ and Q′, respectively (Thm. 4.6.2). By the soundness of the axiom system E_{ℵ} (Propn. 3.2), P′ and Q′ are ℵ-congruent. It follows that P′ and Q′ are strong congruent (Thm. 4.5.2). Hence, by Prop. 4.2 for strong congruence, E_{s} ⊢ P′ = Q′. The claim now follows because E_{s} ⊂ E_{ℵ}. □

5 Prefix Iteration

In this section I derive complete axiomatizations for prefix iteration from the ones for flat iteration. A BCCS^{f∗} process expression is a BCCS^{p∗} expression iff in each subexpression s.P or s^{∗}P, the sumform s consists of a single action α ∈ A_{τ}. The following result about the expressiveness of BCCS^{p∗} stems from [3].

Lemma 5.1 If P_{0} is a BCCS^{p∗} expression and P_{n} ⇒→^{a_{n}} P_{n+1} for n = 0, 1, 2, ..., then there is an N such that a_{n} = a_{N} for n > N.

Definition 5.2 A BCCS^{f∗} expression P_{0} is a potential BCCS^{p∗} expression if every sequence P_{n} ⇒→^{a_{n}} P_{n+1} (n = 0, 1, 2, ...) has the property of Lem. 5.1.

It is easy to see that a potential BCCS^{p∗} expression can not be weakly equivalent to an expression that is not so. Hence, using Propn. 3.2 (soundness):

Lemma 5.3 Let ℵ ∈ {s, b, η, d, w}. If E_{ℵ} ⊢ P = Q then either both P and Q are potential BCCS^{p∗} expressions, or neither of them is.

Using structural induction, the following Lemma is straightforward:

Lemma 5.4 If s^{∗}P is a subterm of a potential BCCS^{p∗} expression, then either A1–4 ⊢ s = 0 or A1–4 ⊢ s = α ∈ A_{τ} or A1–4 ⊢ s = a + τ with a ∈ A. Moreover, these alternatives are mutually exclusive.

Let R be the rewrite system consisting of the axioms A5, A6, FA1 and FT1, read from left to right. As these rewrite rules have no overlapping redexes, R is confluent, and it is equally straightforward to see that it is terminating. Now let φ be the operator on potential BCCS^{p∗} expressions P that first converts any sumform s in a subterm s^{∗}Q of P into one of the forms 0, α or a + τ (using A1–4 and Lem. 5.4), and subsequently brings the resulting term in normal form w.r.t. R. Note that the resulting term φ(P) is a BCCS^{p∗} expression.

Theorem 5.5 Let ℵ ∈ {b, η, d, w}. The theory

φ(E_{ℵ}) = {φ(P) = φ(Q) | (P = Q) ∈ E_{ℵ}}

is a complete axiomatization of \underline{↔}_{ℵ}^{c} over the language BCCS^{p∗}.

Proof: An equation P = Q is provable in equational logic iff there exists a sequence T_{0}, ..., T_{n} with P = T_{0}, Q = T_{n}, and the equation T_{i−1} = T_{i} is obtained from one axiom by means of substitution, placement in a context and (possibly) symmetry (i = 1, ..., n). Suppose that P \underline{↔}_{ℵ}^{c} Q for certain BCCS^{p∗} expressions P and Q. As P and Q are also BCCS^{f∗} expressions, this implies E_{ℵ} ⊢ P = Q. Thus, by Lem. 5.3, there exists a proofsequence as mentioned above in which all the T_{i} are potential BCCS^{p∗} expressions. Now, for i = 1, ..., n, the equation φ(T_{i−1}) = φ(T_{i}) can be obtained from an axiom in φ(E_{ℵ}) by means of substitution, placement in a context and symmetry. This yields a proof-sequence for the equation φ(P) = φ(Q). However, since P and Q are BCCS^{p∗} expressions, φ(P) = P and φ(Q) = Q. Hence φ(E_{ℵ}) ⊢ P = Q. □

In the axiom systems φ(E_{ℵ}), the axioms A5, A6 and FA1 evaluate to identities, whereas the axioms A1–4, T1 and T3 remain unchanged. Furthermore, there are three axioms corresponding to each of FT1–3 and FFIR, depending on whether s evaluates to 0, α, or a + τ, and nine corresponding to FA2, depending on how s and t evaluate. All resulting axiomatizations turn out to be derivable from the corresponding axiomatizations in [2] and vice versa. Hence the above constitutes an alternative proof of the completeness results in [2].

A similar result can be obtained for ℵ = s, but in that case τ should be treated as a normal action, and FT1 should be omitted from the rewrite system.

6 Parallelism

Complete axiomatizations of strong and weak bisimulation congruence over full CCS without recursion or iteration were given in [14]. The strategy, in both cases, was to prove every such CCS expression strongly equivalent to a BCCS expression, using the well known expansion theorem, and then apply the relevant completeness theorem for BCCS expressions. This method does not work in the setting of prefix iteration, as the parallel composition of two BCCS^{p∗} expressions need not be (weakly) equivalent to a BCCS^{p∗} expression. A simple counterexample concerns the expression a^{∗}0 | b^{∗}0, which is not a potential BCCS^{p∗} expression in the sense of Def. 5.2. However, an expansion theorem for CCS^{f∗} poses no problem: let P = s^{∗} ∑_{i∈I} α_{i}.P_{i} and Q = t^{∗} ∑_{j∈J} β_{j}.Q_{j}, then

P | Q\underline{↔}_{s} (s + t + γ)^{∗}(∑_{i∈I} α_{i}.(P_{i} | Q) + ∑_{j∈J} β_{j}.(P | Q_{j}) + C)

with

C = ∑_{α_{i}=\overline{β_{j}}} τ.(P_{i} | Q_{j}) + ∑_{i∈I, t→^{\overline{α_{i}}}} τ.(P_{i} | Q) + ∑_{j∈J, s→^{\overline{β_{j}}}} τ.(P | Q_{j})

and γ = \{ \begin{matrix}τ & if there is an a ∈ A with s →^{a} and t →^{a} \\ 0 & otherwise. \end{matrix}

For a parallel composition without communication just leave out γ and C; in this shape the theorem was first found in [6].

In the presence of a CSP-style parallel composition in which processes are forced to synchronize over a shared alphabet [18], closed expressions with flat iteration can be expressed in terms of prefix iteration. An expression

(a + b)^{∗}(c.P + d.Q)

for instance, in which c and d do not occur in P and Q, is strongly equivalent to

a^{∗}(c.0 + d.0)∥_{{c,d}}b^{∗}(c.P + d.Q)

where synchronization over c and d is enforced. In the general case renaming operators are needed as well.

Acknowledgment The inspiration to write this paper originated from the fruitful collaboration with Luca Aceto, Wan Fokkink and Anna Ingólfsdóttir in [2]. The referees are thanked for careful proofreading, and correcting the expansion theorem above.

References

[1] L. Aceto and J.F. Groote (1995), A complete equational axiomatization for MPA with string iteration, BRICS Research Report RS-95-28, Department of Mathematics and Computer Science, Aalborg University. Available by anonymous

    ftp from ftp.daimi.aau.dk in the directory pub/BRICS/RS/95/28.

[2] L. Aceto, W. Fokkink, R. van Glabbeek and A. Ingólfsdóttir (1996), Axiomatizing prefix iteration with silent steps, I&C 127(1), pp. 26–40.

[3] L. Aceto and A. Ingólfsdóttir (1996), An equational axiomatization of observation congruence for prefix iteration, in Proc. AMAST ’96, Munich, Germany, M. Wirsing and M. Nivat, eds., LNCS 1101, Springer-Verlag, pp. 195–209.

[4] J. Baeten, J. Bergstra and J. Klop (1987), On the consistency of Koomen’s fair abstraction rule, TCS 51, pp. 129–176.

[5] T. Basten (1996), Branching bisimilarity is an equivalence indeed!, IPL 58(3), pp. 141–147.

[6] J. Bergstra, I. Bethke and A. Ponse (1994), Process algebra with iteration and nesting, Computer Journal 37, pp. 243–258. Originally appeared as report P9314, Programming Research Group, University of Amsterdam, 1993.

[7] J. Bergstra and J. Klop (1984), The algebra of recursively defined processes and the algebra of regular processes, in Proceedings 11^{th} ICALP, Antwerpen, J. Paredaens, ed., LNCS 172, Springer-Verlag, pp. 82–95.

[8] F. Corradini, R. De Nicola and A. Labella (1995), Fully abstract models for nondeterministic Kleene algebras (extended abstract), in Proc. CONCUR 95, Philadelphia, I. Lee and S. Smolka, eds., LNCS 962, Springer-Verlag, pp. 130–144.

[9] W. Fokkink (1994), A complete equational axiomatization for prefix iteration, IPL 52, pp. 333–337.

[10] W. Fokkink (1996), A complete axiomatization for prefix iteration in branching bisimulation, Fundamenta Informaticae 26, pp. 103–113.

[11] W. Fokkink and H. Zantema (1994), Basic process algebra with iteration: Completeness of its equational axioms, Computer Journal 37, pp. 259–267.

[12] R. v. Glabbeek (1995), Branching bisimulation as a tool in the analysis of weak

bisimulation. Available at ftp://boole.stanford.edu/pub/DVI/tool.dvi.gz.

[13] R. v. Glabbeek and W. Weijland (1996), Branching time and abstraction in bisimulation semantics, JACM 43(3), pp. 555–600.

[14] M. Hennessy and R. Milner (1985), Algebraic laws for nondeterminism and concurrency, JACM 32, pp. 137–161.

[15] S. Kleene (1956), Representation of events in nerve nets and finite automata, in Automata Studies, C. Shannon and J. McCarthy, eds., Princeton University Press, pp. 3–41.

[16] R. Milner (1989), Communication and Concurrency, Prentice-Hall.

[17] R. Milner (1989), A complete axiomatisation for observational congruence of finite-state behaviours, I&C 81, pp. 227–247.

[18] E.-R. Olderog and C.A.R. Hoare (1986), Specification-oriented semantics for communicating processes, Acta Informatica 23, pp. 9–66.

[19] P. Sewell (1994), Bisimulation is not finitely (first order) equationally axiomatisable, in Proc. 9^{th} LICS, Paris, IEEE Computer Society Press, pp. 62–70.