BRICS RS-04-1 Aceto et al.: Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy’s Merge BRICS

Basic Research in Computer Science

Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy’s Merge

Luca Aceto Willem Jan Fokkink Anna Ingólfsdóttir Bas Luttik

BRICS Report Series RS-04-1

ISSN 0909-0878 January 2004 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, Luca Aceto & Willem Jan Fokkink & Anna

Ingólfsdóttir & Bas Luttik. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/04/1/

Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy’s Merge

Luca Aceto^{∗}

BRICS, Department of Computer Science

Aalborg University 9220 Aalborg Ø, Denmark

     Email: luca@cs.auc.dk

Wan Fokkink

CWI, Department of Software Engineering, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands

       Email: wan@cwi.nl

Anna Ingólfsdóttir

BRICS, Department of Computer Science

Aalborg University 9220 Aalborg Ø, Denmark

     Email: annai@cs.auc.dk

Bas Luttik

Department of Mathematics and Computer Science

Eindhoven Technical University

P.O. Box 513, 5600 MB Eindhoven, The Netherlands

   Email: luttik@win.tue.nl

Abstract

This note shows that split-2 bisimulation equivalence (also known as timed equivalence) affords a finite equational axiomatization over the process algebra obtained by adding an auxiliary operation proposed by Hennessy in 1981 to the recursion free fragment of Milner’s Calculus of Communicating Systems. Thus the addition of a single binary operation, viz. Hennessy’s merge, is sufficient for the finite equational axiomatization of parallel composition modulo this non-interleaving equivalence. This result is in sharp contrast to a theorem previously obtained by the same authors to the effect that the same language is not finitely based modulo bisimulation equivalence.

∗Partially supported by the Statens Naturvidenskabelige Forskningsråd (Danish Natural Science Research Council), project “The Equational Logic of Parallel Processes”, nr. 21-03-0342.

2000 Mathematics Subject Classification: 08A70, 03B45, 03C05, 68Q10, 68Q45, 68Q55, 68Q70. CR Subject Classification (1991): D.3.1, F.1.1, F.1.2, F.3.2, F.3.4, F.4.1. Keywords and Phrases: Concurrency, process algebra, CCS, bisimulation, split-2 bisimulation, non-interleaving equivalences, Hennessy’s merge, left merge, communication merge, parallel composition, equational logic, complete axiomatizations, finitely based algebras.

1 Introduction

This note offers a contribution to the fascinating study of equational characterizations of the parallel composition operation modulo (variations on) the classic notion of bisimulation equivalence [14, 19]. In particular, we provide a finite equational axiomatization of split-2 bisimulation equivalence—a notion of bisimulation equivalence based on the assumption that actions have observable beginnings and endings [9, 10, 11]—over the recursion, relabelling and restriction free fragment of Milner’s CCS [14] enriched with an auxiliary operator proposed by Hennessy in a 1981 preprint entitled “On the relationship between time and interleaving” and its published version [11]. To put this contribution, and its significance, in its research context, we find it appropriate to recall briefly some of the key results in the history of the study of equational axiomatizations of parallel composition in process algebra.

Research on equational axiomatizations of behavioural equivalences over process algebras incorporating a notion of parallel composition can be traced at least as far back as the seminal paper [12], where Hennessy and Milner offered, amongst a wealth of other classic results, a complete equational axiomatization of bisimulation equivalence over the recursion free fragment of CCS. (See the paper [5] for a more detailed historical account highlighting, e.g., Hans Bekić’s early contributions to this field of research.) The axiomatization given by Hennessy and Milner in that paper dealt with parallel composition using the so-called expansion law— an axiom schema with a countably infinite number of instances that is essentially an equational formulation of the Plotkin-style rules describing the operational semantics of parallel composition. This raised the question of whether the parallel composition operator could be axiomatized in bisimulation semantics by means of a finite collection of equations. This question was answered positively by Bergstra and Klop, who gave in [8] a finite equational axiomatization of the merge operator in terms of the auxiliary left merge and communication merge operators. Moller clarified the key role played by the expansion law in the axiomatization of parallel composition over CCS by showing in [16, 17, 18] that strong bisimulation equivalence is not finitely based over CCS and PA without the left merge operator. Thus auxiliary operators like the ones used by Bergstra and Klop are indeed necessary to obtain a finite axiomatization of parallel composition. Moreover, Moller proved in [16, 17] that his negative result holds true for each “reasonable congruence” that is included in standard bisimulation equivalence. In particular, this theorem of Moller’s applies to split-2 bisimulation equivalence since that equivalence is “reasonable” in Moller’s technical sense.

In his paper [11], Hennessy proposed an axiomatization of observation congruence [12] (also known as rooted weak bisimulation equivalence) and timed congruence (essentially rooted weak split-2 bisimulation equivalence) over a CCS-like recursion free process language. Those axiomatizations used an auxiliary operator, denoted |^{/} by Hennessy, that is essentially a combination of Bergstra and Klop’s left and communication merge operators. Apart from having soundness problems (see the reference [1] for a general discussion of this problem, and corrected proofs of Hennessy’s results), the proposed axiomatization of observation congruence offered in op. cit. is infinite, as it used a variant of the expansion theorem from [12]. Confirming a conjecture by Bergstra and Klop in [8, page 118], and answering problem 8 in [2], we showed in [3] that the language obtained by adding Hennessy’s merge to CCS does not afford a finite equational axiomatization modulo bisimulation equivalence. This is due to the fact that, in strong bisimulation semantics, no finite collection of equations can express the interplay between interleaving and communication that underlies the semantics of Hennessy’s merge. Technically, this is captured in our proof of the main result in [3] by showing that no finite collection of axioms that are valid in bisimulation semantics can prove all of the equations in the following family:

a0 |^{/} ∑_{i=0}^{n} āa^{i} ≈ a ∑_{i=0}^{n} āa^{i} + ∑_{i=0}^{n} τa^{i} (n ≥ 0) .

In split-2 semantics, however, these equations are not sound, since they express some form of interleaving. Indeed, we prove that, in sharp contrast to the situation in standard bisimulation semantics, Hennessy’s merge can be finitely axiomatized modulo split-2 bisimulation equivalence, and its use suffices to yield a finite axiomatization of the parallel composition operation. This shows that “reasonable congruences” finer than standard bisimulation equivalence can be finitely axiomatized over CCS using Hennessy’s merge as the single auxiliary operation—compare with the non-finite axiomatizability results for these congruences offered in [16, 17].

The paper is organized as follows. We begin by presenting preliminaries on the language CCS_{H}—the extension of CCS with Hennessy’s merge operator—and split-2 bisimulation equivalence in Sect. 2. We then offer a finite equational axiom system for split-2 bisimulation equivalence over CCS_{H}, and prove that it is sound and complete (Sect. 3).

This is a companion paper to [3], where the interested readers may find further motivation and more references to related literature. However, we have striven to make it readable independently of that paper. Some familiarity with [1, 11] and the basic notions on process algebras and bisimulation equivalence will be helpful, but is not necessary, in reading this study. The uninitiated reader is referred to the textbooks [6, 14] for extensive motivation and background on process algebras. Precise pointers to material in [1, 11] will be given whenever necessary.

2 The language CCS_{H}

The language for processes we shall consider in this paper, henceforth referred to as CCS_{H}, is obtained by adding Hennessy’s merge operator from [11] to the recursion, restriction and relabelling free subset of Milner’s CCS [14]. This language is given by the following grammar:

p ::= 0 | μp | p + p | p | p | p |^{/} p ,

where μ ranges over a set of actions A. We assume that A has the form {τ}∪Λ∪Λ̄, where Λ is a given set of names, Λ̄ = {ā | a ∈ Λ} is the set of complement names, and τ is a distinguished action. Following Milner [14], the action symbol τ will result from the synchronized occurrence of the complementary actions a and ā. We let a, b range over the set of visible actions Λ∪Λ̄. As usual, we postulate that ¯ ā = a for each name a ∈ Λ. We shall use p, q, r to range over process terms. The size of a term is the number of operation symbols in it. Following standard practice in the literature on CCS and related languages, trailing 0’s will often be omitted from terms.

The structural operational semantics for the language CCS_{H} given by Hennessy in [11, Sect. 2.1] is based upon the idea that visible actions have a beginning and an ending. Moreover, for each visible action a, these distinct events may be observed, and are denoted by S(a) and F (a), respectively. We define

E = A ∪ {S(a), F (a) | a ∈ Λ ∪ Λ̄} .

In the terminology of [11], this is the set of events, and we shall use e to range over it. As usual, we write E^{∗} for the collection of finite sequences of events.

Table 1: SOS Rules for S (μ ∈ A, a ∈ Λ ∪ Λ̄ and e ∈ E)

\overline{ap ⟶^{S(a)} a_{S}p}  \overline{a_{S}p ⟶^{F (a)} p}  \overline{μp ⟶^{μ} p}

\frac{p ⟶^{e} s}{p + q ⟶^{e} s}  \frac{q ⟶^{e} s}{p + q ⟶^{e} s}

\frac{s ⟶^{e} s′}{s | t ⟶^{e} s′ | t}  \frac{t ⟶^{e} t′}{s | t ⟶^{e} s | t′}  \frac{s ⟶^{a} s′, t ⟶^{ā} t′}{s | t ⟶^{τ} s′ | t′}

\frac{p ⟶^{e} s}{p |^{/} q ⟶^{e} s | q}  \frac{p ⟶^{a} p′, q ⟶^{ā} q′}{p |^{/} q ⟶^{τ} p′ | q′}

The operational semantics for the language CCS_{H} is given in terms of binary next-state relations ⟶^{e}, one for each event e ∈ E. As explained in [11], the relations ⟶^{e} are defined over the set of states S, an extension of CCS_{H} obtained by adding new prefixing operations a_{S} (a ∈ Λ ∪ Λ̄) to the signature for CCS_{H}. More formally, the set of states is given by the following grammar:

s ::= p | a_{S}p | s | s ,

where p ranges over CCS_{H}. Intuitively, a state of the form a_{S}p is one in which the execution of action a has started, but has not terminated yet. We shall use s, t to range over the set of states S.

The Plotkin style rules for the language S are given in Table 1; comments on these rules may be found in [11, Sect. 2.1].

Definition 2.1 For a sequence of events σ = e_{1} ⋯ e_{k} (k ≥ 0), and states s, s′, we write s ⟶^{σ} s′ iff there exists a sequence of transitions

s = s_{0} ⟶^{e_{1}} s_{1} ⟶^{e_{2}} ⋯ ⟶^{e_{k}} s_{k} = s′ .

If s ⟶^{σ} s′ holds for some state s′, then σ is a trace of s.

The depth of a state s, written depth(s), is the length of the longest trace it affords.

In this paper, we shall consider the language CCS_{H}, and more generally the set of states S, modulo split-2 bisimulation equivalence [4, 9, 11]. (The weak variant of this relation is called t-observational equivalence by Hennessy in [11]. Later on, this relation has been called timed equivalence in [4]. Here we adopt the terminology introduced by van Glabbeek and Vaandrager in [9].)

Definition 2.2 Split-2 bisimulation equivalence, denoted by \underline{↔}_{2S} , is the largest symmetric relation over S such that whenever s \underline{↔}_{2S} t and s ⟶^{e} s′, then there is a transition t ⟶^{e} t′ with s′ \underline{↔}_{2S} t′.

We shall also sometimes refer to \underline{↔}_{2S} as split-2 bisimilarity. If s \underline{↔}_{2S} t, then we say that s and t are split-2 bisimilar.

In what follows, we shall mainly be interested in \underline{↔}_{2S} as it applies to the language CCS_{H}. The interested reader is referred to [11, Sect. 2.1] for examples of (in)equivalent terms with respect to \underline{↔}_{2S} . Here, we limit ourselves to remarking that \underline{↔}_{2S} is a non-interleaving equivalence. For example, the reader can easily check that

a | b \underline{↔}_{2S} / a | b + ab \underline{↔}_{2S} / ab + ba .

It is well-known that split-2 bisimulation equivalence is indeed an equivalence relation. Moreover, two split-2 bisimulation equivalent states afford the same finite non-empty set of traces, and have therefore the same depth.

The following result can be shown following standard lines—see, e.g., [4].

Fact 2.1 Split-2 bisimilarity is a congruence over the language CCS_{H}. Moreover, for all states s, s′, t, t′, if s \underline{↔}_{2S} s′ and t \underline{↔}_{2S} t′, then s | t \underline{↔}_{2S} s′ | t′.

A standard question a process algebraist would ask at this point, and the one that we shall address in the remainder of this paper, is whether split-2 bisimulation equivalence affords a finite equational axiomatization over the language CCS_{H}. As we showed in [3], standard bisimulation equivalence is not finitely based over the language CCS_{H}. In particular, we argued ibidem that no finite collection of equations over CCS_{H} that is sound with respect to bisimulation equivalence can prove all of the equations

e_{n} : a0 |^{/} p_{n} ≈ ap_{n} + ∑_{i=0}^{n} τa^{i} (n ≥ 0) ,  (1)

where a^{0} denotes 0, a^{m+1} denotes a(a^{m}), and the terms p_{n} are defined thus:

p_{n} = ∑_{i=0}^{n} āa^{i} (n ≥ 0) .

Note, however, that none of the equations e_{n} holds with respect to \underline{↔}_{2S} . In fact, for each n ≥ 0, the transition

ap_{n} + ∑_{i=0}^{n} τa^{i} ⟶^{S(a)} a_{S}p_{n}

Table 2: The Axiom System E for CCS_{H} Modulo \underline{↔}_{2S}
A1  x + y ≈ y + x
A2  (x + y) + z ≈ x + (y + z)
A3  x + x ≈ x
A4  x + 0 ≈ x
HM1  (x + y) |^{/} z ≈ x |^{/} z + y |^{/} z
HM2  (x |^{/} y) |^{/} z ≈ x |^{/} (y | z)
HM3  x |^{/} 0 ≈ x
HM4  0 |^{/} x ≈ 0
HM5  (τx) |^{/} y ≈ τ(x | y)
HM6 ax |^{/} ((āy |^{/} w) + z) ≈ ax |^{/} ((āy |^{/} w) + z) + τ(x | y | w)
M  x | y ≈ (x |^{/} y) + (y |^{/} x)

cannot be matched, modulo \underline{↔}_{2S} , by the term a0 |^{/} p_{n}. Indeed, the only state reachable from a0 |^{/} p_{n} via an S(a)-labelled transition is a_{S}0 | p_{n}. This state is not split-2 bisimilar to a_{S}p_{n} because it can perform the transition

a_{S}0 | p_{n} ⟶^{S(ā)} a_{S}0 | ā_{S}0 ,

whereas the only initial event a_{S}p_{n} can embark in is F (a). Thus the family of equations on which our proof of the main result from [3] was based is unsound with respect to split-2 bisimilarity. Indeed, as we shall show in what follows, split-2 bisimilarity affords a finite equational axiomatization over the language CCS_{H}, if the set of actions A is finite. Hence it is possible to finitely axiomatize split-2 bisimilarity over CCS using a single auxiliary binary operation, viz. Hennessy’s merge.

3 An Axiomatization of Split-2 Bisimilarity over CCS_{H}

Let E denote the collection of equations in Table 2. In those equations the symbols x, y, w, z are variables. Equation HM6 is an axiom schema describing one equation per visible action a. Note that E is finite, if so is A.

We write E ⊢ p ≈ q, where p, q are terms in the language CCS_{H} that may possibly contain occurrences of variables, if the equation p ≈ q can be proven from those in E using the standard rules of equational logic. For example, using axioms A1, A2, A3, M, HM1 and HM2, it is possible to derive the equations:

x | 0 ≈ x  (2)
0 | x ≈ x  (3)
x | y ≈ y | x and  (4)
(x | y) | z ≈ x | (y | z)  (5)

that state that, modulo \underline{↔}_{2S} , the language CCS_{H} is a commutative monoid with respect to parallel composition with 0 as unit element. (In light of the provability of (5), we have taken the liberty of omitting parentheses in the second summand of the term at the right-hand side of equation HM6 in Table 2.) Moreover, it is easy to see that:

Fact 3.1 For each CCS_{H} term p, if p \underline{↔}_{2S} 0, then the equation p ≈ 0 is provable using A4, HM4 and M.

All of the equations in the axiom system E may be found in the axiomatization of tobservational congruence proposed by Hennessy in [11]. However, the abstraction from τ-labelled transitions underlying t-observational congruence renders axiom HM2 above unsound. (See the discussion in [1, Page 854 and Sect. 3].) Indeed, to the best of our knowledge, it is yet unknown whether (t-)observational congruence affords a finite equational axiomatization over CCS, with or without Hennessy’s merge.

Our aim, in the remainder of this note, will be to show that, in the presence of a finite collection of actions A, split-2 bisimilarity (that is strong t-bisimulation) is finitely axiomatizable over the language CCS_{H}. This is the import of the following:

Theorem 3.1 For all CCS_{H} terms p, q not containing occurrences of variables, p \underline{↔}_{2S} q if, and only if, E ⊢ p ≈ q.

We now proceed to prove the above theorem by establishing separately that the axiom system E is sound and complete.

Proposition 3.1 [Soundness] For all CCS_{H} terms p, q, if E ⊢ p ≈ q, then p \underline{↔}_{2S} q.

Proof: Since \underline{↔}_{2S} is a congruence over the language CCS_{H} (Fact 2.1), it suffices only to check that each of the equations in E is sound. The verification is tedious, but not hard, and we omit the details. □

Remark 3.1 For later use in the proof of Proposition 3.3, we note that equations (2)–(5) also hold modulo \underline{↔}_{2S} when the variables x, y, z are allowed to range over the set of states S.

The proof of the completeness of the equations in E with respect to \underline{↔}_{2S} follows the general outline of that of [11, Theorem 2.1.2]. As usual, we rely upon the existence of normal forms for CCS_{H} terms. In the remainder of this paper, process terms are considered modulo associativity and commutativity of +. In other words, we do not distinguish p+q and q+p, nor (p+q)+r and p+(q+r). This is justified because, as previously observed, split-2 bisimulation equivalence satisfies axioms A1, A2 in Table 2. In what follows, the symbol = will denote equality modulo axioms A1, A2. We use a summation ∑_{i∈{1,...,k}} p_{i} to denote p_{1} + ⋯ + p_{k}, where the empty sum represents 0.

Definition 3.1 The set NF of normal forms is the least subset of CCS_{H} such that

∑_{i∈I}(a_{i}p_{i} |^{/} p′_{i}) + ∑_{j∈J} τq_{j} ∈ NF ,

where I, J are finite index sets, if the following conditions hold:

1. the terms p_{i}, p′_{i} (i ∈ I) and q_{j} (j ∈ J) are contained in NF and

2. if a_{i}p_{i} |^{/} p′_{i} ⟶^{τ} q for some q, then q = q_{j} for some j ∈ J.

Proposition 3.2 [Normalization] For each CCS_{H} term p, there is a term p̂ ∈ NF such that E ⊢ p ≈ p̂.

Proof: Define the relation ≺ on CCS_{H} terms thus:

p ≺ q if, and only if,

• depth(p) < depth(q) or

• depth(p) = depth(q) and the size of p is smaller than that of q.

Note that ≺ is a well-founded relation, so we may use ≺-induction. The remainder of the proof consists of a case analysis on the syntactic form of p.

We only provide the details for the case p = q |^{/} r. (The cases p = 0, p = q +r and p = μq are trivial—the last owing to the fact that μq ≈ μq |^{/} 0 is an instance of axiom HM3—, and the case p = q | r follows from the case that is treated in detail using axiom M.)

Assume therefore that p = q |^{/} r. Then depth(q) ≤ depth(p) and the size of q is smaller than that of p, so q ≺ p. Hence, by the induction hypothesis there exists q̂ ∈ NF such that E ⊢ q ≈ q̂, say

q̂ = ∑_{i∈I}(a_{i}q_{i} |^{/} q′_{i}) + ∑_{j∈J} τq′′_{j} .

By axioms HM1, HM2, HM4 and HM5 it follows that

p ≈ ∑_{i∈I} a_{i}q_{i} |^{/} (q′_{i} | r) + ∑_{j∈J} τ(q′′_{j} | r) .

Since depth(q′_{i}), depth(q′′_{j}) < depth(q̂) = depth(q) for each i ∈ I and j ∈ J, it follows that

depth(q′_{i} | r), depth(q′′_{j} | r) < depth(q̂ |^{/} r) = depth(q |^{/} r) = depth(p) ,

and hence q′_{i} | r ≺ p and q′′_{j} | r ≺ p. By the induction hypothesis there are normal

forms q̂′_{i} | r, { \atop q′′_{j} | r} such that E ⊢ q′_{i} | r ≈ q̂′_{i} | r, q′′_{j} | r ≈ { \atop q′′_{j} | r}. So E proves the

equation

p ≈ ∑_{i∈I} a_{i}q_{i} |^{/} (q̂′_{i} | r) + ∑_{j∈J} τ({ \atop q′′_{j} | r}) .  (6)

Finally, using equation HM6, it is now a simple matter to add summands to the right-hand side of the above equation in order to meet requirement 2 in Definition 3.1. In fact, let i ∈ I and

q̂′_{i} | r = ∑_{h∈H}(a_{h}r_{h} |^{/} r′_{h}) + ∑_{k∈K} τr′′_{k} .

Using A4, we have that

q̂′_{i} | r ≈ ∑_{h∈H,a_{h}=ā_{i}}(a_{h}r_{h} |^{/} r′_{h}) + ∑_{h∈H,a_{h}≠ā_{i}}(a_{h}r_{h} |^{/} r′_{h}) + ∑_{k∈K} τr′′_{k}

is provable from E. Then, using HM6 and the induction hypothesis repeatedly, we can prove the equation

a_{i}q_{i} |^{/} (q̂′_{i} | r) ≈ a_{i}q_{i} |^{/} (q̂′_{i} | r) + ∑_{h∈H,a_{h}=ā_{i}} τ{ \atop (q_{i} | r_{h} | r′_{h})} .

Using this equation as a rewrite rule from left to right in (6) for each i ∈ I produces a term meeting requirement 2 in Definition 3.1 that is the desired normal form for p = q |^{/} r. □

The key to the proof of the promised completeness theorem is an important cancellation result that has its roots in one proven by Hennessy for his t-observational equivalence in [11].

Theorem 3.2 Let p, p′, q, q′ be CCS_{H} terms, and let a be a visible action. Assume that a_{S}p | p′ \underline{↔}_{2S} a_{S}q | q′. Then p \underline{↔}_{2S} q and p′ \underline{↔}_{2S} q′.

For the moment, we postpone the proof of this result, and use it to establish the following statement, to the effect that the axiom system E is complete with respect to \underline{↔}_{2S} over CCS_{H}.

Theorem 3.3 [Completeness] Let p, q be CCS_{H} terms such that p \underline{↔}_{2S} q. Then E ⊢ p ≈ q.

Proof: By induction on the depth of p and q. (Recall that, since p \underline{↔}_{2S} q, the terms p and q have the same depth.) In light of Propositions 3.1 and 3.2, we may assume without loss of generality that p and q are contained in NF. Let

p = ∑_{i∈I}(a_{i}p_{i} |^{/} p′_{i}) + ∑_{j∈J} τp′′_{j} and
q = ∑_{h∈H}(b_{h}q_{h} |^{/} q′_{h}) + ∑_{k∈K} τq′′_{k} .

We prove that E ⊢ p ≈ p + q, from which the statement of the theorem follows by symmetry and transitivity. To this end, we argue that each summand of q can be absorbed by p using the equations in E, i.e., that

1. E ⊢ p ≈ p + τq′′_{k} for each k ∈ K, and

2. E ⊢ p ≈ p + (b_{h}q_{h} |^{/} q′_{h}) for each h ∈ H.

We prove these two statements in turn.

• Proof of Statement 1. Let k ∈ K. Then q ⟶^{τ} q′′_{k}. Since p \underline{↔}_{2S} q, there is a term r such that p ⟶^{τ} r and r \underline{↔}_{2S} q′′_{k}. Since p ∈ NF, condition 2 in Definition 3.1 yields that r = p′′_{j} for some j ∈ J. The induction hypothesis together with closure with respect to τ-prefixing now yields that

E ⊢ τp′′_{j} ≈ τq′′_{k} .

Therefore, using A1–A3, we have that

E ⊢ p ≈ p + τp′′_{j} ≈ p + τq′′_{k} ,

which was to be shown.

• Proof of Statement 2. Let h ∈ H. Then q ⟶^{S(b_{h})} b_{h}_{S}q_{h} | q′_{h}. Since

p \underline{↔}_{2S} q, there is a state s such that p ⟶^{S(b_{h})} s and s \underline{↔}_{2S} b_{h}_{S}q_{h} | q′_{h}. Because of the form of p, it follows that s = a_{i}_{S}p_{i} | p′_{i} for some i ∈ I such that a_{i} = b_{h}. By Theorem 3.2, we have that

p_{i} \underline{↔}_{2S} q_{h} and p′_{i} \underline{↔}_{2S} q′_{h} .

Since the depth of all of these terms is smaller than that of p, we may apply the induction hypothesis twice to obtain that

E ⊢ p_{i} ≈ q_{h} and E ⊢ p′_{i} ≈ q′_{h} .

Therefore, using A1–A3 and a_{i} = b_{h}, we have that

E ⊢ p ≈ p + (a_{i}p_{i} |^{/} p′_{i}) ≈ p + (b_{h}q_{h} |^{/} q′_{h}) ,

which was to be shown.

The proof of the theorem is now complete. □

To finish the proof of the completeness theorem, and therefore of Theorem 3.1, we are left to show Theorem 3.2. Our proof of that result relies on a unique decomposition property with respect to parallel composition for states modulo \underline{↔}_{2S} . In order to formulate this decomposition property, we shall make use of some notions from [15, 16]. These we now proceed to introduce for the sake of completeness and readability.

Definition 3.2 A state s is irreducible if s \underline{↔}_{2S} s_{1} | s_{2} implies s_{1} \underline{↔}_{2S} 0 or s_{2} \underline{↔}_{2S} 0, for all states s_{1}, s_{2}.

We say that s is prime if it is irreducible and is not split-2 bisimilar to 0.

For example, each state s of depth 1 is prime because every state of the form s_{1} | s_{2}, where s_{1} and s_{2} are not split-2 bisimilar to 0, has depth at least 2, and thus cannot be split-2 bisimilar to s.

Fact 3.2 The state a_{S}p is prime, for each CCS_{H} term p and action a.

Proof: Since a_{S}p is not split-2 bisimilar to 0, it suffices only to show that it is irreducible. To this end, assume, towards a contradiction, that a_{S}p \underline{↔}_{2S} s_{1} | s_{2} for some states s_{1}, s_{2} that are not split-2 bisimilar to 0. Then, since a_{S}p \underline{↔}_{2S} s_{1} | s_{2},

we have that s_{1} ⟶^{F (a)} s′_{1} and s_{2} ⟶^{F (a)} s′_{2}, for some s′_{1}, s′_{2}. But then it follows that

s_{1} | s_{2} ⟶^{F (a)} s′_{1} | s_{2} ⟶^{F (a)} s′_{1} | s′_{2} ,

whereas the term a_{S}p cannot perform two subsequent F (a)-transitions. We may therefore conclude that such s_{1} and s_{2} cannot exist, and hence that the term a_{S}p is irreducible, which was to be shown. □

The following result is the counterpart for the language CCS_{H} of the unique decomposition theorems presented for various languages in, e.g., [4, 13, 15, 16].

Proposition 3.3 Each state is split-2 bisimilar to a parallel composition of primes, uniquely determined up to split-2 bisimilarity and the order of the primes. (We adopt the convention that 0 denotes the empty parallel composition.)

Proof: We shall obtain this result as a consequence of a general unique decomposition result, obtained by the fourth author in [13].

Let [S] denote the set of states modulo split-2 bisimilarity, and, for a state s ∈ S, denote by [s] the equivalence class in [S] that contains s. By Fact 2.1 we can define on [S] a binary operation | by

[s] | [t] = [s | t] .

By Remark 3.1, the set [S] with the binary operation | and the distinguished element [0] is a commutative monoid.

Next, we define on [S] a partial order ≼ by

[s′] ≼ [s] iff there exist s′′ ∈ S and σ ∈ E^{∗} such that s ⟶^{σ} s′′ \underline{↔}_{2S} s′.

Note that ≼ is indeed a partial order (to establish antisymmetry use that transitions decrease depth, and that split-2 bisimilar states have the same depth).

For each state s, there are a sequence of events σ and a state s′ such that

s ⟶^{σ} s′ \underline{↔}_{2S} 0 .

So [0] is the least element of [S] with respect to ≼. Furthermore, if [s′] ≼ [s], then s ⟶^{σ} s′′ \underline{↔}_{2S} s′, for some σ ∈ E^{∗} and state s′′. So, using the SOS rules for S and Fact 2.1, it follows that s | t ⟶^{σ} s′′ | t \underline{↔}_{2S} s′ | t, and hence

[s′] | [t] = [s′ | t] ≼ [s | t] = [s] | [t] .

Thereby, we have now established that [S] with |, [0] and ≼ is a positively ordered commutative monoid in the sense of [13].

From the SOS rules for S it easily follows that this positively ordered commutative monoid is precompositional (see [13]), i.e., that

if [s] ≼ [s_{1}] | [s_{2}], then there are [s′_{1}] ≼ [s_{1}], [s′_{2}] ≼ [s_{2}] s.t. [s] = [s′_{1}] | [s′_{2}].

Consider the mapping | | : [S] → N into the positively ordered monoid of natural numbers with addition, 0 and the standard less-than-or-equal relation, defined by

[s] ↦ depth(s) .

It is straightforward to verify that | | is a stratification (see [13]), i.e., that (i) |[s] | [t]| = |[s]| + |[t]|; and

(ii) if [s] ≺ [t], then |[s]| < |[t]|.

We conclude that [S] with |, [0] and ≼ is a stratified and precompositional positively ordered commutative monoid, and hence, by Theorem 13 in [13], it has unique decomposition. This completes the proof of the proposition. □

Using the above unique decomposition result, we are now in a position to complete the proof of Theorem 3.2.

Proof of Theorem 3.2: Assume that a_{S}p | p′ \underline{↔}_{2S} a_{S}q | q′. Using Proposition 3.3, we have that p′ and q′ can be expressed uniquely as parallel compositions of primes. Say that

p′ \underline{↔}_{2S} p_{1} | p_{2} | ⋯ | p_{m} and
q′ \underline{↔}_{2S} q_{1} | q_{2} | ⋯ | q_{n}

for some m, n ≥ 0 and primes p_{i} (1 ≤ i ≤ m) and q_{j} (1 ≤ j ≤ n) in the language CCS_{H}. Since a_{S}p and a_{S}q are prime (Fact 3.2) and \underline{↔}_{2S} is a congruence (Fact 2.1), the unique prime decompositions of a_{S}p | p′ and a_{S}q | q′ given by Proposition 3.3 are

a_{S}p | p \underline{↔}_{2S} a_{S}p | p_{1} | p_{2} | ⋯ | p_{m} and
a_{S}q | q′ \underline{↔}_{2S} a_{S}q | q_{1} | q_{2} | ⋯ | q_{n} ,

respectively. In light of our assumption that a_{S}p | p′ \underline{↔}_{2S} a_{S}q | q′, these two prime decompositions coincide by Proposition 3.3. Hence, as a_{S}p \underline{↔}_{2S} / q_{j} for each 1 ≤ j ≤ n, we have that

1. a_{S}p \underline{↔}_{2S} a_{S}q,

2. m = n and, without loss of generality,

3. p_{i} \underline{↔}_{2S} q_{i} for each 1 ≤ i ≤ m.

It is now immediate to see that p \underline{↔}_{2S} q and p′ \underline{↔}_{2S} q′, which was to be shown. □

Acknowledgments The work reported in this paper was carried out while Luca Aceto was on leave at Reykjavík University, and Anna Ingólfsdóttir was at de-CODE Genetics. They thank these institutions for their hospitality and excellent working conditions.

References

[1] L. Aceto, On “Axiomatising finite concurrent processes”, SIAM J. Comput., 23 (1994), pp. 852–863.

[2] , Some of my favourite results in classic process algebra, Note NS-03-2, BRICS, Department of Computer Science, Aalborg University, September 2003.

[3] L. Aceto, W. Fokkink, A. Ingólfsdóttir, and B. Luttik, CCS with Hennessy’s merge has no finite equational axiomatization, Research report RS-03-34, BRICS, November 2003.

[4] L. Aceto and M. Hennessy, Towards action refinement in process algebras, Information and Computation, 103 (1993), pp. 204–269.

[5] J. Baeten, A brief history of process algebra, Report CSR 04-02, Eindhoven University of Technology, 2004.

[6] J. Baeten and P. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

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

[8] , Process algebra for synchronous communication, Information and Control, 60 (1984), pp. 109–137.

[9] R. van Glabbeek and F. Vaandrager, Petri net models for algebraic theories of concurrency, in Proceedings PARLE conference, Eindhoven, Vol. II (Parallel Languages), J. de Bakker, A. Nijman, and P. Treleaven, eds., vol. 259 of Lecture Notes in Computer Science, Springer-Verlag, 1987, pp. 224–242.

[10] R. Gorrieri and C. Laneve, Split and ST bisimulation semantics, Information and Computation, 118 (1995), pp. 272–288.

[11] M. Hennessy, Axiomatising finite concurrent processes, SIAM J. Comput., 17 (1988), pp. 997–1017.

[12] M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, J. Assoc. Comput. Mach., 32 (1985), pp. 137–161.

[13] B. Luttik, A unique decomposition theorem for ordered monoids with applications in process theory, in Proceedings of Mathematical Foundations of Computer Science 2003, 28th International Symposium, MFCS 2003, Bratislava, Slovakia, August 25–29, 2003, B. Rovan and P. Vojtás, eds., vol. 2747 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 562–571.

[14] R. Milner, Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

[15] R. Milner and F. Moller, Unique decomposition of processes (note), Theoretical Comput. Sci., 107 (1993), pp. 357–363.

[16] F. Moller, Axioms for Concurrency, PhD thesis, Department of Computer Science, University of Edinburgh, July 1989. Report CST-59-89. Also published as ECS-LFCS-89-84.

[17] , The importance of the left merge operator in process algebras, in Proceedings 17^{th} ICALP, Warwick, M. Paterson, ed., vol. 443 of Lecture Notes in Computer Science, Springer-Verlag, July 1990, pp. 752–764.

[18] , The nonexistence of finite axiomatisations for CCS congruences, in Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, 1990, pp. 142–153.

[19] D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.

Recent BRICS Report Series Publications

RS-04-1 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy’s Merge. January 2004. 16 pp.

RS-03-53 Kyung-Goo Doh and Peter D. Mosses. Composing Programming Languages by Combining Action-Semantics Modules. December 2003. 39 pp. Appears in Science of Computer Programming, 47(1):2–36, 2003.

RS-03-52 Peter D. Mosses. Pragmatics of Modular SOS. December 2003. 22 pp. Invited paper, published in Kirchner and Ringeissen, editors, Algebraic Methodology and Software Technology: 9th International Conference, AMAST ’02 Proceedings, LNCS 2422, 2002, pages 21–40.

RS-03-51 Ulrich Kohlenbach and Branimir Lambov. Bounds on Iterations of Asymptotically Quasi-Nonexpansive Mappings. December 2003. 24 pp.

RS-03-50 Branimir Lambov. A Two-Layer Approach to the Computability and Complexity of Real Numbers. December 2003. 16 pp.

RS-03-49 Marius Mikucionis, Kim G. Larsen, and Brian Nielsen. Online On-the-Fly Testing of Real-time Systems. December 2003. 14 pp.

RS-03-48 Kim G. Larsen, Ulrik Larsen, Brian Nielsen, Arne Skou, and Andrzej Wasowski. Danfoss EKC Trial Project Deliverables. December 2003. 53 pp.

RS-03-47 Hans Hüttel and Jiří Srba. Recursive Ping-Pong Protocols. December 2003. 21 pp. To appear in the proceedings of 2004 IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS Workshop on Issues in the Theory of Security (WITS’04).

RS-03-46 Philipp Gerhardy. The Role of Quantifier Alternations in Cut Elimination. December 2003. 10 pp. Extends paper appearing in Baaz and Makowsky, editors, European Association for Computer Science Logic: 17th International Workshop, CSL ’03 Proceedings, LNCS 2803, 2003, pages 212-225.