BRICS

Basic Research in Computer Science

Bisimilarity is not Finitely Based over BPA with Interrupt

Luca Aceto Willem Jan Fokkink Anna Ingólfsdóttir Sumit Nain

BRICS Report Series RS-05-33

ISSN 0909-0878 October 2005 BRICS RS-05-33 Aceto et al.: Bisimilarity is not Finitely Based over BPA with Interrupt Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, Luca Aceto & Willem Jan Fokkink & Anna

Ingólfsdóttir & Sumit Nain. 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/05/33/

Bisimilarity is not Finitely Based over BPA with Interrupt

Luca Aceto^{c,a,∗}, Wan Fokkink^{e,b}, Anna Ingolfsdottir^{c,a} Sumit Nain^{d}

aBRICS (Basic Research in Computer Science), Centre of the Danish National Research Foundation, Department of Computer Science, Aalborg University, Fr. Bajersvej 7B, 9220

Aalborg Ø, Denmark.

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

cDepartment of Computer Science, School of Science and Engineering, Reykjavík University, Ofanleiti 2, 103 Reykjavík, Iceland.

dDepartment of Computer Science, Mail Stop 132, Rice University, 6100 S. Main Street, Houston, TX 77005-1892, USA.

eVrije Universiteit Amsterdam, Department of Computer Science, Section Theoretical Computer Science, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands.

Abstract

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop’s Basic Process Algebra with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based.

Key words: Concurrency, process algebra, Basic Process Algebra (BPA), interrupt, disrupt, bisimulation, equational logic, complete axiomatizations, non-finitely based algebras, expressiveness 1991 MSC:08A70, 03B45, 03C05, 68Q10, 68Q45, 68Q55, 68Q70

∗ Corresponding author.

Email addresses: luca@ru.is,luca@cs.aau.dk (Luca Aceto),

wanf@cs.vu.nl (Wan Fokkink), annai@ru.is,annai@cs.aau.dk (Anna

Ingolfsdottir), sumitnain@yahoo.com (Sumit Nain).

  URLs: http://www.cs.aau.dk/~luca (Luca Aceto),
http://www.cs.vu.nl/~wanf (Wan Fokkink),
http://www.cs.aau.dk/~annai (Anna Ingolfsdottir).

Preprint submitted to Elsevier Science

1 Introduction

Programming and specification languages often include constructs to specify mode switches (see, e.g., [8,11,23,24,26]). Indeed, some form of mode transfer in computation appears in the time-honoured theory of operating systems in the guise of, e.g., interrupts, in programming languages as exceptions, and in the behaviour of control programs and embedded systems as discrete “mode switches” triggered by changes in the state of their environment.

In light of the ubiquitous nature of mode changes in computation, it is not surprising that classic process description languages either include primitive operators to describe mode changes—for example, LOTOS [15,23] offers the so-called disruption operator—or have been extended with variations on mode transfer operators. For instance, examples of such operators that may be added to CCS are discussed by Milner in [25, pp. 192–193], and the reference [17] offers some discussion of the benefits of adding one of those, viz. the checkpointing operator, to that language.

In the setting of Basic Process Algebra (BPA), as introduced by Bergstra and Klop in [12], some of these extensions, and their relative expressiveness, have been discussed in the early paper [11]. That preprint of Bergstra’s has later been revised and extended in [7]. There, Baeten and Bergstra study the equational theory and expressiveness of BPA_{δ} (the extension of BPA with a constant δ to describe “deadlock”) enriched with two mode transfer operators, viz. the disrupt and interrupt operators. In particular, they offer an equational axiomatization of bisimulation equivalence [25,29] over the resulting extension of the language BPA_{δ}. This axiomatization is finite, if so is the underlying set of actions—a state of affairs that is most pleasing for process algebraists.

However, the axiomatization of bisimulation equivalence offered by Baeten and Bergstra in [7] relies on the use of four auxiliary operators—two per mode transfer operator. (Two of those auxiliary operators are, however, redundant since they are derived BPA operators.) Although the use of auxiliary operators in the axiomatization of behavioral equivalences over process description languages has been well established since Bergstra and Klop’s axiomatization of parallel composition using the left and communication merge operators [13], to our mind, a result like the aforementioned one always begs the question whether the use of auxiliary operators is necessary to obtain a finite axiomatization of bisimulation equivalence.

For the case of parallel composition, Moller showed in [27,28] that strong bisimulation equivalence is not finitely based over CCS [25] and PA [13] without the left merge operator. (The process algebra PA [13] contains a parallel composition operator based on pure interleaving without communication, and the left merge operator.) Thus auxiliary operators are necessary to obtain a finite axiomatization of parallel composition. But, is the use of auxiliary operators necessary to give a finite axiomatization of bisimulation equivalence over the language BPA enriched with the mode transfer operators studied by Baeten and Bergstra in [7]?

We address the above natural question in this paper. In particular, we mostly focus on BPA enriched with the interrupt operator. Intuitively, “p interrupted by q” describes a process that normally behaves like p. However, at each point of the computation before p terminates, q can interrupt it, and begin its execution. If this happens, p resumes its computation upon termination of q.

We show that, in the presence of a single action, bisimulation equivalence is not finitely based over BPA with the interrupt operator. Moreover, we prove that the collection of closed equations over this language is also not finitely based. This result provides evidence that the use of auxiliary operators in the technical developments presented in [7] is indeed necessary in order to obtain a finite axiomatization of bisimulation equivalence.

Our main result adds the interrupt operator to the list of operators whose addition to a process algebra spoils finite axiomatizability modulo bisimulation equivalence; see, e.g., [3,4,14,16,20,30,31] for other examples of non-finite axiomatizability results over process algebras, and some of their precursors in the setting of formal language theory. Of special relevance for concurrency theory are the aforementioned results of Moller’s to the effect that the process algebras CCS and PA without the auxiliary left merge operator from [12] do not have a finite equational axiomatization modulo bisimulation equivalence [27,28]. Recently, in collaboration with Luttik, the first three authors have shown in [5] that the process algebra obtained by adding Hennessy’s merge operator from [22] to CCS does not have a finite equational axiomatization modulo bisimulation equivalence. This result is in sharp contrast with a theorem established by Fokkink and Luttik in [18] to the effect that the process algebra PA [13] affords an ω-complete axiomatization that is finite if so is the underlying set of actions. Aceto, Ésik and Ingolfsdottir proved in [2] that there is no finite equational axiomatization that is ω-complete for the max-plus algebra of the natural numbers, a result whose process algebraic implications are discussed in [1]. Fokkink and Nain have shown in [19] that no congruence over the language BCCSP, a basic formalism to express finite process behaviour, that is included in possible worlds equivalence, and includes ready trace equivalence, affords a finite ω-complete equational axiomatization.

Having established that the addition of the interrupt operator to BPA spoils finite axiomatizability modulo bisimulation equivalence, it is natural to ask ourselves whether the same holds true for the disrupt operator from [7]. Intuitively, “p disrupted by q” describes a process that normally behaves like p. However, at each point of the computation before p terminates, q can pre-empt it, and begin its execution. If this happens, p never resumes its computation.

We show that, perhaps surprisingly, in sharp contrast to the main result of the paper, the use of auxiliary operators is not necessary in order to obtain a finite axiomatization of bisimulation equivalence over closed terms in the language obtained by enriching BPA with the disrupt operator. The key to this positive result is the distributivity of the disrupt operator with respect to the non-deterministic choice operator of BPA in its first argument—a property that is not afforded by the interrupt operator.

The paper is organized as follows. We begin by presenting the language BPA with the interrupt operator, its operational semantics and preliminaries on equational logic in Section 2. There we also show that the interrupt operator is not definable in BPA modulo bisimilarity. The general structure of the proof of our main result, to the effect that bisimilarity is not finitely based over the language BPA with the interrupt operator, is presented in Section 3. In that section, we also show how to reduce the proof of our main result to that of a technical statement describing a key property of closed instantiations of sound equations that is preserved under equational derivations (Proposition 13). We offer a proof of Proposition 13 in Section 4. We conclude the paper by presenting in Section 5 an axiomatization of bisimulation equivalence over closed terms in the language obtained by enriching BPA with the disrupt operator from [7]. Such an axiomatization is finite in the presence of a finite set of actions, and does not employ auxiliary operators.

An extended abstract of this paper appeared as [6]. There we announced without proof our main result (namely, Theorem 9) under the assumption that the set of actions contains two distinct actions. The present version of the paper sharpens Theorem 9 in that it now applies to any non-empty set of actions, and offers the full proof of our main result (all of the material in Section 4). Moreover, Proposition 20 in the current paper is new.

2 Preliminaries

We begin by introducing the basic definitions and results on which the technical developments to follow are based. The interested reader is referred to [7,12] for more information.

2.1 The Language BPA_{int}

We assume a non-empty alphabet A of atomic actions, with typical element a. The language for processes we shall consider in the main body of this paper, henceforth referred to as BPA_{int}, is obtained by adding the interrupt operator from [7] to Bergstra and Klop’s BPA [12]. This language is given by the following grammar:

t ::= x | a | t · t | t + t | t ⊳ t ,

where x is a variable drawn from a countably infinite set V and a is an action. In the above grammar, we use the symbol ⊳ for the interrupt operator.

Intuitively, a term of the form p ⊳ q describes a process that normally behaves like p. However, at each point of the computation before p terminates, q can interrupt it, and begin its execution. If this happens, p resumes its computation upon termination of q. An alternative composition p+q nondeterministically behaves as either p or q. A sequential composition p·q first behaves as p, and upon termination of p behaves as q.

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 symbols in it. Formally,

• the size of variables and actions is 1, and

• that of t · u, t + u and t ⊳ u is one plus the sum of the sizes of t and u.

A process term is closed if it does not contain any variables. Closed terms will be typically denoted by p, q, r, s. As usual, we shall often write tu in lieu of t · u, and we assume that · binds stronger than + and ⊳.

A (closed) substitution is a mapping from process variables to (closed) BPA_{int} terms. For every term t and substitution σ, the term obtained by replacing every occurrence of a variable x in t with the term σ(x) will be written σ(t). Note that σ(t) is closed, if so is σ. In what follows, we shall use the notation σ[x ↦ p], where σ is a closed substitution and p is a closed BPA_{int} term, to stand for the substitution mapping x to p, and acting like σ on all of the other variables in V.

In the remainder of this paper, we let a^{1} denote a, and a^{m+1} denote a(a^{m}). Moreover, we consider terms 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 + is associative and commutative with respect to the notion of equivalence we shall consider over BPA_{int}. (See axioms A1, A2 in Table 3 on page 12.) In what follows, the symbol = will denote equality modulo associativity and commutativity of +.

We say that a term t has + as head operator if t = t_{1} + t_{2} for some terms t_{1} and t_{2}. For example, a + b has + as head operator, but (a + b)a does not.

For k ≥ 1, we use a summation ∑_{i∈{1,...,k}} t_{i} to denote t_{1} + ⋯ + t_{k}. It is easy to see that every BPA_{int} term t has the form ∑_{i∈I} t_{i}, for some finite, non-empty index set I, and terms t_{i} (i ∈ I) that do not have + as head operator. The terms t_{i} (i ∈ I) will be referred to as the (syntactic) summands of t. For example, the term (a + b)a has only itself as (syntactic) summand.

The operational semantics for the language BPA_{int} is given by the labelled transition

\overline{a →^{a}✓}

\frac{t →^{a}✓}{t + u →^{a}✓}  \frac{u →^{a}✓}{t + u →^{a}✓}  \frac{t →^{a} t′}{t + u →^{a} t′}  \frac{u →^{a} u′}{t + u →^{a} u′}

\frac{t →^{a}✓}{t · u →^{a} u}  \frac{t →^{a} t′}{t · u →^{a} t′ · u}

\frac{t →^{a}✓}{t ⊳ u →^{a}✓}  \frac{t →^{a} t′}{t ⊳ u →^{a} t′ ⊳ u}  \frac{u →^{a}✓}{t ⊳ u →^{a} t}  \frac{u →^{a} u′}{t ⊳ u →^{a} u′ · t}

Table 1 Transition Rules for BPA_{int}

system

(BPA_{int}, {→^{a}| a ∈ A}, {→^{a}✓ | a ∈ A}) ,

where the transition relations →^{a} and the unary predicates →^{a}✓ are, respectively, the least subsets of BPA_{int}×BPA_{int} and BPA_{int} satisfying the rules in Table 1. Intuitively, a transition t →^{a} u means that the system represented by the term t can perform the action a, thereby evolving into u. The special symbol ✓ stands for (successful) termination; therefore the interpretation of the statement t →^{a}✓ is that the process term t can terminate by performing a. Note that, for every closed term p, there is some action a for which either p →^{a} p′ holds for some p′, or p →^{a}✓ does.

For terms t, u, and action a, we say that u is an a-derivative of t if t →^{a} u.

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

Definition 1 For a sequence of actions a_{1} ⋯ a_{k} (k ≥ 0), and BPA_{int} terms t, t′, we write t →^{a_{1}···a_{k}} t′ iff there exists a sequence of transitions

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

Similarly, we say that a_{1} ⋯ a_{k} (k ≥ 1) is a termination trace of a BPA_{int} term t iff there exists a term t′ such that

t ⟶^{a_{1}···a_{k−1}} t′ →^{a_{k}}✓ .

If t ⟶^{a_{1}···a_{k}} t′ holds for some BPA_{int} term t′, or a_{1} ⋯ a_{k} is a termination trace of t, then a_{1} ⋯ a_{k} is a trace of t.

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

The norm of a term t, denoted by norm(t), is the length of its shortest termination trace; this notion stems from [9].

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

depth(a) = 1
depth(p + q) = max{depth(p), depth(q)}
depth(pq) = depth(p) + depth(q)
depth(p ⊳ q) = depth(p) + depth(q)
norm(a) = 1
norm(p + q) = min{norm(p), norm(q)}
norm(pq) = norm(p) + norm(q)
norm(p ⊳ q) = norm(p) .

Note that the depth and the norm of each closed BPA_{int} term are positive, and therefore that the norm of each closed term of the form pq is at least 2. This simple, but useful, observation will be used repeatedly in the remainder of this study.

In what follows, we shall sometimes need to consider the possible origins of a transition of the form σ(t) →^{a} p, for some action a, closed substitution σ, BPA_{int} term t and closed term p. Naturally enough, we expect that σ(t) affords that transition if t →^{a} 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. Similarly, we shall sometimes need to consider the possible origins of a transition of the form σ(t) →^{a}✓, for some action a, closed substitution σ and BPA_{int} term t.

To fully describe these situations, we introduce the auxiliary notion of configuration of a BPA_{int} 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, but has not yet terminated.

Definition 2 The collection of BPA_{int} configurations is given by the grammar:

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

where t is a BPA_{int} term, and x_{d} ∈ V_{d}.

\overline{x →^{x_{s}} x_{d}}  \overline{x →^{x}✓}

\frac{t →^{x} t′}{t + u →^{x} t′}  \frac{t →^{x_{s}} c}{t + u →^{x_{s}} c}  \frac{t →^{x}✓}{t + u →^{x}✓}

\frac{u →^{x} u′}{t + u →^{x} u′}  \frac{u →^{x_{s}} c}{t + u →^{x_{s}} c}  \frac{u →^{x}✓}{t + u →^{x}✓}

\frac{t →^{x} t′}{tu →^{x} t′u}  \frac{t →^{x_{s}} c}{tu →^{x_{s}} cu}  \frac{t →^{x}✓}{tu →^{x} u}

\frac{t →^{x} t′}{t ⊳ u →^{x} t′ ⊳ u}  \frac{t →^{x_{s}} c}{t ⊳ u →^{x_{s}} c ⊳ u}  \frac{t →^{x}✓}{t ⊳ u →^{x}✓}

\frac{u →^{x} u′}{t ⊳ u →^{x} u′t}  \frac{u →^{x_{s}} c}{t ⊳ u →^{x_{s}} ct}  \frac{u →^{x}✓}{t ⊳ u →^{x} t}

Table 2 SOS Rules for the Auxiliary Transitions →^{x}, →^{x_{s}} and →^{x}✓ (x ∈ V)

For example, the configuration x_{d} · (a ⊳ 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 (and has not terminated), but the one on the right-hand side has not. Note that each configuration contains at most one occurrence of an x_{d} ∈ V_{d}.

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 BPA_{int} term, to stand for the substitution mapping x_{d} to p, and acting like σ on all of the other variables.

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 three auxiliary transition relations whose elements have the following forms:

• t →^{x_{s}} c (read “t can start executing x and become c in doing so”), where t is a term, x is a variable, and c is a configuration,

• t →^{x} t′, where t and t′ are terms and x is a variable, or

• t →^{x}✓, where t is a term.

The first of these types of transitions will be used to account for those transitions of the form σ(t) →^{a} p that are due to a-labelled transitions of the closed term σ(x) that do not lead to its termination. The second will describe the origin of transitions of the form σ(t) →^{a} σ(t′) that are due to a-labelled transitions of the closed term σ(x) that lead to its termination. Finally, transitions of the third kind will allow us to describe the origin of termination transitions of the form σ(t) →^{a}✓ that are due to a-labelled termination transitions of the closed term σ(x).

The SOS rules defining these transition relations are given in Table 2. In those rules, the meta-variables t, u, t′ and u′ denote BPA_{int} terms, and c ranges over the collection of configurations that contain one occurrence of a symbol of the form x_{d}. The attentive reader might have already noticed that the left-hand sides of the rules in Table 2 are always BPA_{int} terms, and therefore that no transitions are possible from configurations that contain one occurrence of a symbol of the form x_{d}. This is in line with our aim in defining the auxiliary transition relations →^{x}, →^{x_{s}} and →^{x}✓ (x ∈ V), viz. to describe the possible origins of the initial transitions of a term of the form σ(t), with t a BPA_{int} term and σ a closed substitution.

Lemma 3 For each BPA_{int} term t, configuration c and variable x, if t →^{x_{s}} c, then x_{d} occurs in c. Moreover, if c = x_{d} then x is a summand of t.

The precise connection between the transitions of a term σ(t) and those of t is expressed by the following lemma.

Lemma 4 (Operational Correspondence) Assume that t is a BPA_{int} term, σ is a closed substitution and a is an action. Then the following statements hold:

(1) If t →^{a}✓, then σ(t) →^{a}✓.

(2) If t →^{a} t′, then σ(t) →^{a} σ(t′).

(3) If t →^{x}✓ and σ(x) →^{a}✓, then σ(t) →^{a}✓.

(4) If t →^{x} t′ and σ(x) →^{a}✓, then σ(t) →^{a} σ(t′).

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

(6) Assume that σ(t) →^{a}✓. Then either t →^{a}✓ or there is a variable x such that

t →^{x}✓ and σ(x) →^{a}✓.

(7) Assume that σ(t) →^{a} p, for some closed term p. Then one of the following possibilities applies:

• t →^{a} t′ for some term t′ such that p = σ(t′),

• t →^{x} t′, σ(x) →^{a}✓ and p = σ(t′), for some term t′ and variable x, or

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

PROOF. Statements 1–5 are proven by induction on the proof of the relevant transitions. The proof of statement 4 uses statement 3. On the other hand, statements 6– 7 are proven by induction on the structure of the term t. The proof of statement 7 uses statement 6.

The details are lengthy, but straightforward, and we therefore omit them. □

In this paper, we shall consider the language BPA_{int} modulo bisimulation equivalence [25,29].

Definition 5 Two closed BPA_{int} terms p and q are bisimilar, denoted by p \underline{↔} q, if there exists a symmetric binary relation B over closed BPA_{int} terms which relates p and q, such that:

- if r B s and r →^{a} r′, then there is a transition s →^{a} s′ such that r′ B s′;

- if r B s and r →^{a}✓, then s →^{a}✓.

Such a relation B will be called a bisimulation. The relation \underline{↔} will be referred to as bisimulation equivalence or bisimilarity.

It is well known that \underline{↔} is an equivalence relation, and that it is the largest bisimulation [25,29]. Moreover, the transition rules in Table 1 are in the ‘path’ format of Baeten and Verhoef [10]. Hence, bisimulation equivalence is a congruence with respect to all the operators in the signature of BPA_{int}.

Note that bisimilar closed BPA_{int} terms afford the same finite non-empty collection of (termination) traces, and therefore have the same norm and the same depth.

Bisimulation equivalence is extended to arbitrary BPA_{int} terms thus:

Definition 6 Let t, u be BPA_{int} terms. Then t \underline{↔} u iff σ(t) \underline{↔} σ(u) for every closed substitution σ.

For instance, we have that

x ⊳ y \underline{↔} (x ⊳ y) + yx

because, as our readers can easily check, the terms p ⊳ q and (p ⊳ q) + qp have the same set of initial “capabilities”, i.e.,

p ⊳ q →^{a} r iff (p ⊳ q) + qp →^{a} r , for each a and r, and

p ⊳ q →^{a}✓ iff (p ⊳ q) + qp →^{a}✓, for each a .

On the other hand, neither of the equivalences

(x + y) ⊳ z \underline{↔} (x ⊳ z) + (y ⊳ z) and
x ⊳ (y + z) \underline{↔} (x ⊳ y) + (x ⊳ z)

holds. Indeed, as our readers can easily check,

(a + a^{2}) ⊳ a \underline{↔} / (a ⊳ a) + (a^{2} ⊳ a) and
a^{2} ⊳ (a + a^{2}) \underline{↔} / (a^{2} ⊳ a) + (a^{2} ⊳ a^{2}) .

It is natural to expect that the interrupt operator cannot be defined in the language BPA modulo bisimulation equivalence. This expectation is confirmed by the following simple, but instructive, result:

Proposition 7 There is no BPA_{int} term t such that t does not contain occurrences of the interrupt operator, and t \underline{↔} x ⊳ y.

PROOF. Assume, towards a contradiction, that t is a BPA_{int} term such that t does not contain occurrences of the interrupt operator, and t \underline{↔} x ⊳ y.

Consider the closed substitution σ_{a} mapping each variable to a. Since

σ_{a}(t) \underline{↔} a ⊳ a and a ⊳ a →^{a}✓ ,

we have that σ_{a}(t) →^{a}✓. Lemma 4(6) yields that either t →^{a}✓ or there is a variable z such that t →^{z}✓ and σ_{a}(z) →^{a}✓. We shall now argue that both of these possibilities imply that t \underline{↔} / x ⊳ y, contradicting our assumption.

Indeed, using the former possibility and Lemma 4(1), we may infer that

σ_{a}[x ↦ a^{2}](t) →^{a}✓ .

This implies that t \underline{↔} / x ⊳ y, because a^{2} ⊳ a does not have termination traces of length 1.

Assume now that there is a variable z such that t →^{z}✓ and σ_{a}(z) →^{a}✓. It is not hard to see that t \underline{↔} z + u for some term u, since t does not contain occurrences of the interrupt operator and t →^{z}✓. We claim that

σ_{a}[x ↦ a^{2}](t) \underline{↔} / a^{2} ⊳ a .

If z ≠ x, our claim follows, because, reasoning as above,

σ_{a}[x ↦ a^{2}](t) \underline{↔} a + σ_{a}[x ↦ a^{2}](u) →^{a}✓

whereas a^{2} ⊳ a does not have termination traces of length 1.

If t \underline{↔} x + u, then σ_{a}[x ↦ a^{2}](t) →^{a} p for some p \underline{↔} a. On the other hand, the two a-derivatives of a^{2} ⊳ a, namely a ⊳ a and a^{2}, have depth 2, and thus neither of them is bisimilar to a. □

2.2 Equational Logic

An axiom system is a collection of equations t ≈ u over the language BPA_{int}. An equation t ≈ u is derivable from an axiom system E, notation E ⊢ t ≈ u, if it can

\begin{aligned}A1 & x + y & ≈ & y + x \\ A2 & (x + y) + z & ≈ & x + (y + z) \\ A3 & x + x & ≈ & x \\ A4 & (x + y)z & ≈ & (xz) + (yz) \\ A5 & (xy)z & ≈ & x(yz) \end{aligned}

Table 3 Some Axioms for BPA_{int}

be proven from the axioms in E using the rules of equational logic (viz. reflexivity, symmetry, transitivity, substitution and closure under BPA_{int} 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′}{t + t′ ≈ u + u′} \frac{t ≈ u t′ ≈ u′}{tt′ ≈ uu′} \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, the equation σ(t) ≈ σ(u) is called a substitution instance of an axiom in E.

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. In the remainder of this paper, we shall tacitly assume that our equational axiom systems are closed with respect to symmetry.

It is well-known (see, e.g., Sect. 2 in [21]) that if an equation relating two closed terms can be proven from an axiom system E, then there is a closed proof for it.

Definition 8 An equation t ≈ u over the language BPA_{int} 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.

A collection of equations over the language BPA that is sound and complete with respect to \underline{↔} is given in Table 3. Those equations stem from [12].

In [7], Baeten and Bergstra gave a sound and complete axiomatization of bisimilarity over BPA_{δ} (the extension of BPA with a constant δ to describe “deadlock”) enriched with the interrupt operator, using an auxiliary binary operator, which we denote by H . Intuitively, p H q behaves as p ⊳ q, with the restriction that it must take its first action from p. The axioms from [7] for the interrupt operator and its help operator are given below (except for one axiom that involves δ).

\begin{aligned}x ⊳ y & ≈ & (x H y) + (yx) \\ a H x & ≈ & a  (a ∈ A) \\ (ax) H y & ≈ & a(x ⊳ y)  (a ∈ A) \\ (x + y) H z & ≈ & (x H z) + (y H z) . \end{aligned}

Observe that, in the presence of a finite set of actions, this collection of equations is finite. Note, furthermore, that, unlike the interrupt operator, the auxiliary operator H is distributive with respect to + in its first argument. As we shall also remark in Section 5, this property is very useful for achieving a finite equational axiomatization of bisimilarity. Indeed, the absence of distributivity with respect to + casts doubts as to the possibility that a finite axiom system be powerful enough to “expand” the initial behaviour of terms of the form p ⊳ q when the number of non-bisimilar summands in p grows sufficiently large. This observation lies at the heart of the proof of our main result in this study (Theorem 9). This we now proceed to present.

3 Bisimilarity is not Finitely Based over BPA_{int}

Our main order of business in the remainder of this paper will be to show the following theorem:

Theorem 9 Bisimilarity is not finitely based over the language BPA_{int}—that is, there is no finite axiom system that is sound with respect to \underline{↔}, and proves all of the equations t ≈ u such that t \underline{↔} u. Moreover, the same holds true if we restrict ourselves to the collection of closed equations over BPA_{int} that hold modulo \underline{↔}.

The above theorem is an immediate corollary of the following result:

Theorem 10 Let E be a finite collection of equations over the language BPA_{int} that hold modulo \underline{↔}. Let n > 3 be larger than the size of each term in the equations in E. Then E ⊬ e_{n}, where the family of equations e_{n} (n ≥ 1) is defined thus:

e_{n} : Φ_{n} ⊳ a ≈ a + ∑_{i=2}^{n} a((a^{i−1} + a^{3} + a) ⊳ a) + aΦ_{n} .  (1)

In the above family, Φ_{n} = ∑_{i=1}^{n} p_{i} where p_{1} = a and p_{i} = a(a^{i−1} + a^{3} + a) for i > 1.

Note that the term ∑_{i=2}^{n} a((a^{i−1} + a^{3} + a) ⊳ a) is only present on the right-hand side of equation e_{n} if n > 1. Observe, furthermore, that, for each n ≥ 1, the closed equation e_{n} is sound modulo bisimilarity. Indeed, the left-hand and right-hand sides of the equation have isomorphic labelled transitions systems. Therefore, as claimed above, Theorem 9 is an immediate consequence of Theorem 10.

The following simple properties of the closed terms Φ_{n} for n ≥ 1 and p_{i} for 1 ≤ i ≤ n will find repeated application in what follows.

Lemma 11

(1) The norm of p_{i} is 1 if i = 1, and 2 otherwise. The depth of p_{i} is 1 if i = 1, and max{i, 4} otherwise.

(2) The norm of Φ_{n} ⊳ a is 1. Its depth is 2 if n = 1, 5 if n = 2 or n = 3, and n + 1 if n > 3.

(3) Each a-derivative of Φ_{n} or Φ_{n} ⊳ a has norm 1.

(4) Assume that 1 ≤ i < j. Then p_{i} \underline{↔} p_{j} if, and only if, i = 2 and j = 4. Therefore Φ_{n} has n − 1 non-bisimilar summands if n > 3.

PROOF. We limit ourselves to presenting the proof of the former claim in statement (4). The latter claim in that statement is an immediate consequence of the former.

If i = 2 and j = 4, then p_{i} \underline{↔} p_{j} follows immediately from the definition of the terms p_{ℓ} (ℓ ≥ 1). Conversely, assume that p_{i} \underline{↔} p_{j} and 1 ≤ i < j. Observe that i > 1 by statement (1) of the lemma. Since p_{i} \underline{↔} p_{j}, the terms p_{i} and p_{j} have the same set of terminating traces, namely

{a^{i}, a^{4}, a^{2}} = {a^{j}, a^{4}, a^{2}} .

Since i < j by the proviso of the statement, it follows that i, j ∈ {2, 4}. Again using i < j, we derive that i = 2 and j = 4, which was to be shown. □

In the remainder of this study, we shall offer a proof of Theorem 10. In order to prove this theorem, it will be sufficient to establish the following technical result:

Proposition 12 Let E be a finite axiom system over the language BPA_{int} that is sound modulo bisimilarity. Let n > 3 be larger than the size of each term in the equations in E. Assume, furthermore, that

• E ⊢ p ≈ q,

• p \underline{↔} Φ_{n} ⊳ a, and

• p has a summand bisimilar to Φ_{n} ⊳ a.

Then q has a summand bisimilar to Φ_{n} ⊳ a.

Indeed, assuming Proposition 12, we can prove Theorem 10, and therefore Theorem 9, as follows.

Proof of Theorem 10: Assume that E is a finite axiom system over the language BPA_{int} that is sound modulo bisimilarity. Pick n > 3 and larger than the size of the terms in the equations in E. Assume that, for some closed term q,

E ⊢ Φ_{n} ⊳ a ≈ q .

By Proposition 12, we have that q has a summand bisimilar to Φ_{n} ⊳ a. Using Lemma 11(2) it is easy to see that the summands of the right-hand side of equation e_{n}, viz.

a + ∑_{i=2}^{n} a((a^{i−1} + a^{3} + a) ⊳ a) + aΦ_{n} ,

are not bisimilar to Φ_{n} ⊳ a, and thus that

q ≠ a + ∑_{i=2}^{n} a((a^{i−1} + a^{3} + a) ⊳ a) + aΦ_{n} .

We may therefore conclude that E does not prove equation e_{n}, which was to be shown. □

Our order of business will now be to provide a proof of Proposition 12. Our proof of that result will be proof-theoretic in nature, and will proceed by induction on the depth of equational derivations from a finite axiom system E. The crux in such an induction proof is given by the following proposition, to the effect that the statement of Proposition 12 holds for closed instantiations of axioms in E.

Proposition 13 Let t ≈ u be an equation over the language BPA_{int} that holds modulo bisimilarity. Let σ be a closed substitution, p = σ(t) and q = σ(u). Assume that

• n > 3 and the size of t is smaller than n,

• p \underline{↔} Φ_{n} ⊳ a, and

• p has a summand bisimilar to Φ_{n} ⊳ a.

Then q has a summand bisimilar to Φ_{n} ⊳ a.

Indeed, let us assume for the moment that the above result holds. Using it, we can prove Proposition 12 thus:

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

(1) E ⊢ p ≈ q, (2) p \underline{↔} Φ_{n} ⊳ a, and

(3) p has a summand bisimilar to Φ_{n} ⊳ a.

We prove that q also has a summand bisimilar to Φ_{n} ⊳ a 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 applications of symmetry happen first in equational proofs (that is, E is closed with respect to symmetry).

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 substitution σ. Since n > 3 is larger than the size of each term mentioned in equations in E, the claim follows by Proposition 13.

• 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 Φ_{n} ⊳ a, we have that so does either p′ or p′′. Assume, without loss of generality, that p′ has a summand bisimilar to Φ_{n} ⊳ a. Since p is bisimilar to Φ_{n} ⊳ a, so is p′. The inductive hypothesis now yields that q′ has a summand bisimilar to Φ_{n} ⊳ a. Hence, q has a summand bisimilar to Φ_{n} ⊳ a, 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′′. This case is vacuous. In fact, norm(p) = 1 by our assumption that p \underline{↔} Φ_{n} ⊳ a, whereas the norm of a closed term of the form p′p′′ is at least 2.

• 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′′. The claim is immediate because p and q are their only summands, and E is sound modulo bisimilarity.

This completes the proof. □

In light of our previous discussion, all that we are left to do to complete our proof of Theorem 9 is to show Proposition 13. The next section of this paper will be entirely devoted to a proof of that result.

4 Proof of Proposition 13

We begin our proof of Proposition 13 by stating a few auxiliary results that will find application in the technical developments to follow.

Lemma 14 For n > 1, 2 ≤ j ≤ n and closed BPA_{int} term q, the term Φ_{n} ⊳ a is not bisimilar to closed terms that have a summand ((a^{j−1} + a^{3} + a) ⊳ a) ⊳ q.

PROOF. Observe that ((a^{j−1} + a^{3} + a) ⊳ a) ⊳ q →^{a} (a^{2} ⊳ a) ⊳ q. The claim now follows immediately by Lemma 11(3). □

Lemma 15 Let n ≥ 1. Assume that p ⊳ q \underline{↔} Φ_{n} ⊳ a, for closed BPA_{int} terms p and q. Then p \underline{↔} Φ_{n} and q \underline{↔} a.

PROOF. Since p ⊳ q \underline{↔} Φ_{n} ⊳ a and Φ_{n} ⊳ a →^{a} Φ_{n}, there is a closed term r such

that p ⊳ q →^{a} r and r \underline{↔} Φ_{n}.

We proceed by examining the possible origins of the transition p ⊳ q →^{a} r. There are three possibilities to consider, viz.

(1) q →^{a} q′ and r = q′p, for some q′,

(2) q →^{a}✓ and r = p, or

(3) p →^{a} p′ and r = p′ ⊳ q, for some p′.

The first case is impossible because the norm of r = q′p is at least 2, whereas the norm of Φ_{n} is 1. This contradicts r \underline{↔} Φ_{n}.

In the second case, we have that p \underline{↔} Φ_{n}. Therefore, as \underline{↔} is a congruence,

p ⊳ q \underline{↔} Φ_{n} ⊳ q \underline{↔} Φ_{n} ⊳ a .

We claim that q \underline{↔} a, which was to be shown. In fact, observe that the depth of q is 1. Moreover, q can only perform action a, or else the terms Φ_{n} ⊳ q and Φ_{n} ⊳ a would not afford the same traces. It follows that q \underline{↔} a as claimed.

Finally, assume that the third case applies. Observe, first of all, that, since

p′ ⊳ q \underline{↔} Φ_{n} ,

a is the only action q can perform. We claim that q \underline{↔} a. To see that this claim holds, assume that q →^{a} q′ for some q′. Then

p′ ⊳ q →^{a} q′p′ and norm(q′p′) ≥ 2 .

On the other hand, each a-derivative of the term Φ_{n} has norm 1 (Lemma 11(3)). This contradicts

p′ ⊳ q \underline{↔} Φ_{n} .

Thus q \underline{↔} a and, using congruence of \underline{↔} and the assumption of the statement of the lemma,

p ⊳ a \underline{↔} Φ_{n} ⊳ a .  (2)

If n = 1, then we can immediately conclude that p \underline{↔} a = p_{1}, and we are done. Assume therefore that n ≥ 2. Since p ⊳ a →^{a} p, we may infer from (2) that

• either p \underline{↔} Φ_{n} • or p \underline{↔} (a^{j−1} + a^{3} + a) ⊳ a for some j ∈ \{2, …, n\}.

In the former case, we are done. To complete our argument, we now show that the latter case leads to a contradiction. To this end, assume that

p \underline{↔} (a^{j−1} + a^{3} + a) ⊳ a .

Using congruence of \underline{↔} and (2), we may derive that

((a^{j−1} + a^{3} + a) ⊳ a) ⊳ a \underline{↔} Φ_{n} ⊳ a .

This contradicts Lemma 14.

The proof of the lemma is now complete. □

The following observation will find a key application in the subsequent technical developments.

Lemma 16 Let t be a BPA_{int} term that does not have + as head operator. Assume that σ is a closed substitution, and that

σ(t) \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}} ,

for some m > 2 and 1 ≤ 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 = a. This case is vacuous because, since m > 2 and 1 ≤ i_{1} < i_{m}, the depth of p_{i_{1}} + ⋯ + p_{i_{m}} is greater than 1.

(2) Case t = t′t′′ for some terms t′, t′′. Then

σ(t) = σ(t′)σ(t′′) \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}} .

Observe, first of all, that i_{1} > 1 and σ(t′) \underline{↔} a, for otherwise either p_{i_{1}} + ⋯ + p_{i_{m}} would have norm 1 or σ(t′)σ(t′′) would have an a-derivative whose norm is at least 2, contradicting the above equivalence.

Using congruence of \underline{↔},

aσ(t′′) \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}} .

It follows that p_{i_{2}} \underline{↔} p_{i_{m}}. As 2 ≤ i_{1} < i_{2} < i_{m} (for m > 2 by the assumption of the lemma), this contradicts Lemma 11(4).

(3) Case t = t′ ⊳ t′′ for some terms t′, t′′. Then

σ(t) = σ(t′) ⊳ σ(t′′) \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}} .

Observe, first of all, that σ(t′′) \underline{↔} a, for otherwise σ(t′) ⊳ σ(t′′) would have an a-derivative whose norm is at least 2, contradicting the above equivalence.

Using congruence of \underline{↔},

σ(t′) ⊳ a \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}} .

It follows that, for some j ∈ {1, …, m},

σ(t′) \underline{↔} (a^{i_{j}−1} + a^{3} + a) .

Again using congruence of \underline{↔}, we may now infer that

(a^{i_{j}−1} + a^{3} + a) ⊳ a \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}} .

This is a contradiction because

(a^{i_{j}−1} + a^{3} + a) ⊳ a →^{a} a^{2} ⊳ a and norm(a^{2} ⊳ a) = 2 ,

whereas each a-derivative of p_{i_{1}} + ⋯ + p_{i_{m}} has norm 1.

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

Remark 17 The proviso that m be larger than 2 in the statement of the above result is necessary. In fact, if m = 2, i_{1} = 2 and i_{2} = 4 then

p_{2} + p_{4} \underline{↔} a(a^{3} + a) .

It follows that σ(ax) \underline{↔} p_{2} + p_{4} if σ(x) = a^{3} + a.

The following observations will be used repeatedly in the proof of Proposition 13.

Lemma 18 Let t be a BPA_{int} term, x be a variable, and σ be a closed substitution. Assume that x ∈ var(t). Then the following statements hold:

(1) depth(σ(t)) ≥ depth(σ(x)), and

(2) if depth(σ(t)) = depth(σ(x)), then either t \underline{↔} x or t \underline{↔} x+u for some BPA_{int} term u that does not contain occurrences of x.

PROOF. Both statements are shown by induction on the structure of t. Here we limit ourselves to presenting a proof for statement 2. The case t = x is trivial, and those where t = t_{1}t_{2} or t = t_{1} ⊳ t_{2}, for some terms t_{1}, t_{2} are vacuous, because depth(σ(t)) is larger than depth(σ(x)) for terms t of those forms. We are thus left to examine the case t = t_{1} + t_{2} for some terms t_{1}, t_{2}.

Since x ∈ var(t), either x ∈ var(t_{1}) ∩ var(t_{2}) or x occurs in exactly one of t_{1} and t_{2}. We examine these two possibilities in turn.

Assume that x ∈ var(t_{1}) ∩ var(t_{2}). We claim that, for i ∈ {1, 2},

depth(σ(x)) = depth(σ(t_{i})) .

Indeed, by statement 1 of the lemma, we have that depth(σ(x)) ≤ depth(σ(t_{i})) for i ∈ {1, 2}. Moreover, for i ∈ {1, 2},

depth(σ(t_{i})) ≤ max{depth(σ(t_{1})), depth(σ(t_{2}))}
= depth(σ(t_{1} + t_{2})) = depth(σ(x)) .

Therefore, by the induction hypothesis, for i ∈ {1, 2}, we may infer that either t_{i} \underline{↔} x or t_{i} \underline{↔} x + u_{i} for some BPA_{int} term u_{i} that does not contain occurrences of x.

If both t_{1} \underline{↔} x and t_{2} \underline{↔} x, then t_{1} + t_{2} \underline{↔} x. Otherwise, t = t_{1} + t_{2} \underline{↔} x + u for some BPA_{int} term u that does not contain occurrences of x.

Assume now, without loss of generality, that x ∈ var(t_{1}) and x ∉ var(t_{2}). Reasoning as above, we may apply the inductive hypothesis to t_{1} to obtain that either t_{1} \underline{↔} x or t_{1} \underline{↔} x + u_{1} for some BPA_{int} term u_{1} that does not contain occurrences of x. In both cases, it follows that t = t_{1} + t_{2} \underline{↔} x + u for some BPA_{int} term u that does not contain occurrences of x. □

Lemma 19 Let t ≈ u be an equation over the language BPA_{int} that is sound with respect to bisimulation equivalence. 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 set I, we can write

t = ∑_{i∈I} t_{i} ,

where none of the t_{i} (i ∈ I) has + as head operator. Assume that variable x occurs as a summand in t—i.e., there is an i ∈ I with t_{i} = x. We shall argue that x also occurs as a summand in u.

Consider the substitution σ_{a} mapping each variable to a. As t ≈ u is sound with respect to bisimulation equivalence,

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

Pick an integer m larger than the depth of σ_{a}(t) and of σ_{a}(u). Let σ be the substitution mapping x to the term a^{m+1} and agreeing with σ_{a} 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}, because t_{i} = x and σ(x) = a^{m+1} →^{a} a^{m}. Hence, for some closed term p,

σ(u) →^{a} p \underline{↔} a^{m} .

By Lemma 4(7) and the definition of σ, one of the following holds:

• u →^{y} u′, σ(y) →^{a}✓ and p = σ(u′), for some term u′ and variable y ≠ x,

• u →^{a} u′ for some u′ such that p = σ(u′), or

• u →^{x_{s}} c for some configuration c such that σ[x_{d} ↦ a^{m}](c) = p.

In the first two cases, we can conclude that either depth(p) ≥ m+1 if x ∈ var(u′), or depth(p) < m otherwise. This contradicts p \underline{↔} a^{m}. In the third case, we claim that c = x_{d} and that x is a summand of u. In fact, x_{d} occurs in c (Lemma 3). Moreover, if c ≠ x_{d} then it is easy to see that depth(σ[x_{d} ↦ q](c)) > m, again contradicting p \underline{↔} a^{m}. Hence c = x_{d} as claimed. Since, u →^{x_{s}} c = x_{d}, it follows that x is a summand of u (Lemma 3), which was to be shown. □

We are finally in a position to conclude our technical developments by offering a proof of Proposition 13.

Proof of Proposition 13: Recall that, by the proviso of the proposition,

(1) t ≈ u is an equation over the language BPA_{int} that holds modulo bisimilarity,

(2) n > 3 and the size of t is smaller than n,

(3) σ is a closed substitution, p = σ(t) and q = σ(u),

(4) p \underline{↔} Φ_{n} ⊳ a, and

(5) p has a summand bisimilar to Φ_{n} ⊳ a.

We shall prove that q also has a summand bisimilar to Φ_{n} ⊳ a.

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

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

where none of the t_{i} (i ∈ I) and u_{j} (j ∈ J) has + as its head operator.

Since p = σ(t) has a summand bisimilar to Φ_{n} ⊳ a, so does σ(t_{i}) for some index i ∈ I. Our aim is now to show that there is an index j ∈ J such that σ(u_{j}) has a summand bisimilar to Φ_{n} ⊳ a. 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, σ(x) has a summand bisimilar to Φ_{n} ⊳ a, and t has x as a summand. As t ≈ u is sound with respect to bisimulation equivalence, it follows that u also has x as a summand (Lemma 19). Thus there is an index j ∈ J such that u_{j} = x, and, modulo bisimulation, σ(u) has Φ_{n} ⊳ a as a summand, which was to be shown.

(2) Case t_{i} = t′t′′ for some terms t′, t′′. This case is vacuous. Indeed, note, first of all, that σ(t_{i}) = σ(t′)σ(t′′) is its only summand. Therefore,

σ(t_{i}) = σ(t′)σ(t′′) \underline{↔} Φ_{n} ⊳ a .

This is a contradiction because

norm(Φ_{n} ⊳ a) = 1 < 2 ≤ norm(σ(t′)σ(t′′)) = norm(σ(t_{i})) .

(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′′) is its only summand, we have that

σ(t_{i}) = σ(t′) ⊳ σ(t′′) \underline{↔} Φ_{n} ⊳ a .

By Lemma 15, this yields that

σ(t′) \underline{↔} Φ_{n} and  (5)
σ(t′′) \underline{↔} a .  (6)

Now, t′ can be written thus:

t′ = w_{1} + ⋯ + w_{k} (k ≥ 1) ,

where none of the summands w_{h} has + as head operator. Observe that, since n is larger than the size of t, we have that 2k < n − 1. Indeed, the size of

t_{i} = t′ ⊳ t′′ = (w_{1} + ⋯ + w_{k}) ⊳ t′′

is at least 2k + 1 and n is larger than the size of t, and therefore of t_{i}. Hence, since Φ_{n} has n − 1 inequivalent summands (Lemma 11(4)) and

σ(t′) \underline{↔} Φ_{n} ,

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

σ(w_{h}) \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}}

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

σ(x) \underline{↔} p_{i_{1}} + ⋯ + p_{i_{m}} .  (7)

Note that, as x is a summand of t′,

t′ = x + t′′′ , for some term t′′′ .

Moreover, we have that x ∉ var(t′′), or else σ(t′′) \underline{↔} / a, contradicting (6).

Our order of business will now be to use the information collected so far in this case of the proof to argue that the term σ(u) has a summand that is bisimilar to Φ_{n} ⊳ a. To this end, consider the substitution

σ′ = σ[x ↦ a(Φ_{n} ⊳ a)] .

We have that

σ′(t_{i}) = σ′(t′) ⊳ σ′(t′′)
= (σ′(x) + σ′(t′′′)) ⊳ σ′(t′′) (As t′ = x + t′′′)
= (σ′(x) + σ′(t′′′)) ⊳ σ(t′′) (As x ∉ var(t′′))
\underline{↔} (a(Φ_{n} ⊳ a) + σ′(t′′′)) ⊳ a (As σ(t′′) \underline{↔} a) .

Thus, for some p′,

σ′(t_{i}) →^{a} p′ \underline{↔} (Φ_{n} ⊳ a) ⊳ a .

By (3), σ′(t) →^{a} p′ also holds. Since t ≈ u is sound with respect to \underline{↔} , it follows that σ′(t) \underline{↔} σ′(u). Hence, by (4), there exist an index j ∈ J and a q′ such that

σ′(u_{j}) →^{a} q′ \underline{↔} (Φ_{n} ⊳ a) ⊳ a .  (8)

Recall that, by one of the assumptions of the proposition,

σ(u) \underline{↔} Φ_{n} ⊳ a ,

and thus σ(u) has depth n + 1 because n > 3 (Lemma 11(2)). On the other hand, by (8),

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}) .  (9)

We shall now argue that σ(u_{j}) \underline{↔} Φ_{n} ⊳ a by a further case analysis on the form a term u_{j} satisfying (8) and (9) may have.

(a) Case u_{j} = x. This case is vacuous because

σ′(u_{j}) = σ′(x) = a(Φ_{n} ⊳ a) →^{a} Φ_{n} ⊳ a

is the only initial transition afforded by σ′(u_{j}). Clearly this contradicts (8).

(b) Case u_{j} = u′u′′ for some terms u′, u′′. We show that this case also

leads to a contradiction.

Recall that

σ′(u_{j}) = σ′(u′)σ′(u′′) →^{a} q′ \underline{↔} (Φ_{n} ⊳ a) ⊳ a .

We proceed by a case analysis on the possible origin of this transition. There are two possibilities, viz.

(i) σ′(u′) →^{a} r and q′ = rσ′(u′′), for some r, or

(ii) σ′(u′) →^{a}✓ and q′ = σ′(u′′).

The former case is vacuous because norm(q′) = 1 but norm(rσ′(u′′)) ≥ 2.

In the latter case, we claim that x ∈ var(u′′). In fact, if x ∉ var(u′′), then we obtain a contradiction thus:

n + 2 = depth(σ′(u′′)) (By (8))
= depth(σ(u′′)) (As x ∉ var(u′′))
< depth(σ(u_{j})) (As u_{j} = u′u′′)
≤ depth(σ(u))
= n + 1 (As σ(u) \underline{↔} Φ_{n} ⊳ a and n > 3) .

Thus x ∈ var(u′′), as claimed. Moreover,

depth(σ′(u′′)) = depth(q′) = n + 2 = depth(σ′(x)) .

Observe now that u′′ \underline{↔} / x. Indeed, if u′′ were bisimilar to x, then we could infer that

q′ = σ′(u′′) \underline{↔} σ′(x) = a(Φ_{n} ⊳ a) .

This contradicts (8) because norm(q′) = 1, whereas norm(σ′(x)) = 2. Lemma 18(2) thus yields that

u′′ \underline{↔} x + u′′′ ,

for some u′′′ that does not contain x. Hence,

q′ = σ′(u′′)
\underline{↔} σ′(x) + σ′(u′′′)
= a(Φ_{n} ⊳ a) + σ(u′′′) (As x ∉ var(u′′′))
\underline{↔} (Φ_{n} ⊳ a) ⊳ a (By (8)) .

Since the transition

(Φ_{n} ⊳ a) ⊳ a →^{a} ((a^{n−1} + a^{3} + a) ⊳ a) ⊳ a

can only be matched by a transition of the form

σ(u′′′) →^{a} r \underline{↔} ((a^{n−1} + a^{3} + a) ⊳ a) ⊳ a ,

for some r (Lemma 14), and n > 3 by one of the assumptions of the proposition, we may infer that

depth(σ(u′′′)) > n + 1 .

We can finally derive a contradiction as follows:

n + 1 = depth(q)
= depth(σ(u))
≥ depth(σ(u_{j}))
= depth(σ(u′)) + depth(σ(u′′))
= depth(σ(u′)) + depth(σ(x) + σ(u′′′))
> n + 1 .

This completes the proof for the case u_{j} = u′u′′.

(c) Case u_{j} = u′ ⊳ u′′ for some terms u′, u′′. This is the lengthiest subcase of case 3 of the proof, and its analysis will occupy us for the next few pages.

Recall that, by (8),

σ′(u_{j}) = σ′(u′) ⊳ σ′(u′′) →^{a} q′ \underline{↔} (Φ_{n} ⊳ a) ⊳ a .

We proceed by a case analysis on the possible origin of this transition. There are three possibilities, namely

(i) σ′(u′′) →^{a} q′′ and q′ = q′′σ′(u′), for some q′′,

(ii) σ′(u′) →^{a} q′′ and q′ = q′′ ⊳ σ′(u′′), for some q′′, or

(iii) σ′(u′′) →^{a}✓ and q′ = σ′(u′).

We examine these sub-cases in turn.

• Case 3c.i. This case is vacuous because, since by (8), norm(q′) = 1. On the other hand, the norm of q′′σ′(u′) is at least 2.

• Case 3c.ii. Note, first of all, that, since

q′ = q′′ ⊳ σ′(u′′) \underline{↔} (Φ_{n} ⊳ a) ⊳ a ,

we have that x ∉ var(u′′). In fact, if x ∈ var(u′′), then we would be able to infer that

depth(q′) = depth(q′′) + depth(σ′(u′′))
> depth(σ′(u′′))
≥ n + 2 (By Lemma 18(1)) ,

contradicting the above equivalence. Since x ∉ var(u′′) and x ∈ var(u_{j}) by (9), we may infer that

x ∈ var(u′) .  (10)

Recall that, by the assumptions for this sub-case, σ′(u′) →^{a} q′′. Using Lemma 4(7), one of the following possibilities arises:

(i) u′ →^{y} w, σ′(y) →^{a} ✓ and q′′ = σ′(w), for some term w and variable y,

(ii) u′ →^{a} w for some w such that q′′ = σ′(w), or (iii) u′ →^{y_{s}} c and σ′(y) →^{a} r, for some variable y, configuration c

and closed term r such that σ′[y_{d} ↦ r](c) = q′′. We consider these possibilities in turn.

The first of these cases is vacuous. In fact, using the assumptions for this case, we can derive a contradiction as follows. Note, first of all, that y ≠ x because σ′(y) →^{a}✓. Therefore

σ(y) = σ′(y) →^{a}✓ .

Hence, by Lemma 4(4), σ(u′) →^{a} σ(w). So

σ(u_{j}) = σ(u′) ⊳ σ(u′′) →^{a} σ(w) ⊳ σ(u′′) .

depth(σ(u_{j})) ≤ depth(σ(u)) = n + 1, so depth(σ(w) ⊳ σ(u′′)) ≤ n. This implies that x ∈ var(w). For else, by assumptions of this sub-case,

q′ = q′′ ⊳ σ′(u′′) = σ′(w) ⊳ σ′(u′′) = σ(w) ⊳ σ(u′′) .

Then q′ would have depth at most n, contradicting (8). But, as x ∈ var(w), Lemma 18(1) yields that

depth(q′) > depth(σ′(w)) ≥ depth(σ′(x)) = n + 2 ,

again contradicting (8).

The second case is also vacuous because, exactly as in the first case, we can show that depth(q′) is no larger than n if x ∉ var(w), and is larger than n + 2 otherwise. This contradicts (8).

We are therefore left to examine the third possibility. Note that x ∉ var(c), or else

depth(q′) > depth(q′′) ≥ n + 2 ,

contradicting (8). We claim that y = x. To see that this does hold, assume, towards a contradiction, that y ≠ x. Then, by the assumptions for this sub-case,

σ(y) = σ′(y) →^{a} r .

Lemma 4(5) and u′ →^{y_{s}} c now yield that

σ(u′) →^{a} σ[y_{d} ↦ r](c) = σ′[y_{d} ↦ r](c) = q′′ .

(The first equality holds because x ∉ var(c).) Hence, since x ∉ var(u′′),

σ(u_{j}) →^{a} q′′ ⊳ σ(u′′) = q′′ ⊳ σ′(u′′) = q′ .

As depth(σ(u_{j})) ≤ depth(σ(u)) = n+1, this implies that depth(q′) is no larger than n, contradicting (8). Hence y = x as claimed.

Since σ′(x) →^{a} r, it follows that r = Φ_{n} ⊳ a. By one of the assumptions for this sub-case, and since x ∉ var(u′′),

q′ = σ′[x_{d} ↦ r](c) ⊳ σ(u′′) .

Since depth(q′) = n + 2 by (8), x_{d} occurs in c (Lemma 3), and depth(r) = n + 1, this is only possible if

· c = x_{d} and · σ(u′′) \underline{↔} a.

(Indeed, by Definition 2, the only other possible forms of a configuration c containing x_{d} are c_{1} · w and c_{1} ⊳ w for some configuration c_{1} and BPA_{int} term w. In both of these cases,

depth(σ′[x_{d} ↦ r](c)) ≥ n + 2 = depth(q′) ,

contradicting q′ = σ′[x_{d} ↦ r](c) ⊳ σ(u′′).) We shall now argue that

σ(u_{j}) \underline{↔} Φ_{n} ⊳ a ,  (11)

proving that q = σ(u) has a summand bisimilar to Φ_{n} ⊳ a, which was to be shown. In fact,

σ(u_{j}) = σ(u′) ⊳ σ(u′′) \underline{↔} σ(u′) ⊳ a .

We shall now prove that σ(u′) \underline{↔} Φ_{n}. Indeed, since

σ(u_{j}) →^{a} σ(u′)

it follows that

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

Recall that σ(u) \underline{↔} Φ_{n} ⊳ a. Therefore, there is an a-derivative of Φ_{n} ⊳ a that is bisimilar to σ(u′). This a-derivative of Φ_{n} ⊳ a can only be Φ_{n}. In fact, the other a-derivatives of Φ_{n} ⊳ a have the form

(a^{j−1} + a^{3} + a) ⊳ a (j ∈ {2, …, n}) .

If one of those terms were bisimilar to σ(u′), then using our assumption that σ(u) \underline{↔} Φ_{n} ⊳ a, we could infer that, for some j ∈ {2, …, n},

Φ_{n} ⊳ a \underline{↔} Φ_{n} ⊳ a + ((a^{j−1} + a^{3} + a) ⊳ a) ⊳ a .

This contradicts Lemma 14.

Therefore, σ(u′) \underline{↔} Φ_{n}, as claimed. We may finally conclude that σ(u_{j}) \underline{↔} Φ_{n} ⊳ a.

The proof for case 3c.ii is now complete.

• Case 3c.iii. Since σ′(u′′) →^{a}✓, using Lemma 4(6) we may infer that

· u′′ →^{a}✓, or

· u′′ →^{y}✓ and σ′(y) →^{a}✓, for some variable y. In the latter case, as σ′(x) →^{a}✓ does not hold, y ≠ x, and so σ(y) = σ′(y) →^{a}✓. Using statements 1 and 3 of Lemma 4, we therefore in either case have that

σ(u′′) →^{a}✓ .

This yields that σ(u_{j}) = σ(u′) ⊳ σ(u′′) →^{a} σ(u′).

Now, reasoning exactly as in the previous case, we can argue that σ(u′) \underline{↔} Φ_{n}. Therefore, using congruence of \underline{↔},

σ(u_{j}) \underline{↔} Φ_{n} ⊳ σ(u′′) .

This equivalence yields that depth(σ(u_{j})) = depth(σ(u)) = n + 1, and that the depth of σ(u′′) is 1. It follows that σ(u′′) \underline{↔} a. Hence, σ(u) has a summand, namely σ(u_{j}), that is bisimilar to Φ_{n} ⊳ a.

This completes the proof of case 3c, and thus that of case 3.

Since we have examined all the possible forms that t_{i} can take, the proof of the proposition is now complete. □

5 BPA with the Disrupt Operator

As mentioned in Section 1, in their paper [7], Baeten and Bergstra have given a finite axiomatization of bisimilarity over BPA_{δ} (the extension of BPA with a constant δ to describe “deadlock”) enriched with two mode transfer operators, viz. the disrupt and interrupt operators, using auxiliary operators. The main result in this paper (Theorem 9) shows that the use of auxiliary operators is indeed necessary in order to obtain a finite axiomatization of bisimulation equivalence over the language BPA_{int}, and that this holds true even if we restrict ourselves to axiomatizing the collection of closed equations over this language.

A natural question to ask at this point is whether this negative result applies also to the language BPA_{dis} obtained by enriching BPA with the disrupt operator. Intuitively, “p disrupted by q”—which we shall write p ▶ q in what follows—describes a process that normally behaves like p. However, at each point of the computation before p terminates, q can begin its execution. If this happens, q takes over, and p never resumes its computation. This intuition is captured formally by the following transition rules:

\frac{t →^{a}✓}{t ▶ u →^{a}✓}  \frac{t →^{a} t′}{t ▶ u →^{a} t′ ▶ u}  \frac{u →^{a}✓}{t ▶ u →^{a}✓}  \frac{u →^{a} u′}{t ▶ u →^{a} u′}

As was the case for the interrupt operator (see Proposition 7), the disrupt operator cannot be defined in the language BPA modulo bisimulation equivalence.

Proposition 20 There is no BPA_{dis} term t such that t does not contain occurrences of the disrupt operator, and t \underline{↔} x ▶ y.

PROOF. Assume, towards a contradiction, that t is a BPA_{dis} term such that t does not contain occurrences of the disrupt operator, and t \underline{↔} x ▶ y.

Consider the closed substitution σ mapping variable x to a and each other variable to a^{2}. Since

σ(t) \underline{↔} a ▶ a^{2} and a ▶ a^{2} →^{a}✓ ,

we have that σ(t) →^{a}✓. Since σ(t) →^{a}✓ and t does not contain occurrences of the disrupt operator, it is not hard to see that, for some term u, either t \underline{↔} a + u or t \underline{↔} x + u. Both of these possibilities lead to a contradiction.

Indeed, using the former possibility, we may infer that

σ[x ↦ a^{2}](t) →^{a}✓ .

This implies that t \underline{↔} / x ▶ y, because a^{2} ▶ a^{2} does not have termination traces of length 1.

Assume now that t \underline{↔} x + u. We claim that

σ[x ↦ a^{2}, y ↦ a^{3}](t) \underline{↔} / a^{2} ▶ a^{3} .

This follows because σ[x ↦ a^{2}, y ↦ a^{3}](t) →^{a} p for some p \underline{↔} a, since t \underline{↔} x + u. On the other hand, the two a-derivatives of a^{2} ▶ a^{3}, namely a ▶ a^{3} and a^{2}, have depth at least 2, and thus neither of them is bisimilar to a. □

It is not hard to see that the following equations are sound modulo bisimilarity over the language BPA_{dis}:

\begin{aligned}(D1) & a ▶ x & ≈ & a + x \\ (D2) & ax ▶ y & ≈ & a(x ▶ y) + y and \\ (D3) & (x + y) ▶ z & ≈ & (x ▶ z) + (y ▶ z) . \end{aligned}

In the first two equations above, the symbol a ranges over the set of actions A. Those two identities are therefore equation schemas. Note, however, that such schemas have only finitely many instances if A is finite.

The last of the equations above is particularly important, at least as far as obtaining a finite equational axiomatization of bisimilarity over the collection of closed terms in the language BPA_{dis} is concerned. (The interested reader may have already noticed that its soundness modulo bisimulation equivalence depends crucially on the fact that transitions due to moves of the second argument of a disrupt discard the first argument.) Indeed, its repeated use in conjunction with the first two laws allows us to eliminate occurrences of the disrupt operator from closed terms. This effectively reduces the problem of finitely axiomatizing bisimilarity over the collection of closed terms in the language BPA_{dis} to that of offering a finite axiomatization of bisimilarity over closed BPA terms. As shown by Bergstra and Klop in [12], the five equations in Table 3 suffice to axiomatize bisimilarity over the language BPA.

In sharp contrast to Theorem 9, we therefore have that:

Theorem 21 The collection of closed equations over BPA_{dis} that hold modulo \underline{↔} is axiomatized by (A1)–(A5) in Table 3 together with (D1)–(D3), and is therefore finitely based if A is finite.

It follows that, in the presence of a finite action set, the use of auxiliary operators is not necessary in order to obtain a finite axiomatization of bisimulation equivalence over closed terms in the language BPA_{dis}.

The axiomatization of bisimilarity over closed terms in the language BPA_{dis} offered in the theorem above is not ω-complete. For example, the reader can easily check that the disrupt operator is associative modulo bisimilarity, i.e., that the equation

(x ▶ y) ▶ z ≈ x ▶ (y ▶ z)

holds modulo \underline{↔}. This equation is not provable using the equations mentioned in Theorem 21. However, we conjecture that, in the presence of a finite action set, bisimilarity also affords a finite ω-complete axiomatization over BPA_{dis}. Work on a proof of this conjecture is in progress.

References

[1] L. Aceto, Z. Ésik, A. Ingolfsdottir, On the two-variable fragment of the equational theory of the max-sum algebra of the natural numbers, in: H. Reichel, S. Tison (Eds.), Proceedings of the 17th International Symposium on Theoretical Aspects of Computer Science, STACS 2000 (Lille), Vol. 1770 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 267–278.

[2] L. Aceto, Z. Ésik, A. Ingolfsdottir, The max-plus algebra of the natural numbers has no finite equational basis, Theoretical Comput. Sci. 293 (1) (2003) 169–188.

[3] L. Aceto, W. Fokkink, R. van Glabbeek, A. Ingolfsdottir, Nested semantics over finite trees are equationally hard, Information and Computation 191 (2) (2004) 203–232.

[4] L. Aceto, W. Fokkink, A. Ingolfsdottir, A menagerie of non-finitely based process semantics over BPA*—from ready simulation to completed traces, Mathematical Structures in Computer Science 8 (3) (1998) 193–230.

[5] L. Aceto, W. Fokkink, A. Ingolfsdottir, B. Luttik, CCS with Hennessy’s merge has no finite equational axiomatization, Theoretical Comput. Sci. 330 (3) (2005) 377–405.

[6] L. Aceto, W. Fokkink, A. Ingolfsdottir, S. Nain, Bisimilarity is not finitely based over BPA with interrupt, in: J. L. Fiadeiro, N. Harman, M. Roggenbach, J. J. M. M. Rutten (Eds.), Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings, Vol. 3629 of Lecture Notes in Computer Science, Springer-Verlag, 2005, pp. 52–66.

[7] J.  Baeten,  J.  Bergstra,  Mode

transfer in process algebra, Report CSR 00–01, Technische Universiteit Eindhoven, this paper is an expanded and revised version of [11] (2000). Available from

http://alexandria.tue.nl/extra1/wskrap/publichtml/200010731.pdf  .

[8] J. Baeten, J. Bergstra, J. W. Klop, Syntax and defining equations for an interrupt mechanism in process algebra, Fundamenta Informaticae IX (2) (1986) 127–168.

[9] J. Baeten, J. Bergstra, J. W. Klop, Decidability of bisimulation equivalence for processes generating context-free languages, J. ACM 40 (3) (1993) 653–682.

[10] J. Baeten, C. Verhoef, A congruence theorem for structured operational semantics, in: E. Best (Ed.), Proceedings CONCUR 93, Hildesheim, Germany, Vol. 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 477–492.

[11] J. Bergstra, A mode transfer operator in process algebra, Report P8808, Programming Research Group, University of Amsterdam (1988).

[12] J. Bergstra, J. W. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam (1982).

[13] J. Bergstra, J. W. Klop, Process algebra for synchronous communication, Information and Control 60 (1/3) (1984) 109–137.

[14] S. Blom, W. Fokkink, S. Nain, On the axiomatizability of ready traces, ready simulation and failure traces, in: J. Baeten, J. K. Lenstra, J. Parrow, G. J. Woeginger (Eds.), Proceedings 30th Colloquium on Automata, Languages and Programming— ICALP’03, Eindhoven, Vol. 2719 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 109–118.

[15] E. Brinksma, A tutorial on LOTOS, in: M. Diaz (Ed.), Proceedings of the IFIP Workshop on Protocol Specification, Testing and Verification, North-Holland, 1986, pp. 73–84.

[16] J. H. Conway, Regular Algebra and Finite Machines, Mathematics Series (R. Brown and J. De Wet eds.), Chapman and Hall, London, United Kingdom, 1971.

[17] A. Dsouza, B. Bloom, On the expressive power of CCS, in: P. S. Thiagarajan (Ed.), Foundations of Software Technology and Theoretical Computer Science (Bangalore, 1995), Vol. 1026 of Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 309–323.

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

[19] W. Fokkink, S. Nain, On finite alphabets and infinite bases: From ready pairs to possible worlds, in: I. Walukiewicz (Ed.), Proceedings of Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Vol. 2897, Springer-Verlag, 2004, pp. 182–194.

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

[21] J. F. Groote, A new strategy for proving ω–completeness with applications in process algebra, in: J. Baeten, J. W. Klop (Eds.), Proceedings CONCUR 90, Amsterdam, Vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 314–331.

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

[23] ISO, Information processing systems – open systems interconnection – LOTOS – a formal description technique based on the temporal ordering of observational behaviour ISO/TC97/SC21/N DIS8807 (1987).

[24] S. Mauw, PSF – A Process Specification Formalism, Ph.D. thesis, University of Amsterdam (Dec. 1991).

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

[26] R. Milner, M. Tofte, R. Harper, D. MacQueen, The Definition of Standard ML (Revised), MIT Press, 1997.

[27] F. Moller, The importance of the left merge operator in process algebras, in: M. Paterson (Ed.), Proceedings 17^{th} ICALP, Warwick, Vol. 443 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 752–764.

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

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

[30] V. Redko, On defining relations for the algebra of regular events, Ukrainskii Matematicheskii Zhurnal 16 (1964) 120–126, in Russian.

[31] P. Sewell, Nonaxiomatisability of equivalences over finite state processes, Annals of Pure and Applied Logic 90 (1–3) (1997) 163–191.

Recent BRICS Report Series Publications

RS-05-33 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Sumit Nain. Bisimilarity is not Finitely Based over BPA with Interrupt. October 2005. 33 pp. This paper supersedes BRICS Report RS-04-24. An extended abstract of this paper appeared in Algebra and Coalgebra in Computer Science, 1st Conference, CALCO 2005, Swansea, Wales, 3–6 September 2005, Lecture Notes in Computer Science 3629, pp. 54–68, Springer-Verlag, 2005.

RS-05-32 Anders Møller, Mads Østerby Olesen, and Michael I. Schwartzbach. Static Validation of XSL Transformations. October 2005. 50 pp.

RS-05-31 Christian Kirkegaard and Anders Møller. Type Checking with XML Schema in Xact. September 2005. 20 pp.

RS-05-30 Karl Krukow. An Operational Semantics for Trust Policies. September 2005. 38 pp.

RS-05-29 Olivier Danvy and Henning Korsholm Rohde. On Obtaining the Boyer-Moore String-Matching Algorithm by Partial Evaluation. September 2005. ii+9 pp. To appear in Information Processing Letters. This version supersedes BRICS RS-05-14.

RS-05-28 Jiří Srba. On Counting the Number of Consistent Genotype Assignments for Pedigrees. September 2005. 15 pp. To appear in FSTTCS ’05.

RS-05-27 Pascal Zimmer. A Calculus for Context-Awareness. August 2005. 21 pp.

RS-05-26 Henning Korsholm Rohde. Measuring the Propagation of Information in Partial Evaluation. August 2005. 39 pp.

RS-05-25 Dariusz Biernacki and Olivier Danvy. A Simple Proof of a Folklore Theorem about Delimited Control. August 2005. ii+11 pp. To appear in Journal of Functional Programming. This version supersedes BRICS RS-05-10.

RS-05-24 Ma�gorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. August 2005. iv+43 pp. To appear in the journal Logical Methods in Computer Science. This version supersedes BRICS RS-05-11.