BRICS RS-03-34 Aceto et al.: CCS with Hennessy’s Merge has no Finite Equational Axiomatization BRICS

Basic Research in Computer Science

CCS with Hennessy’s Merge has no Finite Equational Axiomatization

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

BRICS Report Series RS-03-34

ISSN 0909-0878 November 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, 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/03/34/

CCS with Hennessy’s Merge has no Finite Equational Axiomatization

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 paper confirms a conjecture of Bergstra and Klop’s from 1984 by establishing that the process algebra obtained by adding an auxiliary operator proposed by Hennessy in 1981 to the recursion free fragment of Milner’s Calculus of Communicationg Systems is not finitely based modulo bisimulation equivalence. Thus Hennessy’s merge cannot replace the left merge and communication merge operators proposed by Bergstra and Klop, at least if a finite axiomatization of parallel composition is desired. 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, Hennessy’s merge, left merge, communication merge, parallel composition, equational logic, complete axiomatizations, non-finitely based algebras.

1 Introduction

Process algebras are prototype description languages for reactive systems that arose from the pioneering work of figures like Bergstra, Hoare, Klop and Milner. Well known examples of such languages are ACP [7], CCS [26], CSP [23] and Meije [5]. These algebraic description languages for processes differ in the basic collection of operators that they offer for building new process descriptions from existing ones. However, since they are designed to allow for the description and analysis of systems of interacting processes, they all contain some form of parallel composition (also known as merge) operator allowing one to put two process terms in parallel with one another. These operators usually interleave the behaviours of their arguments, and allow for some form of synchronization between them. For example, Milner’s CCS offers the binary operator |, whose intended semantics is described by the following classic rules in Plotkin-style [32]:

\frac{x →^{μ} x′}{x | y →^{μ} x′ | y}  \frac{y →^{μ} y′}{x | y →^{μ} x | y′}  \frac{x →^{α} x′, y →^{ᾱ} y′}{x | y →^{τ} x′ | y′}  (1)

(In the above rules, the symbol μ stands for an action that a process may perform, α and ᾱ are two observable actions that may synchronize, and τ is a symbol denoting the result of their synchronization.)

Although the above rules describe the behaviour of the parallel composition operator in very intuitive fashion, the equational characterization of this operator is not straightforward. In their seminal paper [22], Hennessy and Milner offered, amongst a wealth of other classic results, a complete equational axiomatization of bisimulation equivalence [31] over the recursion free fragment of CCS. The axiomatization proposed by Hennessy and Milner ibidem dealt with parallel composition using the so-called expansion law—a law that, intuitively, allows one to obtain a term describing the initial transitions of the parallel composition of two terms whose initial transitions are known. This law can be expressed as a conditional equation thus

\frac{x = ∑_{i∈I} μ_{i}x_{i}, y = ∑_{j∈J} γ_{j}y_{j}}{x | y = ∑_{i∈I} μ_{i}(x_{i} | y) + ∑_{j∈J} γ_{j}(x | y_{j}) + ∑_{i∈I,j∈J,μ_{i}=\overline{γ_{j}}} τ(x_{i} | y_{j})}

(where I and J are two finite index sets, and the μ_{i} and γ_{j} are actions), and is nothing but an equational formulation of the aforementioned rules describing the operational semantics of parallel composition.

As already remarked, the expansion law, however, is a conditional equation, which may alternatively be viewed as an equation schema with a countably infinite number of instances. 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 showed in [29, 30] that strong bisimulation equivalence is not finitely based over CCS and PA without the left merge operator. (The process algebra PA [8] contains a parallel composition operator based on pure interleaving without communication—viz. an operator described by the first two rules in (1)—and the left merge operator.) Thus auxiliary operators are necessary to obtain a finite axiomatization of parallel composition.

In the arguably less well known paper [21], Hennessy proposed an axiomatization of observation congruence [22] (also known as rooted weak bisimulation) and timed congruence (also known as split-2 congruence) over a CCS-like recursion free process language. (It is worth noting that, although this paper was published in 1988 by the SIAM Journal on Computing as [21], the results reported ibidem were actually obtained in 1981–1982.) Those axiomatizations used an auxiliary operator, denoted |^{/} by Hennessy, that is essentially a combination of the left and communication merge operators as its behaviour is described by the first and the last rule in (1). 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 [22]. This led Bergstra and Klop to write in [8, page 118] that:

“It seems that γ does not have a finite equational axiomatization.”

(In op. cit. Bergstra and Klop used γ to denote Hennessy’s merge.) To the best of our knowledge, the non-finite axiomatizability of Hennessy’s merge has, however, never been proven. The main result in this paper confirms this conjecture of Bergstra and Klop’s by showing that, in the presence of two distinct complementary actions, it is impossible to provide a finite axiomatization of the recursion free fragment of CCS modulo bisimulation using Hennessy’s merge operator |^{/}. We believe that this result further reinforces the status of the left merge and the communication merge operators as auxiliary operators in the finite equational characterization of parallel composition in bisimulation semantics.

The aforementioned negative result holds in a very strong form. Indeed, we prove that no finite collection of equations over the language we study that are sound with respect to bisimulation equivalence can prove all of the sound closed equalities of the form

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

where the terms p_{n} are defined thus:

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

The proof of our main result is given along proof theoretic lines that have their roots in those for the aforementioned results of Moller’s to the effect that bisimulation equivalence is not finitely based over the recursion free fragment of CCS. However, the presence of possible synchronizations in the terms used in the family of equations e_{n} is necessary for our result, and requires careful attention in the proofs. (Indeed, in the absence of synchronization, Hennessy’s merge reduces to Bergstra and Klop’s left merge operator, and thus affords a finite equational axiomatization.) In particular, the infinite family of equations e_{n} and our arguments based upon it exploit the inability of any finite axiom system E that is sound with respect to bisimulation equivalence to “expand” the synchronization behaviour of terms of the form p |^{/} q, for terms q that, like the terms p_{n} above eventually do, have a number of inequivalent “summands” that is larger than the maximum size of the terms mentioned in equations in E. As in the original arguments of Moller’s, the root of this problem can be traced back to the fact that the choice operator + distributes with respect to |^{/} in the first argument, but not in the second.

Related Work The equational characterization of different versions of the parallel composition operator is a classic topic in the theory of computation, and this paper joins the aforementioned seminal references in contributing to this line of research. In particular, the process algebraic literature abounds with results on equational axiomatizations of various notions of behavioural equivalences or preorders over languages incorporating some notion of parallel composition—see, e.g., the textbooks [7, 20, 26] and the classic papers [8, 22, 25] for general references. Early ω-complete axiomatizations are offered in [19, 28]. More recently, Fokkink and Luttik have shown in [17] that the process algebra PA [8] affords an ω-complete axiomatization that is finite if so is the underlying set of actions.

An analysis of the reasons why operators like the left merge and the communication merge are equationally well behaved in bisimulation semantics has led to general algorithms for the generation of (finite) equational axiomatizations for behavioural equivalences from their operational semantics—see, e.g., [3, 6] and the references in [4] for further details.

Parallel composition appears as the shuffle operator in the time-honoured theory of formal languages. Not surprisingly, the equational theory of shuffle has received considerable attention in the literature. Here we limit ourselves to mentioning some results that have a special relationship with process theory.

In [35], Tschantz offered a finite equational axiomatization of the theory of languages over concatenation and shuffle, solving an open problem raised by Pratt. In proving this result he essentially rediscovered the concept of pomset [33]—a model of concurrency based on partial orders whose algebraic aspects have been investigated by Gischer in [18]—, and proved that the equational theory of series-parallel pomsets coincides with that of languages over concatenation and shuffle. The argument adopted by Tschantz was based on the observation that series-parallel pomsets may be coded by a suitable homomorphism into languages, where the series and parallel composition operators on pomsets are modelled by the concatenation and shuffle operators on languages. Tschantz’s technique of coding pomsets with languages homomorphically was further extended in the papers [10, 12, 13] to deal with several other operators, infinite pomsets and infinitary languages, and sets of pomsets. The axiomatizations by Gischer and Tschantz have later been extended in [13, 16] to a two-sorted language with ω powers of the concatenation and parallel composition operators. The axiomatization of the algebra of pomsets resulting from the addition of these iteration operators is, however, necessarily infinite because, as shown in op. cit. no finite collection of equations can capture all the sound equalities involving them. (See [14] for closely related developments.)

The results of Moller’s on the non-finite axiomatizability of bisimulation equivalence over the recursion free fragment of CCS and PA without the left merge operator given in [29, 30] are paralleled in the world of formal language theory by those offered in [9, 11, 15]. In the first of those references, Bloom and Ésik proved that the valid inequations in the algebra of languages equipped with concatenation and shuffle have no finite basis. Ésik and Bertol showed in [15] that the equational theory of union, concatenation and shuffle over languages has no finite first-order axiomatization relative to the collection of all valid inequations that hold for concatenation and shuffle. Hence the combination of some form of parallel composition, sequencing and choice is hard to characterize equationally both in the theory of languages and in that of processes. Moreover, Bloom and Ésik have shown in [11] that the variety of all languages over a finite alphabet ordered by inclusion with the operators of concatenation and shuffle, and a constant denoting the singleton language containing only the empty word is not finitely axiomatizable by first-order sentences that are valid in the the equational theory of languages over concatenation, union and shuffle.

Roadmap of the Paper We begin by presenting preliminaries on the language CCS_{H}—the extension of CCS with Hennessy’s merge operator—and equational logic (Sect. 2). In particular, Sect. 2.2offers a detailed discussion of the simplifying assumptions we shall make, without loss of generality, on the equational axiom systems that we shall consider in the rest of the paper. Our main result on the nonexistence of a finite equational axiomatization for bisimulation equivalence over the language CCS_{H} (Theorem 3.1) is stated in Sect. 3. There we show how to reduce the proof of Theorem 3.1 to that of a proposition (Proposition 3.2) to the effect that no finite axiom system over the fragment of the language CCS_{H} that does not use the parallel composition operator can prove all of the aforementioned equations e_{n}. The following two technical sections of the paper, viz. Sects. 4 and 5, are entirely devoted to a detailed proof of Proposition 3.2. The paper ends with some concluding remarks (Sect. 6).

2 Preliminaries

We begin by introducing the basic definitions and results on which the technical developments to follow are based.

2.1 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 [21] to the recursion, restriction and relabelling free subset of Milner’s CCS [26]. This language is given by the following grammar:

t ::= x | 0 | at | āt | τt | t + t | t | t | t |^{/} t ,

where x is a variable drawn from a countably infinite set V, a is an action, and ā is its complement. We assume that the actions a and ā are distinct. Following Milner [26], the action symbol τ will result from the synchronized occurrence of the complementary actions a and ā. We let μ ∈ {a, ā, τ} and α ∈ {a, ā}. As usual, we postulate that ¯ ā = a. We shall use the meta-variables t, u, v, w to range over process terms, and write var(t) for the collection of variables occurring in the term t. The size of a term is the number of operator symbols in it. A process term is Table 1: SOS Rules for the CCS Operators (μ ∈ {a, ā, τ} and α ∈ {a, ā})

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

\frac{x →^{μ} x′}{x | y →^{μ} x′ | y}  \frac{y →^{μ} y′}{x | y →^{μ} x | y′}  \frac{x →^{α} x′, y →^{ᾱ} y′}{x | y →^{τ} x′ | y′}

closed if it does not contain any variables. Closed terms will be typically denoted by p, q, r.

In order to obtain the negative results offered in this paper, it will be sufficient to consider the above language. The results we shall present in what follows carry over unchanged to a setting with an arbitrary number of actions, and corresponding unary prefixing operators.

A (closed) substitution is a mapping from process variables to (closed) CCS_{H} terms. For every term t and (closed) substitution σ, the (closed) term obtained by replacing every occurrence of a variable x in t with the (closed) term σ(x) will be written σ(t).

In the remainder of this paper, we let a^{0} denote 0, and a^{m+1} denote a(a^{m}). The SOS rules for all of the classic CCS operators are standard, and may be

found in Table 1. Those for Hennessy’s |^{/} formalize the intuition that this operator is indeed a combination of the left and communication merge operators, and are:

\frac{x →^{μ} x′}{x |^{/} y →^{μ} x′ | y}  \frac{x →^{α} x′, y →^{ᾱ} y′}{x |^{/} y →^{τ} x′ | y′}

These transition rules give rise to transitions between CCS_{H} terms. The operational semantics for CCS_{H} is thus given by the labelled transition system [24] whose states are CCS_{H} terms, and whose labelled transitions are those that are provable using the rules. As usual, for each term t and action μ, we write t →^{μ} if t →^{μ} t′ holds for some term t′.

The transition relations →^{μ} naturally compose to determine the possible effects that performing a sequence of actions may have on a CCS_{H} term.

Definition 2.1 For a sequence of actions s = μ_{1} ⋯ μ_{k} (k ≥ 0), and CCS_{H} terms t, t′, we write t →^{s} t′ iff there exists a sequence of transitions

t = t_{0} →^{μ_{1}} t_{1} →^{μ_{2}} ⋯ →^{μ_{k}} t_{k} = t′ .

If t →^{s} t′ holds for some CCS_{H} term t′, then s is a trace of t.

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

The depth of closed terms can also be characterized inductively thus:

depth(0) = 0
depth(μp) = 1 + depth(p)
depth(p + q) = max{depth(p), depth(q)}
depth(p | q) = depth(p) + depth(q)
depth(p |^{/} q) = \begin{cases}0 & if depth(p) = 0 , \\ depth(p) + depth(q) & otherwise . \end{cases}

In what follows, we shall sometimes need to consider the possible origins of a transition of the form σ(t) →^{α} p, for some action α ∈ {a, ā}, closed substitution σ, CCS_{H} term t and closed term p. Naturally enough, we expect that σ(t) affords that transition if t →^{α} t′, for some t′ such that p = σ(t′). However, the above transition may also derive from the initial behaviour of some closed term σ(x), provided that the collection of initial moves of σ(t) depends, in some formal sense, on that of the closed term substituted for the variable x. To fully describe this situation, we introduce the auxiliary notion of configuration of a CCS_{H} term. To this end, we assume a set of symbols

V_{d} = {x_{d} | x ∈ V }

disjoint from V. Intuitively, the symbol x_{d} (read “during x”) will be used to denote that the closed term substituted for variable x has begun executing.

Definition 2.2 The collection of CCS_{H} configurations is given by the following grammar:

c ::= t | x_{d} | c | t | t | c ,

where t is a CCS_{H} term, and x_{d} ∈ V_{d}.

For example, the configuration x_{d} | (a0 |^{/} x) is meant to describe a state of the computation of some term in which the (closed term substituted for the) occurrence of variable x on the left-hand side of the | operator has begun its execution, but the one on the right-hand side has not. We shall consider the symbols x_{d} as variables, and use the notation σ[x_{d} ↦ p], where σ is a closed substitution and p is a closed CCS_{H} term, to stand for the substitution mapping x_{d} to p, and acting like σ on all of the variables in V.

The way in which the initial behaviour of a term may depend on that of the variables that occur in it is formally described by an auxiliary transition relation whose elements have the form t →^{x} c, where t is a term, x is a variable, and c is a configuration. The SOS rules defining these transitions are given in Table 2.

Table 2: SOS Rules for the Auxiliary Transitions →^{x} (x ∈ V)

\overline{x →^{x} x_{d}}  \frac{t →^{x} c}{t + u →^{x} c}  \frac{u →^{x} c}{t + u →^{x} c}

\frac{t →^{x} c}{t | u →^{x} c | u}  \frac{u →^{x} c}{t | u →^{x} t | c}  \frac{t →^{x} c}{t |^{/} u →^{x} c | u}

Lemma 2.1 Assume that t is a CCS_{H} term, σ is a closed substitution and α ∈ {a, ā}. Then the following statements hold:

1. If t →^{α} t′, then σ(t) →^{α} σ(t′).

2. Assume that t →^{x} c and σ(x) →^{α} p, for some closed term p. Then σ(t) →^{α} σ[x_{d} ↦ p](c).

3. Assume that σ(t) →^{α} p, for some closed term p. Then

• either t →^{α} t′ for some t′ such that p = σ(t′)

• or t →^{x} c and σ(x) →^{α} q, for some variable x, configuration c and closed term q such that σ[x_{d} ↦ q](c) = p.

In this paper, we shall consider the language CCS_{H} modulo bisimulation equivalence [26, 31].

Definition 2.3 Bisimulation equivalence (also sometimes referred to as bisimilarity), denoted by \underline{↔}, is the largest symmetric relation over closed CCS_{H} terms such that whenever p \underline{↔} q and p →^{μ} p′, then there is a transition q →^{μ} q′ with p′ \underline{↔} q′.

If p \underline{↔} q, then we say that p and q are bisimilar.

It is well-known that, as the name suggests, bisimulation equivalence is indeed an equivalence relation (see, e.g., the references [26, 31]). Moreover, two bisimulation equivalent terms over the language CCS_{H} afford the same finite non-empty set of traces, and have therefore the same depth. Since the SOS rules defining the operational semantics of the language CCS_{H} are in de Simone’s format [34], we have that:

Fact 2.1 Bisimulation equivalence is a congruence over the language CCS_{H}.

Bisimulation equivalence is extended to arbitrary CCS_{H} terms thus:

Definition 2.4 Let t, u be CCS_{H} terms. Then t \underline{↔} u iff σ(t) \underline{↔} σ(u) for every closed substitution σ.

For instance, we have that

0 |^{/} x \underline{↔} 0

because 0 |^{/} p affords no transition, for each closed term p.

Definition 2.5 We say that a term t has a 0 factor if it contains a subterm of the form t′ | t′′ or t′ |^{/} t′′, where either t′ or t′′ is bisimilar to 0.

For example, the terms a(0 | x) and (0 |^{/} x) | y have a 0 factor.

2.2 Equational Logic

An axiom system is a collection of equations t ≈ u over the language CCS_{H}. An equation p ≈ q is derivable from an axiom system E, notation E ⊢ p ≈ q, if it can be proven from the axioms in E using the rules of equational logic (viz. reflexivity, symmetry, transitivity, substitution and closure under CCS_{H} contexts):

t ≈ t \frac{t ≈ u}{u ≈ t} \frac{t ≈ u u ≈ v}{t ≈ v} \frac{t ≈ u}{σ(t) ≈ σ(u)} \frac{t ≈ u}{μt ≈ μu}

\frac{t ≈ u t′ ≈ u′}{t + t′ ≈ u + u′} \frac{t ≈ u t′ ≈ u′}{t |^{/} t′ ≈ u |^{/} u′} \frac{t ≈ u t′ ≈ u′}{t | t′ ≈ u | u′} .

Without loss of generality one may assume that substitutions happen first in equational proofs, i.e., that the rule

\frac{t ≈ u}{σ(t) ≈ σ(u)}

may only be used when (t ≈ u) ∈ E. In this case σ(t) ≈ σ(u) is called a substitution instance of an axiom in E.

Definition 2.6 We call a closed substitution σ substantial if depth(σ(x)) > 0 for each variable x.

For reasons of technical convenience, in the proofs of our non-finite axiomatizability results presented in this paper we shall only allow for the use of closed substantial substitutions in the rule of substitution. This does not limit the generality of those results because every finite equational axiomatization E can be converted into a finite equational axiomatization E′ such that the closed substitution instances of the axioms of E are the same as the closed substantial substitution instances of the axioms of E′ (when equating any closed subterm of depth 0 with 0). This is done by including in E′ any equation that can be obtained from an equation in E by replacing all occurrences of any number of variables by 0. (The identification of each CCS_{H} term that is bisimilar to 0 with 0 can be done equationally using three equations. See Fact 2.2 to follow.)

Definition 2.7 We say that a substitution σ is a 0-substitution iff σ(x) ≠ x implies that σ(x) = 0, for each variable x.

An axiom system E is closed with respect to 0-substitutions iff σ(t) ≈ σ(u) is contained in E, for each 0-substitution σ, if so is t ≈ u.

Simplifying Assumption 1 In the remainder of this paper, we shall always tacitly assume that equational axiom systems are closed with respect to 0-substitutions.

Note that if E is a finite axiom system, then so is its closure with respect to 0substitutions. In fact, for each term t, the collection of terms

{σ(t) | σ a 0-substitution}

is finite.

Moreover, by postulating that for each axiom in E also its symmetric counterpart is present in E, one may assume that applications of symmetry happen first in equational proofs.

Simplifying Assumption 2 In the remainder of this paper, we shall also tacitly assume that our equational axiom systems are closed with respect to symmetry.

Definition 2.8 An equation t ≈ u over the language CCS_{H} is sound with respect to \underline{↔} iff t \underline{↔} u. An axiom system is sound with respect to \underline{↔} iff so is each of its equations.

An example of a collection of equations over the language CCS_{H} that are sound with respect to \underline{↔} is given in Table 3. In addition, the following law, which expresses the parallel composition operator in terms of Hennessy’s merge, is easily seen to be sound with respect to \underline{↔}:

x | y ≈ (x |^{/} y) + (y |^{/} x) .  (2)

The axioms A4, HM1 and M1 in Table 3 (used from left to right) are enough to establish that each CCS_{H} term that is bisimilar to 0 is also provably equal to 0. Since we feel that the proof of this little result is instructive, we now proceed to present its sketch.

Table 3: Some Axioms for CCS_{H}

A1  x + y ≈ y + x
A2 (x + y) + z ≈ x + (y + z)
A3  0 + x ≈ x
A4  x + 0 ≈ x
HM1  0 |^{/} x ≈ 0
HM2  x |^{/} 0 ≈ x
M1  x | 0 ≈ x
M2  0 | x ≈ x

Fact 2.2 Let t be a CCS_{H} term. Then t \underline{↔} 0 if, and only if, the equation t ≈ 0 is provable using axioms A4, HM1 and M1 in Table 3 from left to right.

Proof: The “if” implication is an immediate consequence of the soundness of the equations A4, HM1 and M1 with respect to \underline{↔}. To prove the “only if” implication, define, first of all, the collection NIL of CCS_{H} terms as the set of terms generated by the following grammar:

t ::= 0 | t + t | t | t | t |^{/} u ,

where u is an arbitrary CCS_{H} term. We claim that:

Claim 1 Each CCS_{H} term t is bisimilar to 0 if, and only if, t ∈ NIL.

Using this claim and structural induction on t ∈ NIL, it is a simple matter to show that if t \underline{↔} 0, then t ≈ 0 is provable using axioms A4, HM1 and M1 from left to right, which was to be shown.

To complete the proof, it therefore suffices to show the above claim. To establish the “if” implication in the statement of the claim, one proves, using structural induction on t and the congruence properties of bisimilarity (Fact 2.1), that if t ∈ NIL, then σ(t) \underline{↔} 0 for every closed substitution σ. To show the “only if” implication, we establish the contrapositive statement, viz. that if t ∉ NIL, then σ(t) \underline{↔} / 0 for some closed substitution σ. To this end, it suffices only to show, using structural induction on t, that if t ∉ NIL, then σ_{a}(t) →^{μ} for some action μ ∈ {a, ā, τ}, where σ_{a} is the closed substitution mapping each variable to the closed term a0. The details of this argument are not hard, and are therefore left to the reader. □

In light of the above result, we find it convenient to make the following:

Simplifying Assumption 3 In the technical developments to follow, we shall assume, without loss of generality, that each axiom system we consider includes the equations in Table 3.

This assumption means, in particular, that our axiom systems will allow us to identify each term that is bisimilar to 0 with 0.

In the remainder of this paper, process terms are considered modulo associativity and commutativity of +. In other words, we do not distinguish t + u and u + t, nor (t + u) + v and t + (u + v). This is justified because, as previously observed, bisimulation equivalence satisfies axioms A1, A2 in Table 3. In what follows, the symbol = will denote equality modulo axioms A1, A2. We use a summation ∑_{i∈{1,...,k}} t_{i} to denote t_{1} + ⋯ + t_{k}, where the empty sum represents 0. It is easy to see that, modulo the equations in Table 3, every CCS_{H} term t has the form ∑_{i∈I} t_{i}, for some finite index set I, and terms t_{i} (i ∈ I) that are not 0 and do not have themselves the form t′ + t′′, for some terms t′ and t′′. The terms t_{i} (i ∈ I) will be referred to as the summands of t. Moreover, again modulo the equations in Table 3, each of the t_{i} can be assumed to have no 0 factors. (Recall that this means that, whenever a term of the form t′ |^{/} t′′ or t′ | t′′ is a subterm of t_{i}, then t′ \underline{↔} / 0 and t′′ \underline{↔} / 0.) For example, a term of the form (a0 + ā0) | 0 will not be considered a summand in what follows because, using equation M1 in Table 3, that term can be proven equal to a0 + ā0. The collection of summands of a term t can be inductively characterized thus:

• 0 has no summands;

• x and μt are their only summands;

• u is a summand of t_{1} + t_{2} if it is either a summand of t_{1} or a summand of t_{2};

• the summands of t_{1} | t_{2} are

– those of t_{2}, if t_{1} \underline{↔} 0,

– those of t_{1}, if t_{2} \underline{↔} 0, and

– only t_{1} | t_{2}, otherwise;

• the summands of t_{1} |^{/} t_{2} are

– none, if t_{1} \underline{↔} 0,

– those of t_{1}, if t_{2} \underline{↔} 0, and

– only t_{1} |^{/} t_{2}, otherwise.

It is well-known (cf., e.g., Sect. 2 in [19]) that if an equation relating two closed terms can be proven from an axiom system E, then there is a closed proof for it. We shall now argue that if E satisfies a further closure property in addition to those mentioned earlier, and that closed equation relates two terms containing no occurrences of 0 as a summand or factor, then there is a closed proof for it in which all of the terms have no occurrences of 0 as a summand or factor—see [28, Proposition 5.1.5].

Definition 2.9

1. For CCS_{H} terms t and t′, we write t ⇝ t′ if t′ can be obtained from t by applying one of the equations A3, A4, HM1, HM2, M1 and M2 from left to right. As usual, we write ⇝^{∗} for the reflexive, transitive closure of the relation ⇝.

2. Let E be an axiom system. We define the axiom system cl(E) thus:

cl(E) = {t′ ≈ u′ | (t ≈ u) ∈ E, t ⇝^{∗} t′ and u ⇝^{∗} u′} .

3. An axiom system E is saturated if E = cl(E).

Intuitively, one application of the rewrite relation ⇝ eliminates one occurrence of 0 as a summand or a factor in terms. Note that t \underline{↔} t′ holds whenever t ⇝ t′.

The following lemma collects some basic sanity properties of the closure operator cl(·). (Note, in particular, that the application of cl(·) to an axiom system satisfying our simplifying assumptions is guaranteed to produce a saturated axiom system that also affords them.)

Lemma 2.2 Let E be an axiom system. Then the following statements hold.

1. E ⊆ cl(E) = cl(cl(E)).

2. cl(E) is finite, if so is E.

3. cl(E) is sound, if so is E.

4. cl(E) is closed with respect to 0 substitutions and symmetry, if so is E.

5. cl(E) and E prove the same equations, if E contains the equations in Table 3.

Proof: We limit ourselves to sketching a proof of the second statement in the lemma. To prove this claim, we begin by noting that the size of the term t′ is smaller than that of t whenever t ⇝ t′. Using this observation, it is not hard to see that, for each term t, the set

{t′ | t ⇝^{∗} t′}

is finite. In fact, the rooted tree with root t resulting from the unfolding of the directed acyclic graph whose nodes are the terms reachable from t via ⇝^{∗}, and whose edges are given by the ⇝ relation is finitely branching, and all of its paths are finite because the ⇝ relation decreases the size of terms. Thus this tree must be finite, or else it would have an infinite path by König’s lemma. It follows that, for each equation t ≈ u in E, the set cl(E) contains nm equations, where n and m are the cardinalities of the sets {t′ | t ⇝^{∗} t′} and {u′ | u ⇝^{∗} u′}, respectively. We may therefore conclude that cl(E) is finite, if so is E. □

We now proceed to characterize syntactically the normal forms of the rewriting relation ⇝. The syntactic characterization of the normal forms given below will be useful in obtaining the promised result to the effect that if a saturated axiom system E proves a closed equation relating two terms containing no occurrences of 0 as a summand or factor, then there is a closed proof for it in which all of the terms have no occurrences of 0 as a summand or factor.

Definition 2.10 For each CCS_{H} term t, we define t/0 thus:

0/0 = 0  (t + u)/0 = \begin{cases}u/0 & if t \underline{↔} 0 \\ t/0 & if u \underline{↔} 0 \\ (t/0) + (u/0) & otherwise \end{cases}

x/0 = x  (t |^{/} u)/0 = \begin{cases}0 & if t \underline{↔} 0 \\ t/0 & if u \underline{↔} 0 \\ (t/0) |^{/} (u/0) & otherwise \end{cases}

μt/0 = μ(t/0)  (t | u)/0 = \begin{cases}u/0 & if t \underline{↔} 0 \\ t/0 & if u \underline{↔} 0 \\ (t/0) | (u/0) & otherwise . \end{cases}

Intuitively, t/0 is the term that results by removing all occurrences of 0 as a summand or factor from t.

The following lemma, whose simple proof by structural induction on terms is omitted, collects the basic properties of the above construction. In particular, note that, as expected, the term t/0 is the normal form for t with respect to the rewrite relation ⇝.

Lemma 2.3 For each CCS_{H} term t, the following statements hold:

1. t ⇝^{∗} t/0 and therefore t \underline{↔} t/0;

2. t/0 ⇝ u for no term u; 3. the term t/0 has no occurrence of 0 as a summand or factor;

4. t/0 = t, if t has no occurrence of 0 as a summand or factor.

We are now ready to state our counterpart of [28, Proposition 5.1.5].

Proposition 2.1 Assume that E is a saturated axiom system. Suppose furthermore that we have a closed proof from E of the closed equation p ≈ q. Then replacing each term r in that proof with r/0 yields a closed proof of the equation p/0 ≈ q/0. In particular, the proof from E of an equation p ≈ q, where p and q are terms not containing occurrences of 0 as a summand or factor, need not use terms containing occurrences of 0 as a summand or factor.

Proof: The proof follows the lines of that of [28, Proposition 5.1.5], and is therefore omitted. □

In light of this result, since the saturation of a finite axiom system that includes the equations in Table 3 results in an equivalent, finite collection of equations (Lemma 2.2(2) and (5)), we put forth our last:

Simplifying Assumption 4 Henceforth, we shall limit ourselves to considering saturated axiom systems.

The use of saturated axiom systems will play an important role in the proof of our main technical results.

3 Hennessy’s Merge is not Finitely Based

Our order of business in the remainder of this paper will be to show the following result to the effect that bisimulation equivalence does not admit a finite equational axiomatization over the language CCS_{H}, and that thus Bergstra and Klop were indeed right in writing in [8, page 118] that:

“It seems that γ does not have a finite equational axiomatization.”

(In op. cit. Bergstra and Klop used γ to denote Hennessy’s merge.)

Theorem 3.1 Bisimulation equivalence admits no finite equational axiomatization over the language CCS_{H}. In fact, the collection of closed equations over that language that hold with respect to bisimulation equivalence has no finite equational axiomatization.

As a first stepping stone towards the proof of this result, we now proceed to argue that it is sufficient to show that bisimulation equivalence admits no finite equational axiomatization over the language CCS_{H}^{−}, consisting of the CCS_{H} terms that do not contain occurrences of the parallel composition operator. Even though this observation is not unexpected—as equation (2) essentially states that parallel composition is a derived operator in the algebra of CCS_{H} terms modulo bisimulation equivalence—, we now argue for it in some detail for the sake of completeness.

Definition 3.1 For each CCS_{H} term t, we define t̂thus:

\begin{aligned}ˆ0 & = & 0 & { \atop t + u} & = & t̂+ û \\ x̂ & = & x & { \atop t |^{/} u} & = & t̂|^{/} û \\ μ̂t & = & μt̂ & t̂ | u & = & (t̂|^{/} û) + (û |^{/} t̂) \end{aligned} .

If E is an axiom system over the language CCS_{H}, then

Ê = {t̂≈ û | (t ≈ u) ∈ E} .

Note that, for each CCS_{H} term t, the term t̂ is in the language CCS_{H}^{−}. Moreover, if t contains no occurrences of the parallel composition operator, then t̂= t. Since equation (2) is sound with respect to bisimulation equivalence, and bisimilarity is a congruence (Fact 2.1), it is not hard to show that:

Fact 3.1 Each term t in the language CCS_{H} is bisimilar to t̂. Therefore if E is an axiom system over the language CCS_{H} that is sound with respect to bisimilarity, then Ê is an axiom system over the language CCS_{H}^{−} that is sound with respect to bisimilarity.

The following result states the promised reduction of the non-finite axiomatizability of bisimilarity over the language CCS_{H} to that of bisimilarity over the language CCS_{H}^{−}.

Proposition 3.1 Let E be an axiom system over the language CCS_{H}. Then the following statements hold.

1. If E proves the equation t ≈ u, then Ê proves the equation t̂≈ û.

2. If E gives a complete axiomatization of bisimulation equivalence over the language CCS_{H}, then Ê completely axiomatizes bisimulation equivalence over the language CCS_{H}^{−}.

3. If bisimulation equivalence admits no finite equational axiomatization over the language CCS_{H}^{−}, then it has no finite equational axiomatization over the language CCS_{H} either.

Proof: We prove the three statements separately.

• Proof of Statement 1. Assume that E ⊢ t ≈ u. We shall argue that Ê proves the equation t̂ ≈ û by induction on the depth of the proof of t ≈ u from E. We proceed by a case analysis on the last rule used in the proof. Below we only consider the two most interesting cases in this analysis.

– Case E ⊢ t ≈ u, because σ(t′) = t and σ(u′) = u for some equation (t′ ≈ u′) ∈ E. Note, first of all, that, by the definition of Ê, the equation t̂′ ≈ û′ is contained in Ê. Observe now that

t̂= σ̂(t̂′) and û = σ̂(û′) ,

where σ̂ is the substitution mapping each variable x to the term σ̂(x). It follows that the equation t̂≈ û can be proven from the axiom system Ê by instantiating the equation t̂′ ≈ û′ with the substitution σ̂, and we are done.

– Case E ⊢ t ≈ u, because t = t_{1} | t_{2} and u = u_{1} | u_{2} for some t_{i}, u_{i} (i = 1, 2) such that E ⊢ t_{i} ≈ u_{i} (i = 1, 2). Using the inductive hypothesis twice, we have that Ê ⊢ t̂_{i} ≈ û_{i} (i = 1, 2). Therefore, using substitutivity, Ê proves that

t̂= (t̂_{1} |^{/} t̂_{2}) + (t̂_{2} |^{/} t̂_{1}) ≈ (û_{1} |^{/} û_{2}) + (û_{2} |^{/} û_{1}) = û ,

which was to be shown.

The remaining cases are simpler, and we leave the details to the reader.

• Proof of Statement 2. Assume that t and u are two bisimilar terms in the language CCS_{H}^{−}. We shall argue that Ê proves the equation t ≈ u. To this end, we begin by noting that the equation t ≈ u also holds in the algebra of CCS_{H} terms modulo bisimulation. In fact, for each term v in the language CCS_{H} and closed substitution σ mapping variables to CCS_{H} terms, we have that

σ(v) \underline{↔} σ̂(v) ,

where the substitution σ̂ is defined as above.

Since E is complete for bisimilarity over CCS_{H} by our assumptions, it follows that E proves the equation t ≈ u. Therefore, by statement 1 of the proposition, we have that Ê proves the equation t̂ ≈ û. The claim now follows because t̂= t and û = u.

• Proof of Statement 3. This is an immediate consequence of statement 2 because Ê has the same cardinality of E, and is therefore finite, if so is E.

□

In light of this result, henceforth we shall focus on proving that bisimulation equivalence affords no finite equational axiomatization over the language CCS_{H}^{−}. The following infinite family of closed CCS_{H}^{−} terms will play a key role in the technical developments to follow:

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

where the terms p_{n} are defined thus:

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

It is not hard to see that all of the equations e_{n} (n ≥ 0) are sound modulo bisimulation. In the remainder of this paper, we shall prove the following result, of which Theorem 3.1 is an immediate consequence, to the effect that no finite collection of equations over the language CCS_{H}^{−} that are sound with respect to bisimulation equivalence can prove all of the equations e_{n} (n ≥ 0).

Theorem 3.2 Let E be a finite axiom system over the language CCS_{H}^{−} that is sound with respect to bisimulation equivalence. Let n be larger than the size of each term in the equations in E. Then E does not prove the sound equation e_{n} from (3).

The remainder of this paper will be devoted to a proof of the above result, which will be given along proof theoretic lines that have their roots in Moller’s arguments to the effect that bisimulation equivalence is not finitely based over the language CCS—see the references [28, 29, 30]. More precisely, to establish Theorem 3.2, we shall show that there is a property of terms associated with each finite axiom system E over the language CCS_{H}^{−} that is sound with respect to bisimulation equivalence, such that whenever the equation p ≈ q can be derived from E, for some “suitably large” closed terms without 0 summands and factors, then either both p and q enjoy the property, or none of them does. The aforementioned property must be chosen so that, for suitably large values of n, the right-hand side of equality e_{n}, viz. the term a0 |^{/} p_{n}, affords it, whilst the left-hand side, viz. the term ap_{n} + ∑_{i=0}^{n} τa^{i}, does not.

Remark 3.1 In the absence of synchronization, Hennessy’s merge reduces to the left merge operator of Bergstra and Klop’s. It follows that the collection of closed equations that hold modulo \underline{↔} over the sub-language of CCS_{H} obtained by considering those terms that do not contain occurrences of the ā prefixing operator has a finite equational axiomatization. Therefore the use of synchronization is necessary in the proof of Theorem 3.1.

The following proposition states the property mentioned in the proof strategy outlined above.

Proposition 3.2 Let E be a finite axiom system over the language CCS_{H}^{−} that is sound with respect to bisimulation equivalence. Let n be larger than the size of each term in the equations in E. Assume that p and q are closed terms that are bisimilar to a0 |^{/} p_{n}, and contain no occurrences of 0 as a summand or a factor. If E ⊢ p ≈ q and p has a summand bisimilar to a0 |^{/} p_{n}, then so does q.

Using the above proposition, it is a simple matter to prove Theorem 3.2. In fact, since none of the summands of the term

ap_{n} + ∑_{i=0}^{n} τa^{i} ,

viz. ap_{n} and τa^{i} (i ∈ {0, …, n}), is bisimilar to a0 |^{/} p_{n}, if n ≥ 1, Proposition 3.2 yields that the sound equality e_{n} cannot be proven from E, and thus that E is incomplete.

We shall now begin to develop the technical machinery that will be brought to bear in the proof of Proposition 3.2. This proof will occupy the remainder of this study.

4 Preparatory Results and Observations

Note that terms in the language CCS_{H}^{−} may contain some occurrences of variables that can never contribute to the behaviour of their closed instantiations. A typical example of this situation occurs in the term 0 |^{/} x, which is bisimilar to 0. However, terms that have no 0 factors contain no such redundant occurrences of variables. Moreover, each variable occurring in such terms contributes to the behaviour of its closed substantial instantiations. The following basic result, that will be used repeatedly in the technical developments to follow, formalizes this intuition.

Lemma 4.1 Let t be a CCS_{H}^{−} term, and let σ be a closed substitution.

1. Assume that t is not bisimilar to 0, and σ is substantial. Then depth(σ(t)) is positive, and thus σ(t) \underline{↔} / 0.

2. If t has no 0 factors and x ∈ var(t), then depth(σ(t)) ≥ depth(σ(x)).

Remark 4.1 The requirement that σ be substantial is necessary in statement 1 of the above lemma. For example, x \underline{↔} / 0, but σ(x) \underline{↔} 0 if depth(σ(x)) = 0.

Similarly, the proviso that t has no 0 factors cannot be omitted in statement 2. For instance, if t = 0 |^{/} x and σ(x) = a0, then depth(σ(t)) < depth(σ(x)).

In the proof of our main result, we shall make use of some notions from [27, 28]. These we now proceed to introduce for the sake of completeness and readability.

Definition 4.1 A closed term p is irreducible if p \underline{↔} q | r implies q \underline{↔} 0 or r \underline{↔} 0, for all closed terms q, r.

We say that p is prime if it is irreducible and is not bisimilar to 0.

For example, each term p of depth 1 is prime because every term of the form q | r that does not involve 0 factors has depth at least 2, and thus cannot be bisimilar to p. The following proposition states the primality of two families of closed terms that will play a key role in the proof of our main result.

Proposition 4.1

1. Let m ≥ 1 and 0 ≤ i_{1} < … < i_{m}. Then the term ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} is prime. In particular, p_{n} is prime, for each n ≥ 1.

2. The term a0 |^{/} p_{n} is prime, for each n ≥ 0.

Proof: We prove the two claims separately. In each case, since ā.a^{i_{1}} +⋯+ā.a^{i_{m}} and a0 |^{/} p_{n} are not bisimilar to 0, it suffices only to show that the relevant term is irreducible.

• Proof of claim 1. Suppose, towards a contradiction, that there exist closed terms q, r that are not bisimilar 0 such that

ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} \underline{↔} q | r .

Then, since q, r \underline{↔} / 0, in light of the above equivalence we have that q →^{ā} q′ and r →^{ā} r′, for some q′, r′. But then it follows that

q | r →^{ā} q′ | r →^{ā} q′ | r′ ,

whereas the term ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} cannot perform two subsequent ātransitions. It follows that such q and r cannot exist, and hence that the term ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} is irreducible, which was to be shown.

• Proof of claim 2. We now proceed to prove that a0 |^{/} p_{n} is irreducible for n ≥ 0.

If n = 0 then a0 |^{/} p_{0} = a0 |^{/} 0 is a term of depth 1, and is therefore irreducible as claimed.

Let n ≥ 1. Assume, towards a contradiction, that a0 |^{/} p_{n} \underline{↔} p | q for two closed terms p and q with p \underline{↔} / 0 and q \underline{↔} / 0—that is, a0 |^{/} p_{n} is not irreducible. Since n ≥ 1, we have that

a0 |^{/} p_{n} →^{τ} 0 | 0 \underline{↔} 0 .

As a0 |^{/} p_{n} \underline{↔} p | q, there is a transition p | q →^{τ} p′ | q′, for some p′, q′ with p′ | q′ \underline{↔} 0. In light of our assumption that p \underline{↔} / 0 and q \underline{↔} / 0, the transition p | q →^{τ} p′ | q′ must be derived from the synchronization of two transitions p →^{α} p′ and q →^{ᾱ} q′ with α ∈ {a, ā}. This means that p | q →^{ā}, contradicting the assumption that a0 |^{/} p_{n} \underline{↔} p | q. Thus a0 |^{/} p_{n} is irreducible, which was to be shown.

□

Lemma 4.2 Let t be a term in the language CCS_{H}^{−} with neither 0 summands nor factors that does not have + as head operator. Assume that σ is a closed substantial substitution, and that

σ(t) \underline{↔} ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} ,

for some m > 1 and 0 ≤ i_{1} < … < i_{m}. Then t = x, for some variable x.

Proof: Assume, towards a contradiction, that t is not a variable. We proceed by a case analysis on the possible form this term may have.

1. Case t = μt′ for some term t′. Then μ = ā and a^{i_{1}} \underline{↔} σ(t′) \underline{↔} a^{i_{m}}. However, this is a contradiction because, since i_{1} ≠ i_{m}, the terms a^{i_{1}} and a^{i_{m}} are not bisimilar.

2. Case t = t′ |^{/} t′′ for some terms t′, t′′. Since t has no 0 factors, we have that neither t′ nor t′′ is bisimilar to 0. As σ is a substantial substitution, it follows that σ(t′) \underline{↔} / 0 and σ(t′′) \underline{↔} / 0.

Observe now that ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} →^{ā} a^{i_{m}}. Thus, as

σ(t) = σ(t′) |^{/} σ(t′′) \underline{↔} ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} ,

there is a term p such that

σ(t′) →^{ā} p and p | σ(t′′) \underline{↔} a^{i_{m}} .

As σ(t′′) \underline{↔} / 0, this implies that σ(t′′) →^{a} q, for some q. This leads to a contradiction, because the term σ(t) = σ(t′) |^{/} σ(t′′) affords an initial τtransition, viz.

σ(t) = σ(t′) |^{/} σ(t′′) →^{τ} p | q ,

whereas ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} does not.

We may therefore conclude that t must be a variable, which was to be shown. □

The following decomposition property will find application in the proof of our main technical result, viz. Proposition 5.1 to follow.

Lemma 4.3 Let n ≥ 1. Assume that p |^{/} q \underline{↔} a0 |^{/} p_{n}, where q is a closed term that is not bisimilar to 0. Then p \underline{↔} a0 and q \underline{↔} p_{n}.

Proof: Since p |^{/} q \underline{↔} a0 |^{/} p_{n} and a0 |^{/} p_{n} →^{a} 0 | p_{n} \underline{↔} p_{n}, there is a p′ such that p →^{a} p′ and p′ | q \underline{↔} p_{n}. It follows that q \underline{↔} p_{n} and p′ \underline{↔} 0, because p_{n} is prime (Proposition 4.1) and q \underline{↔} / 0. We are therefore left to prove that p is bisimilar to a0. To this end, note, first of all, that, as \underline{↔} is a congruence over the language CCS_{H}, we have that

p |^{/} p_{n} \underline{↔} a0 |^{/} p_{n} .

Assume now that p →^{μ} p′′ for some action μ and closed term p′′. In light of the above equivalence, one of the following two cases may arise:

1. μ = a and p′′ | p_{n} \underline{↔} p_{n} or

2. μ = τ and p′′ | p_{n} \underline{↔} a^{i}, for some i ∈ \{0, …, n\}.

In the former case, p′′ must have depth 0 and is thus bisimilar to 0. The latter case is impossible, because the depth of p′′ | p_{n} is at least n + 1.

We may therefore conclude that every transition of p is of the form p →^{a} p′′, for some p′′ \underline{↔} 0. Since we have already seen that p affords an a-labelled transition leading to 0, modulo bisimulation equivalence, it follows that p \underline{↔} a0, which was to be shown. □

Lemma 4.4 Let t ≈ u be an equation over the language CCS_{H}^{−} that is sound with respect to bisimulation equivalence, where t and u are terms that have neither 0 summands nor factors. Assume that some variable x occurs as a summand in t. Then x also occurs as a summand in u.

Proof: Recall that, for some finite index sets I, J, we can write

t = ∑_{i∈I} t_{i} and  (4)
u = ∑_{j∈J} u_{j} ,  (5)

where none of the t_{i} (i ∈ I) and u_{j} (j ∈ J) is 0 or a sum. Assume that variable x occurs as a summand in t—i.e., that there is an i ∈ I with t_{i} = x. We shall argue that x also occurs as a summand in u—i.e., that there is a j ∈ J with u_{j} = x.

Consider the substitution σ_{0} mapping each variable to 0. Pick an integer m larger than the depth of σ_{0}(t) and of σ_{0}(u). Let σ be the substitution mapping x to the term a^{m+1} and agreeing with σ_{0} on all the other variables.

As t ≈ u is sound with respect to bisimulation equivalence, we have that

σ(t) \underline{↔} σ(u) .

Moreover, the term σ(t) affords the transition σ(t) →^{a} a^{m}, for t_{i} = x and σ(x) = a^{m+1} →^{a} a^{m}. Hence, for some closed term p,

σ(u) = ∑_{j∈J} σ(u_{j}) →^{a} p \underline{↔} a^{m} .

This means that there is a j ∈ J such that σ(u_{j}) →^{a} p. We claim that this u_{j} can only be the variable x. To see that this claim holds, observe, first of all, that x ∈ var(u_{j}). In fact, if x did not occur in u_{j}, then we would reach a contradiction thus:

m = depth(p) < depth(σ(u_{j})) = depth(σ_{0}(u_{j})) ≤ depth(σ_{0}(u)) < m .

Using this observation and Lemma 4.1(2), it is not hard to show that, for each of the other possible forms u_{j} may have, σ(u_{j}) does not afford an a-labelled transition leading to a term of depth m. We may therefore conclude that u_{j} = x, which was to be shown. □

5 Proof of Proposition 3.2

We now proceed to present a detailed proof of Proposition 3.2. The following result, stating that the property mentioned in the statement of that proposition holds for all closed substantial instantiations of axioms in E, will be the crux in such a proof.

Proposition 5.1 Let t ≈ u be an equation over the language CCS_{H}^{−} that is sound with respect to bisimulation equivalence, where t and u are terms without 0 summands or factors. Let n be larger than the size of t. Assume that σ is a substantial substitution. Let p = σ(t) and q = σ(u). Suppose that p and q are bisimilar to a0 |^{/} p_{n}. If p has a summand bisimilar to a0 |^{/} p_{n}, then so does q.

Proof: We can assume that, for some finite non-empty index sets I, J,

t = ∑_{i∈I} t_{i} and  (6)
u = ∑_{j∈J} u_{j} ,  (7)

where none of the t_{i} (i ∈ I) and u_{j} (j ∈ J) is 0 or a sum. (That is, none of the t_{i} (i ∈ I) and u_{j} (j ∈ J) has + as its head operator.) Note that, as t and u have no 0 summands or factors, then none of the t_{i} (i ∈ I) and u_{j} (j ∈ J) does either.

Since p = σ(t) has a summand bisimilar to a0 |^{/} p_{n}, there is an index i ∈ I such that

σ(t_{i}) \underline{↔} a0 |^{/} p_{n} .

Our aim is now to show that there is an index j ∈ J such that

σ(u_{j}) \underline{↔} a0 |^{/} p_{n} ,

proving that q = σ(u) also has a summand bisimilar to a0 |^{/} p_{n}. This we proceed to do by a case analysis on the form t_{i} may have.

1. Case t_{i} = x for some variable x. In this case, we have that

σ(x) \underline{↔} a0 |^{/} p_{n} ,

and t has x as a summand. As t ≈ u is sound with respect to bisimulation equivalence and neither t nor u have 0 summands or factors, it follows that u also has x as a summand (Lemma 4.4). Thus there is an index j ∈ J such that u_{j} = x, and, modulo bisimulation, σ(u) has a0 |^{/} p_{n} as a summand, which was to be shown.

2. Case t_{i} = μt′ for some term t′. This case is vacuous because, since

σ(t_{i}) = μσ(t′) →^{μ} σ(t′)

is the only transition afforded by σ(t_{i}), this term cannot be bisimilar to a0 |^{/} p_{n}.

3. Case t_{i} = t′ |^{/} t′′ for some terms t′, t′′. The analysis of this case is the crux of the proof, and we present the argument in considerable detail.

Since t_{i} = t′ |^{/} t′′, we have that

σ(t_{i}) = σ(t′) |^{/} σ(t′′) \underline{↔} a0 |^{/} p_{n} .

As σ is a substantial substitution, it follows that σ(t′) \underline{↔} / 0 and σ(t′′) \underline{↔} / 0 (Lemma 4.1(1)). Thus σ(t′) \underline{↔} a0 and σ(t′′) \underline{↔} p_{n} (Lemma 4.3). Now, t′′ can be written thus:

t′′ = v_{1} + ⋯ + v_{ℓ} (ℓ > 0) ,

where none of the summands v_{i} is 0 or a sum. Observe that, since n is larger than the size of t, we have that ℓ < n. Hence, since

σ(t′′) \underline{↔} p_{n} = ∑_{i=0}^{n} āa^{i} ,

there must be some h ∈ {1, …, ℓ} such that

σ(v_{h}) \underline{↔} ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}}

for some m > 1 and 0 ≤ i_{1} < … < i_{m} ≤ n. By Lemma 4.2, it follows that v_{h} can only be a variable x and thus that

σ(x) \underline{↔} ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} .  (8)

Since t′ has no 0 factors, the above equation yields that x ∉ var(t′)—or else σ(t′) \underline{↔} / a0 (Lemma 4.1(2)). Thus, since σ is substantial, modulo bisimulation equivalence,

t′ = y_{1} + ⋯ + y_{k}[+a0]  (9)

for some k ≥ 0 and some variables y_{1}, …, y_{k} different from x with

σ(y_{1}) \underline{↔} ⋯ σ(y_{k}) \underline{↔} a0 .

(The notation [+a0] in (9) denotes an optional a0 summand. Moreover, if k = 0, then t′ = a0.) So, modulo bisimulation equivalence, t_{i} has the form t′ |^{/} (x + t′′′), for some term t′′′.

Our order of business will now be to use the information collected so far in this case of the proof to argue that σ(u) has a summand bisimilar to a0 |^{/} p_{n}. To this end, consider the substitution

σ′ = σ[x ↦ ā(a0 |^{/} p_{n})] .

We have that

σ′(t_{i}) = σ′(t′) |^{/} σ′(t′′)
= σ(t′) |^{/} σ′(t′′) (As x ∉ var(t′))
\underline{↔} a0 |^{/} (ā(a0 |^{/} p_{n}) + σ′(t′′′)) .

Thus, σ′(t_{i}) →^{τ} p′ \underline{↔} a0 |^{/} p_{n} for some p′. By (6), we have that σ′(t) →^{τ} p′ also holds. Since t ≈ u is sound with respect to \underline{↔} , it follows that σ′(t) \underline{↔} σ′(u). Hence, by (7), there are a j ∈ J and a q′ such that

σ′(u_{j}) →^{τ} q′ \underline{↔} a0 |^{/} p_{n} .  (10)

Recall that, by one of the assumptions of the proposition, σ(u) \underline{↔} a0 |^{/} p_{n}, and thus σ(u) has depth n + 2. On the other hand, by (10), depth(σ′(u_{j})) ≥ n + 3. Since σ and σ′ differ only in the closed term they map variable x to, it follows that

x ∈ var(u_{j}) .  (11)

We now proceed to show that σ(u_{j}) \underline{↔} a0 |^{/} p_{n} by a further case analysis on the form a term u_{j} satisfying (10) and (11) may have.

(a) Case u_{j} = x. This case is vacuous because σ′(x) = ā(a0 |^{/} p_{n}) ↛^{τ}, and thus this possible form for u_{j} does not meet (10).

(b) Case u_{j} = μu′ for some term u′. In light of (10), we have that μ = τ and q′ = σ′(u′) \underline{↔} (a0 |^{/} p_{n}). Using (11) and the fact that u′ has no 0 factors, we have that depth(σ′(u′)) ≥ n + 3 (Lemma 4.1(2)). Since a0 |^{/} p_{n} has depth n+2, this contradicts the fact that σ′(u′) \underline{↔} a0 |^{/} p_{n}.

(c) Case u_{j} = u′ |^{/} u′′ for some terms u′, u′′. This is the lengthiest sub-case of case 3 of the proof, and its analysis will occupy us for the next couple of pages. Our assumption that u has no 0 factors yields that neither u′ nor u′′ is bisimilar to 0. Moreover, by (11), either x ∈ var(u′) or x ∈ var(u′′). Since σ′(u_{j}) = σ′(u′) |^{/} σ′(u′′) affords transition (10), we have that q′ = q_{1} | q_{2} for some q_{1}, q_{2}. Since a0 |^{/} p_{n} is prime (Proposition 4.1(2)), it follows that either q_{1} \underline{↔} 0 or q_{2} \underline{↔} 0. We now continue our proof by examining the two possible origins for transition (10). These are

i. σ′(u′) →^{τ} q_{1} and q_{2} = σ′(u′′) and

ii. σ′(u′) →^{α} q_{1} and σ′(u′′) →^{ᾱ} q_{2}, with α ∈ {a, ā}.

We examine these two cases in turn. i. Assume that σ′(u′) →^{τ} q_{1} and q_{2} = σ′(u′′). We now proceed to

argue that this case produces a contradiction. To this end, note first of all that, as σ′ is substantial and u′′ is not bisimilar to 0, it must be the case that q_{1} \underline{↔} 0 and q_{2} = σ′(u′′) \underline{↔} a0 |^{/} p_{n}. In light of the definition of σ′, it follows that x occurs in u′, but not in u′′ (Lemma 4.1(2)). Therefore, since σ and σ′ only differ at the variable x,

σ(u′′) = σ′(u′′) \underline{↔} a0 |^{/} p_{n} .

Since \underline{↔} is a congruence, we derive that

σ(u_{j}) = σ(u′) |^{/} σ(u′′) \underline{↔} σ(u′) |^{/} (a0 |^{/} p_{n}) . (12)

Since σ is substantial, x occurs in u′, and u′ has no 0 factors, we may infer that

n + 2 = depth(a0 |^{/} p_{n})
= depth(σ(u)) (As σ(u) \underline{↔} a0 |^{/} p_{n})
≥ depth(σ(u_{j})) (By (7))
= depth(σ(u′)) + n + 2 (By (12))
> n + 2 (As depth(σ(u′)) > 0 by Lemma 4.1(2)) ,

which is the desired contradiction. ii. Assume now that σ′(u′) →^{α} q_{1} and σ′(u′′) →^{ᾱ} q_{2}, with α ∈ {a, ā}.

Recall that exactly one of q_{1}, q_{2} is bisimilar to 0. We proceed with the proof by considering these two possible cases in turn.

Case q_{1} \underline{↔} 0. Our order of business will be to argue that, in this case, σ(u_{j}) \underline{↔} a0 |^{/} p_{n}, and thus that q = σ(u) has a summand bisimilar to a0 |^{/} p_{n}. To this end, observe, first of all, that q_{2} \underline{↔} a0 |^{/} p_{n} by (10). It follows that x ∈ var(u′′), for otherwise we could derive a contradiction thus:

depth(a0 |^{/} p_{n}) = depth(σ(u)) (As σ(u) \underline{↔} a0 |^{/} p_{n})
≥ depth(σ(u_{j})) (By (7))
> depth(σ(u′′)) (As depth(σ(u′)) > 0)
= depth(σ′(u′′)) (As x ∉ var(u′′))
> depth(a0 |^{/} p_{n})

(As σ′(u′′) →^{ᾱ} q_{2} \underline{↔} a0 |^{/} p_{n}) .

Moreover, we claim that x ∉ var(u′). Indeed, if x also occurred in u′, then, since u′ has no 0 factors, the term σ(x) would contribute to the behaviour of σ(u_{j}). Therefore, by (8), the term σ(u_{j}) would afford a sequence of actions containing two occurrences of ā, contradicting our assumption that σ(u) \underline{↔} a0 |^{/} p_{n}. It follows that α = a, because

σ′(u′) = σ(u′) ↛^{ā} ,

since σ(u) \underline{↔} a0 |^{/} p_{n}. Observe now that, as σ′(u′′) →^{ā} q_{2} \underline{↔} a0 |^{/} p_{n}, it must be the case that u′′ has a summand x. To see that this does hold, we examine the other possible forms a summand w of u′′ responsible for the transition

σ′(u′′) →^{ā} q_{2} \underline{↔} a0 |^{/} p_{n}

may have, and argue that each of them leads to a contradiction. A. Case w = āw′, for some term w′. In this case, q_{2} =

σ′(w′). However, the depth of such a q_{2} is either smaller than n + 2 (if x ∉ var(w′)), or larger than n + 2 (if x ∈ var(w′)). This contradicts the fact that q_{2} is bisimilar to a0 |^{/} p_{n}, because the latter term has depth n + 2.

B. Case w = w_{1} |^{/} w_{2}, for some terms w_{1} and w_{2}. Since

σ′(w) = σ′(w_{1}) |^{/} σ′(w_{2}) →^{ā} q_{2} ,

there is a closed term q_{3} such that σ′(w_{2}) →^{ā} q_{3} and q_{2} = q_{3} | σ′(w_{2}) \underline{↔} a0 |^{/} p_{n}. As the term a0 |^{/} p_{n} is prime, σ′ is substantial, and w_{2} is not bisimilar to 0, we may infer that q_{3} \underline{↔} 0 and

σ′(w_{2}) \underline{↔} a0 |^{/} p_{n} .

It follows that x ∉ var(w_{2})—or else the depth of σ′(w_{2}) would be at least n + 3—, and therefore that

σ′(w_{2}) = σ(w_{2}) \underline{↔} a0 |^{/} p_{n} .

However, this contradicts our assumption that σ(u) \underline{↔} a0 |^{/} p_{n}.

Summing up, we have argued that u′′ has a summand x. Therefore, by (8),

σ(u′′) \underline{↔} ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} + r′′ ,

for some closed term r′′. We have already noted that

σ(u′) = σ′(u′) →^{a} q_{1} \underline{↔} 0 .

Therefore, we have that

σ(u′) \underline{↔} a0 + r′ ,

for some closed term r′. Using the congruence properties of bisimulation equivalence, we may infer that

σ(u_{j}) = σ(u′) |^{/} σ(u′′) \underline{↔} (a0+r′) |^{/} (ā.a^{i_{1}} +⋯+ā.a^{i_{m}} +r′′) .

In light of this equivalence, we have that

σ(u_{j}) →^{a} r \underline{↔} ā.a^{i_{1}} + ⋯ + ā.a^{i_{m}} + r′′ \underline{↔} σ(u′′) ,

for some closed term r. By (7),

q = σ(u) →^{a} r .

Since q = σ(u) \underline{↔} a0 |^{/} p_{n} by our assumption, it must be the case that r \underline{↔} σ(u′′) \underline{↔} p_{n}. So, again using the congruence properties of \underline{↔}, we have that

σ(u_{j}) = σ(u′) |^{/} σ(u′′) \underline{↔} (a0 + r′) |^{/} p_{n} .

As σ(u) \underline{↔} a0 |^{/} p_{n}, using Lemma 4.3 it is now a simple matter to infer that

σ(u′) \underline{↔} a0 .

Hence σ(u_{j}) \underline{↔} a0 |^{/} p_{n}. Note that σ(u_{j}) is a summand of q = σ(u). Therefore q has a summand bisimilar to a0 |^{/} p_{n}, which was to be shown. Case q_{2} \underline{↔} 0. We now proceed to argue that this case produces a contradiction. To this end, observe, first of all, that q_{1} \underline{↔} a0 |^{/} p_{n}. Reasoning as in the analysis of the previous case, we may infer that α = a, x occurs in u′, but x does not occur in u′′. Moreover, since σ′(u′) →^{a} q_{1} \underline{↔} a0 |^{/} p_{n}, it must be the case that u′ →^{a} u′′′ for some u′′′ such that

σ′(u′′′) = q_{1} \underline{↔} a0 |^{/} p_{n} .

(For, otherwise, using Lemma 2.1(3), we would have that

σ′(u′) →^{a} q_{1}

because u′ →^{y} c, σ(y) →^{a} q′_{1} and q_{1} = σ′[y_{d} ↦ q′_{1}](c), for some variable y, configuration c and closed term q′_{1}. Note that y ≠ x. In fact, if y = x, then we would have that a = ā by the definition of σ′, contradicting the distinctness of these two complementary actions. Observe now that, again in light of the definition of σ′, the variable x cannot occur in c, or else the depth of q_{1} = σ′[y_{d} ↦ q′_{1}](c) would be at least n + 3, contradicting our assumption that q_{1} \underline{↔} a0 |^{/} p_{n}. Hence, since the variable y is different from x, it is not hard to see that σ(u′) →^{a} q_{1} also holds, and thus that depth(q_{1}) < depth(σ(u)) = n + 2, contradicting our assumption that q_{1} \underline{↔} a0 |^{/} p_{n}.) Since u contains no 0 factors, in light of the definition of σ′, this u′′′ cannot contain occurrences of the variable x. (For, otherwise, Lemma 4.1(2) would yield that

depth(σ′(u′′′)) = depth(q_{1}) ≥ n + 3 ,

contradicting our assumption that q_{1} \underline{↔} a0 |^{/} p_{n}.) So

σ(u′′′) = q_{1} \underline{↔} a0 |^{/} p_{n}

also holds. Thus

n + 2 = depth(a0 |^{/} p_{n})
= depth(σ(u)) (As σ(u) \underline{↔} a0 |^{/} p_{n})
≥ depth(σ(u_{j})) (By (7))
= depth(σ(u′) |^{/} σ(u′′))
> depth(σ(u′′′)) + depth(σ(u′′))

(As σ(u′) →^{a} σ(u′′′))

> n + 2

(As depth(σ(u′′)) > 0 and depth(σ(u′′′)) = n + 2)

which is the desired contradiction. This completes the proof for the case u_{j} = u′ |^{/} u′′ for some terms u′, u′′.

The proof is now complete. □

We are now ready to prove Proposition 3.2, thus completing the proof of Theorem 3.2 and of our main result (Theorem 3.1).

Proof of Proposition 3.2: Assume that E is a finite axiom system over the language CCS_{H}^{−} that is sound with respect to bisimulation equivalence, and that the following hold, for some closed terms p and q and positive integer n larger than the size of each term in the equations in E:

1. E ⊢ p ≈ q,

2. p \underline{↔} q \underline{↔} a0 |^{/} p_{n},

3. p and q contain no occurrences of 0 as a summand or factor, and

4. p has a summand bisimilar to a0 |^{/} p_{n}.

We prove that q also has a summand bisimilar to a0 |^{/} p_{n} by induction on the depth of the closed proof of the equation p ≈ q from E. Recall that, without loss of generality, we may assume that the closed terms involved in the proof of the equation p ≈ q have no 0 summands or factors (by Proposition 2.1, as E may be assumed to be saturated), that applications of symmetry happen first in equational proofs (that is, E is closed with respect to symmetry), and that only closed substantial substitutions are used (E is closed with respect to 0-substititions).

We proceed by a case analysis on the last rule used in the proof of p ≈ q from E. The case of reflexivity is trivial, and that of transitivity follows immediately by using the inductive hypothesis twice. Below we only consider the other possibilities.

• Case E ⊢ p ≈ q, because σ(t) = p and σ(u) = q for some equation (t ≈ u) ∈ E and closed substantial substitution σ. Observe, first of all, that since σ(t) = p and σ(u) = q have no 0 summands or factors, then neither do t and u. Therefore, as n is larger than the size of each term mentioned in equations in E, the claim follows by Proposition 5.1.

• Case E ⊢ p ≈ q, because p = μp′ and q = μq′ for some p′, q′ such that E ⊢ p′ ≈ q′. This case is vacuous because p = μp′ \underline{↔} / a0 |^{/} p_{n}, and thus p does not have a summand bisimilar to a0 |^{/} p_{n}.

• Case E ⊢ p ≈ q, because p = p′ + p′′ and q = q′ + q′′ for some p′, q′, p′′, q′′ such that E ⊢ p′ ≈ q′ and E ⊢ p′′ ≈ q′′. Since p has a summand bisimilar to a0 |^{/} p_{n}, we have that so does either p′ or p′′. Assume, without loss of generality, that p′ has a summand bisimilar to a0 |^{/} p_{n}. Since p is bisimilar to a0 |^{/} p_{n}, so is p′. Using the soundness of E modulo bisimulation, it follows that q′ \underline{↔} a0 |^{/} p_{n}. The inductive hypothesis now yields that q′ has a summand bisimilar to a0 |^{/} p_{n}. Hence, q has a summand bisimilar to a0 |^{/} p_{n}, which was to be shown.

• Case E ⊢ p ≈ q, because p = p′ |^{/} p′′ and q = q′ |^{/} q′′ for some p′, q′, p′′, q′′ such that E ⊢ p′ ≈ q′ and E ⊢ p′′ ≈ q′′. Since the proof involves no uses of 0 as a summand or a factor, we have that p′, p′′ \underline{↔} / 0 and q′, q′′ \underline{↔} / 0. It follows that q is a summand of itself. By our assumptions,

a0 |^{/} p_{n} \underline{↔} q .

Therefore we have that q has a summand bisimilar to a0 |^{/} p_{n}, and we are done.

This completes the proof. □

6 Concluding Remarks

In their seminal paper [8], Bergstra and Klop showed that the parallel composition operator can be finitely axiomatized modulo bisimulation equivalence with the use of two auxiliary operators, viz. the by now classic left merge and communication merge. Independently, and at roughly the same time, Hennessy proposed the auxiliary operator |^{/}, and used it in [21] to give equational axiomatizations of Milner’s observation congruence [26] and timed congruence. The axiomatization of observation congruence offered by Hennessy using the |^{/} operator relies, however, on a variation on the classic expansion law [26], and is therefore infinite. This led Bergstra and Klop to conjecture in [8, page 118] that Hennessy’s |^{/} operator does not have a finite equational axiomatization. The main result in this paper confirms this conjecture of Bergstra and Klop’s, and answers one of the questions in [2, Problem 8], by showing that, in the presence of two distinct complementary actions, it is impossible to provide a finite axiomatization of the recursion free fragment of CCS modulo bisimulation equivalence using |^{/}. This result further reinforces the status of the left merge and the communication merge operators as auxiliary operators in the finite equational characterization of parallel composition in bisimulation semantics.

A natural question to ask at this point is whether there is a single binary operator that preserves bisimulation equivalence, and whose addition to the recursion free fragment of CCS allows for the finite equational axiomatization of parallel composition—see [2, Problem 8]. (As was recently pointed out to us by Jos Baeten and Rob van Glabbeek, it is certainly possible to obtain a finite axiomatization of bisimulation equivalence by adding one ternary operator to the signature of CCS.)

We conjecture that no such operator exists, and that the use of two auxiliary operators is therefore necessary to achieve a finite axiomatization of parallel composition in bisimulation semantics. This result would offer the definitive justification we seek for the canonical standing of the operators proposed by Bergstra and Klop. Work on the confirmation of this conjecture is under way, and we hope to report on it elsewhere in the near future.

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. The authors thank Zoltán Ésik for pointing out useful references on the study of the equational theory of shuffle in formal language theory.

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, BRICS Report NS-03-2, BRICS, Department of Computer Science, Aalborg University, September 2003.

[3] L. Aceto, B. Bloom, and F. Vaandrager, Turning SOS rules into equations, Information and Computation, 111 (1994), pp. 1–52.

[4] L. Aceto, W. Fokkink, and C. Verhoef, Structural operational semantics, in Handbook of Process Algebra, North-Holland, 2001, pp. 197–292.

[5] D. Austry and G. Boudol, Algèbre de processus et synchronisations, Theoretical Comput. Sci., 30 (1984), pp. 91–131.

[6] J. Baeten and E. de Vink, Axiomatizing GSOS with termination, in Proceedings of STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes-Juan les Pins, France, March 14–16, 2002, H. Alt and A. Ferreira, eds., vol. 2285 of Lecture Notes in Computer Science, Springer-Verlag, 2002, pp. 583–595.

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

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

[9] S. L. Bloom and Z. Ésik, Nonfinite axiomatizability of shuffle inequalities, in Proceedings of TAPSOFT’95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE, Aarhus, Denmark, May 22–26, 1995, P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, eds., vol. 915 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 318–333.

[10] , Free shuffle algebras in language varieties, Theoret. Comput. Sci., 163 (1996), pp. 55–98.

[11] , Axiomatizing shuffle and concatenation in languages, Inform. and Comput., 139 (1997), pp. 62–91.

[12] , Varieties generated by languages with poset operations, Math. Structures Comput. Sci., 7 (1997), pp. 701–713.

[13] , Shuffle binoids, RAIRO Inform. Théor. Appl., 32 (1998), pp. 175–198.

[14] Z. Ésik, Axiomatizing the subsumption and subword preorders on finite and infinite partial words, Theoret. Comput. Sci., 273 (2002), pp. 225–248. WORDS (Rouen, 1999).

[15] Z. Ésik and M. Bertol, Nonfinite axiomatizability of the equational theory of shuffle, Acta Inform., 35 (1998), pp. 505–539.

[16] Z. Ésik and S. Okawa, Series and parallel operations on pomsets, in Proceedings of Foundations of Software Technology and Theoretical Computer Science (Chennai, 1999), vol. 1738 of Lecture Notes in Comput. Sci., Springer-Verlag, Berlin, 1999, pp. 316–328.

[17] W. Fokkink and B. Luttik, An omega-complete equational specification of interleaving, in Proceedings 27th Colloquium on Automata, Languages and Programming—ICALP’00, Geneva, U. Montanari, J. Rolinn, and E. Welzl, eds., vol. 1853 of Lecture Notes in Computer Science, Springer-Verlag, July 2000, pp. 729–743.

[18] J. L. Gischer, The equational theory of pomsets, Theoretical Comput. Sci., 61 (1988), pp. 199–224.

[19] J. F. Groote, A new strategy for proving ω–completeness with applications in process algebra, in Proceedings CONCUR 90, Amsterdam, J. Baeten and J. Klop, eds., vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 314–331.

[20] M. Hennessy, Algebraic Theory of Processes, MIT Press, Cambridge, Massachusetts, 1988.

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

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

[23] C. Hoare, Communicating Sequential Processes, Prentice-Hall International, Englewood Cliffs, 1985.

[24] R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371–384.

[25] R. Milner, Flowgraphs and flow algebras, J. Assoc. Comput. Mach., 26 (1979), pp. 794–818.

[26] , Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

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

[28] 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.

[29] , 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.

[30] , 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.

[31] 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.

[32] G. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

[33] V. Pratt, Modeling concurrency with partial orders, International Journal of Parallel Programming, 15 (1986), pp. 33–71.

[34] R. de Simone, Higher-level synchronising devices in Meije–SCCS, Theoretical Comput. Sci., 37 (1985), pp. 245–267.

[35] S. T. Tschantz, Languages under concatenation and shuffling, Mathematical Structures in Computer Science, 4 (1994), pp. 505–511.

Recent BRICS Report Series Publications

RS-03-34 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. CCS with Hennessy’s Merge has no Finite Equational Axiomatization. November 2003. 37 pp.

RS-03-33 Olivier Danvy. A Rational Deconstruction of Landin’s SECD Machine. October 2003. 32 pp. This report supersedes the earlier BRICS report RS-02-53.

RS-03-32 Philipp Gerhardy and Ulrich Kohlenbach. Extracting Herbrand Disjunctions by Functional Interpretation. October 2003. 17 pp.

RS-03-31 Stephen Lack and Pawe� Sobociński. Adhesive Categories. October 2003. 25 pp.

RS-03-30 Jesper Makholm Byskov, Bolette Ammitzbøll Madsen, and Bjarke Skjernaa. New Algorithms for Exact Satisfiability. October 2003. 31 pp.

RS-03-29 Aske Simon Christensen, Christian Kirkegaard, and Anders Møller. A Runtime System for XML Transformations in Java. October 2003. 15 pp.

RS-03-28 Zoltán Ésik and Kim G. Larsen. Regular Languages Definable by Lindström Quantifiers. August 2003. 82 pp. This report supersedes the earlier BRICS report RS-02-20.

RS-03-27 Luca Aceto, Willem Jan Fokkink, Rob J. van Glabbeek, and Anna Ingólfsdóttir. Nested Semantics over Finite Trees are Equationally Hard. August 2003. 31 pp.

RS-03-26 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. August 2003. 23 pp. Extended version of a paper appearing in Hu and Rodríguez-Artalejo, editors, Sixth International Symposium on Functional and Logic Programming, FLOPS ’02 Proceedings, LNCS 2441, 2002, pages 134–151. This report supersedes the earlier BRICS report RS-02-30.

RS-03-25 Biernacki Dariusz and Danvy Olivier. From Interpreter to Logic Engine: A Functional Derivation. June 2003.

RS-03-24 Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines. June 2003. 13 pp.