BRICS RS-95-28 Aceto & Groote: Equational Axiomatization for MPA with String Iteration

BRICS

Basic Research in Computer Science

A Complete Equational Axiomatization for MPA with String Iteration

Luca Aceto Jan Friso Groote

BRICS Report Series RS-95-28 ISSN 0909-0878 May 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, 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 publications in the BRICS Report Series. 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@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

A Complete Equational Axiomatization for MPA with String Iteration

Luca Aceto^{∗}

BRICS^{†} Department of Mathematics and Computer Science, Aalborg University Fredrik Bajersvej 7E, 9220 Aalborg Ø, Denmark luca@iesd.auc.dk

Jan Friso Groote^{‡}

Department of Philosophy, University of Utrecht Heidelberglaan 8, 3584 CS Utrecht, The Netherlands jfg@phil.ruu.nl

Abstract

We study equational axiomatizations of bisimulation equivalence for the language obtained by extending Milner’s basic CCS with string iteration. String iteration is a variation on the original binary version of the Kleene star operation p^{∗}q obtained by restricting the first argument to be a non-empty sequence of atomic actions. We show that, for every positive integer k, bisimulation equivalence over the set of processes in this language with loops of length at most k is finitely axiomatizable. We also offer a countably infinite equational theory that completely axiomatizes bisimulation equivalence over the whole language. We prove that this result cannot be improved upon by showing that no finite equational axiomatization of bisimulation equivalence over basic CCS with string iteration can exist, unless the set of actions is empty.

AMS Subject Classification (1991): 68Q40, 68Q42. CR Subject Classification (1991): D.3.1, F.3.2, F.4.2. Keywords and Phrases: Minimal Process Algebra, Kleene star, string iteration, equational logic, bisimulation equivalence.

1 Introduction

Process theory aims at providing a framework for the description and analysis of reactive systems, i.e., systems that compute by reacting to stimuli from their environment. As such systems tend to be, because of their own nature, non-terminating, all process algebraic specification formalisms (cf., e.g., [2, 20, 27, 4]) include facilities for the specification and analysis of infinite behaviours. The description of such behaviours has been traditionally achieved in process theory by means of systems of recursion equations. For example, the recursion equation

∗On leave from the School of Cognitive and Computing Sciences, University of Sussex. Partially supported by the HCM project EXPRESS.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

‡This research has been partly carried out during a visit to Aalborg University.

(1)  X =^{def} send · receive · X

describes a system that is willing to perform alternatively the acts of sending and receiving ad infinitum. In order to extend axiomatic verification methods to reason about processes specified by means of recursion equations, several inference rules for proving equalities involving infinite processes have been studied in the literature. (Cf., e.g., rules like unique fixed-point induction in its various flavours [27, 4], the approximation induction principle [7] and ω-induction [19].)

The research literature on process theory has recently witnessed a resurgence of interest in the study of Kleene star-like operations as an alternative, purely algebraic, way of introducing infinite behaviours in process algebras. (Cf., e.g., the papers [14, 5, 6, 12, 10, 31, 9]). Some of these studies, notably [6], have investigated the expressive power of variations on standard process description languages in which infinite behaviours are defined by means of Kleene’s star operation [22, 8] rather than by means of systems of recursion equations. For example, using the original, binary version of the Kleene star operation from [22] studied in [6], the system described by the recursion equation (1) can alternatively be denoted by the term (send · receive)^{∗}δ, and, as shown in [6], any regular process can be specified in the axiom system ACP_{τ} with Kleene star using only handshake communication. (Interestingly, as already noted by Milner in [26, Sect. 6], not every process defined using finite-state systems of recursion equations can be described, up to bisimulation equivalence, using only regular expressions.)

The possibility of describing infinite behaviours in a purely algebraic syntax has spurred a flurry of research into the expressive power of equational logic to (finitely) axiomatize behavioural equivalences over simple languages incorporating variations on the Kleene star operation. Because of its central nature in process theory, bisimulation equivalence [29, 27] and variations on its theme have been prime candidates for this type of investigation. (Examples of contributions along this line of research may be found in, e.g., [14, 31, 12, 1, 13, 15].) A notable positive result in this direction was obtained by Fokkink and Zantema, who showed in [14] that the finite equational theory for the language of basic process algebra with iteration BPA^{∗} proposed in [6] is indeed complete for bisimulation equivalence over that language. This remarkable result is in sharp contrast with a negative one later obtained by Sewell in [31]. Sewell shows that bisimulation equivalence cannot be finitely axiomatized over the language BPA_{δ}^{∗} obtained by adding the stopped process δ to the signature of BPA^{∗}.

The catastrophic effect, for what concerns finite axiomatizability of bisimulation equivalence, of the addition of the, apparently innocuous, stopped process δ to BPA^{∗} may be slightly disconcerting. Terms in the language BPA^{∗} can denote process graphs with arbitrarily long loops, i.e., sequences of transitions leading back to the state they started from. However, any BPA^{∗} term is normed in the sense of [3], i.e., any term is capable of terminating by performing a finite sequence of transitions. This implies that perpetual behaviours like, for instance, that specified by the recursion equation (1) cannot be denoted by any BPA^{∗} term. It is the normedness of terms that is lost when δ is added to BPA^{∗}.

In an attempt to reconcile finite axiomatizability of bisimulation with the presence of perpetual processes, Fokkink showed in [12] that bisimulation equivalence is finitely axiomatizable over a language obtained by adding prefix iteration to Milner’s basic CCS. The language considered by Fokkink in the aforementioned reference allows for the specification of perpetual behaviours, but such behaviours must have loops of length exactly one.

It is our thesis that the cause of the impossibility of finitely axiomatizing bisimulation equivalence over BPA_{δ}^{∗} is the combination of the loss of normedness and of the existence of unboundedly long loops in behaviours. Intuitively, unlike the case of normed processes, two perpetual behaviours can be bisimilar even if the lengths of their loops are very different. For example, the equality

(2)  (a^{n})^{∗}δ = a^{∗}δ

holds for every positive integer n with respect to any equivalence in the linear timebranching time spectrum [16]. However, as it will be made clear by the proof of Thm. 35, any finite equational theory can only change the length of finitely many loops in terms, and thus cannot prove every equivalence of the form (2).

To provide a formal justification for our thesis, we have chosen to study the expressive power of equational logic in characterizing bisimulation equivalence over the simplest extension of Milner’s basic CCS in which it is possible to express perpetual processes with unboundedly long loops. More precisely, we consider the subset of CCS consisting of the basic operations to denote finite synchronization trees, extended with string iteration w^{∗}P. Intuitively, for a non-empty string of actions w, the term w^{∗}P denotes a process that can execute the string of actions w repeatedly, and that, after each cycle along the w-loop, can decide to behave like P, if P can exhibit any transition at all. We denote the resulting language by MPA^{s∗}(A). An example of a perpetual MPA^{s∗}(A) term is the term (send · receive)^{∗}δ.

Our first main result of the paper is that bisimulation equivalence can be equationally axiomatized over the language MPA^{s∗}(A) (cf. Thm. 29). We also prove that, for every positive integer k, bisimulation equivalence over the set of MPA^{s∗}(A) terms with loops of length at most k has a finite equational axiomatization. Thus it is indeed the case that, at least over MPA^{s∗}(A), bisimulation equivalence between perpetual processes with bounded loops can be finitely axiomatized. On the other hand, if the length of loops in process behaviours is not bounded from above, the equational theory that characterizes bisimulation equivalence over the whole of the language MPA^{s∗}(A) is countably infinite. We show that this result cannot be improved upon by proving that no finite equational axiomatization of bisimulation equivalence over the language MPA^{s∗}(A) can exist, unless the set of actions A is empty. (Cf. Thm. 35.) These positive and negative results are then extended to the language BPA_{δϵ}^{s∗}(A) obtained by extending MPA^{s∗}(A) with general sequential composition in lieu of action prefixing, and with the empty process from [23].

In the process of establishing the aforementioned results, we also obtain solutions to problems of independent interest. In particular, we present a novel, detailed analysis of bisimulation equivalence over a class of simple cyclic terms which we refer to as terminal cycles (cf. Lem. 22). As a technical tool for the study of equalities involving terminal cycles, we also prove a unique decomposition theorem over finite strings (cf. Thm. 2) which may be of independent string-theoretic interest.

We conclude this introduction by providing a brief road-map to the contents of this paper. Section 2 introduces the mathematical results and notations that will be used throughout the paper. In that section we also present a unique decomposition theorem for finite strings that will find application in the later developments of the paper. The language of minimal process algebra with string iteration and its operational semantics are introduced in Sect. 3. Section 4 is entirely devoted to detailed proofs of our completeness theorems for bisimulation equivalence over MPA^{s∗}(A). Perhaps surprisingly, the proofs of the completeness theorems are rather involved, and, for this reason, we have chosen to present them in great detail in a style which is inspired by [24]. The non-existence of a finite equational axiomatization for bisimulation equivalence over the language MPA^{s∗}(A) is presented in Sect. 5. Finally, Sect. 6 is devoted to extensions of our main results to the language BPA_{δϵ}^{s∗}(A).

2 Preliminaries on Strings

We begin with some mathematical preliminaries. In particular, we present a basic result about finite strings which will find application in the remainder of this paper.

Let K be any set. The set of (possibly empty) finite sequences of elements of K, usually referred to as strings, is denoted by K^{∗}. We shall use the symbols s, u, v, w, possibly subscripted and/or superscripted, to range over K^{∗}. String concatenation will be denoted by juxtaposition; λ will be used to denote the empty string, and the sequence containing one element a ∈ K will be written a. We use w^{p}, where w is a string in K^{∗} and p is a non-negative integer, to denote the string \underbrace{w ⋯ w}_{p-times}. By convention, w^{0} will stand

for the empty string λ. As it is standard practice, the set of non-empty strings over K will be denoted by K^{+}. The length of a string w ∈ K^{∗} will be denoted by length(w). We use ℕ = {1, 2, 3, …} for the set of natural numbers. Throughout the paper, the symbol =^{△} will stand for “equals by definition”. For integers p and q, not both zero, we shall write gcd(p, q) for the greatest common divisor of p and q.

The following notions about strings will be useful in the remainder of this paper.

Definition 1. Let w ∈ K^{∗}. A root decomposition of w is a pair (v, n) ∈ K^{∗} × ℕ such that w = v^{n}. The string w is a prime root iff (w, 1) is its only root decomposition. A prime root decomposition of w is a root decomposition (v, n) for it with v a prime root string.

As an example, consider the string w = abab. Both (w, 1) and (ab, 2) are root decompositions of w. In fact, they are the only root decompositions for that string. As w admits a non-trivial root decomposition, i.e. (ab, 2), it is not a prime root. On the other hand, the string ab is a prime root, and (ab, 2) is therefore the unique prime root decomposition for w.

We shall now prove that, as it was the case in the above example, every string w ∈ K^{∗} has a unique prime root decomposition. Apart from its intrinsic string-theoretic interest, this result will be useful to establish an important lemma about the language for processes studied in this paper (cf. Lem. 19).

Theorem 2 (Unique Prime Root Decomposition Theorem). Every string s ∈ K^{∗} has a unique prime root decomposition.

The remainder of this section will be devoted to a proof of the above theorem. In the proof of this result, we shall make use of a result from number theory that may be found in, e.g., [28, Chapter 2]. Before stating this number-theoretic result, we recall a basic notion from number theory.

Definition 3. Let p and q be integers. If a positive integer m divides the difference p − q, we say that p is congruent to q modulo m and write p ≡ q (mod m). In other words, p ≡ q (mod m) iff p = q + km for some integer k.

The following result pertaining to the solution of congruence equations will find an important application in the proof of Thm. 2. The interested reader is referred to, e.g., [28, Corollary 2.9] for its proof.

Theorem 4. Let p, q, r be integers with p and q relatively prime, i.e. with gcd(p, q) = 1, and with q > 0. Then the equation

px ≡ r (mod q)

has a solution x_{1} =^{△} p^{ϕ(q)−1}r, where ϕ(q) is the positive integer associated with q by Euler’s ϕ-function^{1}. All solutions are given by x = x_{1} + jq, where j = 0, ±1, ±2, . . ..

Our application of the above number-theoretic result will be in the proof of the following result about strings.

Lemma 5. Let s ∈ K^{+}. Assume that (u, n) and (v, m) are root decompositions of s. Then (w, k) is a root decomposition of s for some string w of length gcd(length(u), length(v)).

Proof. Let s ∈ K^{+} and assume that (u, n) and (v, m) are both root decompositions of s. Let p =^{△} length(u)/ gcd(length(u), length(v)) and q =^{△} length(v)/ gcd(length(u), length(v)). Note, first of all, that p and q are well-defined positive integers because, as s ∈ K^{+}, both u and v are non-empty strings. Now, both u and v can be expressed (uniquely) as concatenations of, respectively, p and q substrings of length gcd(length(u), length(v)). Therefore, let

(3)  u = u_{1} ⋯ u_{p}
(4)  v = v_{1} ⋯ v_{q}

1As stated in, e.g., [28, Thm. 2.5], ϕ(q) is the number of positive integers less than or equal to q that are relatively prime to q.

where each u_{i} (1 ≤ i ≤ p) and v_{j} (1 ≤ j ≤ q) is of length gcd(length(u), length(v)). As (u, n) and (v, m) are both root decompositions of s, it follows from (3) and (4) above that, for every l ≥ 0,

(5)  (u_{1} ⋯ u_{p})^{ln} = (v_{1} ⋯ v_{q})^{lm} .

We claim that the strings u_{i} and v_{j} are equal for every 1 ≤ i ≤ p and 1 ≤ j ≤ q. To see that this indeed the case, consider arbitrary i ∈ {1, …, p} and j ∈ {1, …, q}. The substring u_{i} occurs at positions

i + px (0 ≤ x ≤ ln − 1)

in the sequence of strings (u_{1} ⋯ u_{p})^{ln}. Similarly, the substring v_{j} occurs at positions

j + qy (0 ≤ y ≤ lm − 1)

in the sequence of strings (v_{1} ⋯ v_{q})^{lm}. If, for some non-negative integers x and y in the given ranges, we have that:

(6)  i + px = j + qy

then there is a position in the string s^{l} = (u_{1} ⋯ u_{p})^{ln} = (v_{1} ⋯ v_{q})^{lm} at which the substrings u_{i} and v_{j} both occur. As length(u_{i}) = length(v_{j}), u_{i} and v_{j} must be equal, as desired. So, all we have to do to prove that u_{i} is equal to v_{j} is to solve (6). This is where Thm. 4 comes into play. In fact, assume, without loss of generality, that j ≥ i. Then, for all integers x and y,

i + px = j + qy ⇔ px = (j − i) + qy
⇔ px ≡ (j − i) (mod q) .

Now, because of the way p and q are defined, it follows that gcd(p, q) = 1. Therefore we may apply Thm. 4 to infer that the congruence equation

px ≡ (j − i) (mod q)

has an infinite family of solutions given by x = x_{1} + hq for h = 0, ±1, ±2, …, where x_{1} =^{△} p^{ϕ(q)−1}(j − i). Now, pick non-negative integers x =^{△} x_{1} and y such that px_{1} = (j − i) + qy. (Note that, as x_{1} ≥ 0 and 0 ≤ j − i ≤ q − 1, it must be the case that y ≥ 0.) Next, pick l ≥ 0 such that i + px_{1} ≤ ln and j + qy ≤ lm. As x_{1} and y are solutions of Eqn. 6, the strings u_{i} and v_{j} occur at the same position in the sequence

s^{l} = (u_{1} ⋯ u_{p})^{ln} = (v_{1} ⋯ v_{q})^{lm}

and are therefore equal. As this holds for every i ∈ {1, …, p} and j ∈ {1, …, q}, it follows that all the u_{i}s and v_{j}s are equal. To finish the proof, it is thus sufficient to take

w =^{△} u_{1}(= u_{2} = ⋯ = u_{p} = v_{1} = ⋯ = v_{q}) and k =^{△} np(= mq). □

Having established the above result, we are now in a position to prove the promised unique prime root decomposition theorem.

Proof of Theorem 2. If s is the empty string, then (s, 1) is its unique root decomposition, which is prime. Assume then that s ∈ K^{+}. Let {(v_{1}, n_{1}), …, (v_{k}, n_{k})} be the non-empty, finite set of root decompositions of s. Choose 1 ≤ i ≤ k such that n_{i} is the maximum of the non-empty set of natural numbers {n_{1}, …, n_{k}}. It follows that v_{i} is a prime root and that (v_{i}, n_{i}) is a prime root decomposition of s. This establishes the existence of such a root decomposition.

We now argue for the uniqueness of such a prime root decomposition. Assume, towards a contradiction, that (v_{j}, n_{j}) is a different prime root decomposition of s. It is immediate to note that v_{i} ≠ v_{j} and n_{i} ≠ n_{j}. Moreover, as n_{i} = max{n_{1}, …, n_{k}}, it must be the case that n_{j} < n_{i} and length(v_{i}) < length(v_{j}). Then, as s = v_{i}^{n_{i}} = v_{j}^{n_{j}}, Lem. 5 gives the existence of a root decomposition (w, k) of s, with w a string of length gcd(length(v_{i}), length(v_{j})). As length(v_{i}) < length(v_{j}), we have also that length(w) < length(v_{j}) and that v_{j} = w^{p} for some positive integer p > 1. This implies that (w, p) is a non-trivial root decomposition of v_{j}, contradicting the assumption that v_{j} were a prime root. This establishes the uniqueness of the prime root decomposition of s. □

To conclude this section, we present a result about prime root strings that will find application in the remainder of this paper. (Cf. Lem. 20.)

Lemma 6. Let s ∈ K^{∗} and a ∈ A. Assume that the string as is a prime root. Then so is sa.

Proof. We show the contrapositive statement. To this end, let s ∈ K^{∗}, and a ∈ A. Assume that sa is not a prime root. We shall prove that as is not a prime root either.

If sa is not a prime root, then there exist a string v ∈ K^{+} and a natural number n > 1 such that sa = v^{n}. As sa = v^{n}, v must be of the form ua for some string u ∈ A^{∗}. Moreover it holds that s = (ua)^{n−1}u. Therefore as = a(ua)^{n−1}u = (au)^{n}. As n > 1, it follows immediately that as cannot be a prime root. □

3 Minimal Process Algebra with String Iteration

We assume a finite set A of observable actions. The symbols a, b, c will be used as typical members of this set. We also assume the existence of a countably infinite set Var of process variables, ranged over by x, y, z. The language of minimal process algebra with string iteration MPA^{s∗}(A, Var) is given by the following grammar:

E ::= x | δ | aE | E + E | w^{∗}E

where x ∈ Var, a ∈ A and w ∈ A^{+}. We shall use E, F, G, possibly subscripted and/or superscripted to range over MPA^{s∗}(A, Var). Instead of repeated action prefix, e.g. a_{1}a_{2} … a_{n}E, we shall often write wE with w = a_{1}a_{2} … a_{n}. By convention, λE ≡ E, where the symbol ≡ stands for syntactic equality of terms. When writing MPA^{s∗}(A, Var) terms, we shall sometimes adopt the following parsing conventions: ^{∗} binds stronger than a, which in turn binds stronger than +.

For a positive integer k, we say that a term E in MPA^{s∗}(A, Var) is k-bounded if the length of any string w occurring in sub-terms of E of the form w^{∗}F is smaller than or equal to k. For a term E, we shall sometimes refer to the smallest k for which E is kbounded as the iteration bound of E, notation IB(E). For example, the iteration bound of the term (ab)^{∗}x + a^{∗}y is 2.

The set of variables occurring in a term E ∈ MPA^{s∗}(A, Var) will be denoted by Var(E). We shall write MPA^{s∗}(A) for the set of closed terms, i.e. terms without occurrences of variables, in the language MPA^{s∗}(A, Var). The symbols P, Q, R, T, possibly subscripted and/or superscripted, will be used to range over closed terms.

A (closed) substitution σ is a mapping from variables in Var to (closed) terms in MPA^{s∗}(A, Var). For every E ∈ MPA^{s∗}(A, Var) and substitution σ, we shall write Eσ for the result of substituting each variable x occurring in E with the term σ(x). For every substitution σ, variable x ∈ Var and term E ∈ MPA^{s∗}(A, Var), we shall use σ[x ↦ E] to denote the substitution mapping x to E, and agreeing with σ on all the other variables.

Definition 7. The size |P | of an MPA^{s∗}(A) term P is defined by structural recursion as follows:

|δ| =^{△} 1
|w^{∗}P | =^{△} length(w) + |P |
|aP | =^{△} 1 + |P |
|P + Q| =^{△} |P | + |Q| + 1

The operational semantics of the language MPA^{s∗}(A) is given by the labelled transition system [21, 30]

(MPA^{s∗}(A), A, {→^{a}| a ∈ A})

where the transition relations →^{a}⊆ MPA^{s∗}(A) × MPA^{s∗}(A) are the least ones satisfying the operational rules in Table 1.

The following trivial lemma ensures that, for every k ∈ ℕ, the language of k-bounded terms is closed under transitions. This property will be implicitly used in the proof of the completeness result for this set of terms.

Lemma 8. Let P be a k-bounded MPA^{s∗}(A) term. Assume that P →^{a} Q. Then Q is also k-bounded.

For each w ∈ A^{∗}, we define the derived transition relation →^{w} by induction on length(w) in the standard way as follows:

• P →^{λ} Q iff P ≡ Q, and

• P →^{aw} Q iff P →^{a} P′ →^{w} Q for some MPA^{s∗}(A) term P′.

aP →^{a} P

\frac{P →^{a} P′}{P + Q →^{a} P′}  \frac{Q →^{a} Q′}{P + Q →^{a} Q′}

(aw)^{∗}P →^{a} w(aw)^{∗}P \frac{P →^{b} P′}{(aw)^{∗}P →^{b} P′}

Table 1: The operational rules for MPA^{s∗}(A) (a, b ∈ A)

For MPA^{s∗}(A) terms P, Q, we say that Q is a state of P iff there exists a string w ∈ A^{∗} such that P →^{w} Q. Not surprisingly, a straightforward argument by structural induction on MPA^{s∗}(A) terms gives that:

Lemma 9. For every P ∈ MPA^{s∗}(A), the set of states of P is finite.

The notion of behavioural equivalence over MPA^{s∗}(A) terms that we shall consider in this paper is that of bisimulation equivalence, due to Park and Milner [29, 27].

Definition 10. A binary relation ℜ over MPA^{s∗}(A) is a bisimulation iff it is symmetric and whenever P ℜ Q, for all a ∈ A, P′ ∈ MPA^{s∗}(A):

if P →^{a} P′, then, for some Q′ ∈ MPA^{s∗}(A), Q →^{a} Q′ and P′ ℜ Q′.

Two MPA^{s∗}(A) terms P, Q are bisimulation equivalent, denoted by P {↔ \atop ––}Q, iff there is a bisimulation relation ℜ such that P ℜ Q.

Bisimulation equivalence can be extended to all of the language MPA^{s∗}(A, Var) in the following standard fashion:

Definition 11. For all E, F ∈ MPA^{s∗}(A, Var), E{↔ \atop ––}F iff Eσ{↔ \atop ––}F σ, for every closed substitution σ.

It is well known that {↔ \atop ––} is an equivalence relation, and, as the rules in Table 1 are in tyft/tyxt-format [17], it is also a congruence relation. Therefore it makes sense to form the quotient algebra MPA^{s∗}(A)/{↔ \atop ––}. The following lemma states a cardinality property of the algebra MPA^{s∗}(A)/{↔ \atop ––} that will be useful in the developments in Sect. 5 (cf. Lem. 32).

Lemma 12. If the set of actions A is non-empty, then the (carrier of the) quotient algebra MPA^{s∗}(A)/{↔ \atop ––} is countably infinite.

Proof. If A is non-empty, then we can pick an action a ∈ A. For each natural number n, we may then define the term P_{n} =^{△} a^{n}δ. It is trivial to see that, for all n, m ∈ ℕ, P_{n}{↔ \atop ––}P_{m} iff n = m. □

A1  x + y = y + x
A2  (x + y) + z = x + (y + z)
A3  x + x = x
A6  x + δ = x
S1  x + w(w^{∗}x) = w^{∗}x
S2  w^{∗}(w^{∗}x) = w^{∗}x
S3  (w^{n})^{∗}δ = w^{∗}δ
S4  a(ua)^{∗}δ = (au)^{∗}δ

Table 2: The axioms for MPA^{s∗}(A) (w ∈ A^{+}, u ∈ A^{∗} and n ∈ ℕ)

The main aim of this paper will be to provide a complete equational axiomatization of bisimulation equivalence over the language MPA^{s∗}(A), and the whole of the next section will be devoted to this end.

4 An Equational Axiomatization for MPA^{s∗}(A)

The equational axioms in Table 2 will be shown to completely characterize the relation of bisimulation equivalence between MPA^{s∗}(A) terms. We shall refer to this equational theory as MPA^{s∗}. By analogy with our terminology for MPA^{s∗}(A, Var) terms, in case the length of the strings w^{n}, w, ua and au mentioned in axioms S1–S5 does not exceed k we call these axioms k-bounded. In this case we refer to the resulting set of axioms as MPA_{k}^{s∗}. Note that, as the set of actions A is finite, the family of axioms MPA_{k}^{s∗} is finite, for every positive integer k. The equational theory MPA^{s∗}, however, consists of a countably infinite collection of equations.

Definition 13. For an equational theory E over the signature of MPA^{s∗}(A), we write E ⊢ P = Q iff the equality P = Q can be derived from those in E using the rules of equational logic. (For ease of reference, the inference rules of equational logic are collected in Table 3.) We also write E ⊢ Q ⊆ P, read “Q is a provable summand of P ” or “Q can be absorbed into P ”, iff E ⊢ P + Q = P. By convention, all the equational theories we shall consider in this section will contain axioms A1 and A2.

In equational proofs to follow, we shall find it useful to have the following equations at hand:

\begin{aligned}S5 & (w^{n})^{∗}w^{∗}δ & = & w^{∗}δ \\ S6 & w^{∗}x & = & w^{∗}x + x \\ S7 & w^{∗}x & = & w^{∗}x + w(w^{∗}x) \end{aligned}

Equations S6 and S7 are easily seen to be derivable from S1 and A3. Finally, note that equation S5 is derivable from axioms S2 and S3 as follows:

(w^{n})^{∗}w^{∗}δ =^{S3} (w^{n})^{∗}(w^{n})^{∗}δ =^{S2} (w^{n})^{∗}δ =^{S3} w^{∗}δ .

\overline{E = E} \frac{F = E}{E = F} \frac{E = F F = G}{E = G}
\overline{Eσ = F σ} (E = F) ∈ E, σ a substitution

\frac{E_{i} = F_{i} (1 ≤ i ≤ n)}{f(E_{1}, …, E_{n}) = f(F_{1}, …, F_{n})} f an operation symbol of arity n

Table 3: The inference rules of equational logic

The first main result of this paper can now be stated.

Theorem 14. The axiom system in Table 2 is sound and complete for bisimulation equivalence over the language MPA^{s∗}(A), i.e. for all MPA^{s∗}(A) terms P and Q,

P {↔ \atop ––}Q ⇔ MPA^{s∗} ⊢ P = Q.

Moreover, for k-bounded MPA^{s∗}(A)-terms P and Q, we find

P {↔ \atop ––}Q ⇔ MPA_{k}^{s∗} ⊢ P = Q.

The remainder of this section will be devoted to a detailed proof of the above result. The proof we present is similar in spirit to those for related results given in, e.g., [18, 1, 13, 15], but the details will be rather different and, perhaps surprisingly, quite involved.

First of all, we establish the soundness of the equational theory MPA^{s∗}.

Lemma 15 (Soundness). For all MPA^{s∗}(A, Var) terms E, F, MPA^{s∗} ⊢ E = F implies

E{↔ \atop ––}F.

Proof. As bisimulation equivalence is a congruence with respect to the operators of the language MPA^{s∗}(A, Var), the soundness of the axiom system MPA^{s∗} can be shown by establishing that each axiom in MPA^{s∗} is sound. This easy, but somewhat tedious, verification is left to the reader. □

We remark here that the soundness of equation S3 depends crucially on the fact that the argument of the string iteration construct is a stopped process, i.e., a process that cannot exhibit any transition. In fact, in general, w^{∗}P {↮ \atop ––}(w^{n})^{∗}P. As an example, consider w =^{△} a, n =^{△} 2 and P ≡ bδ. Then a^{∗}P {↮ \atop ––}(aa)^{∗}P because a^{∗}P →^{ab} δ, whereas (aa)^{∗}P cannot perform the string of actions ab.

The rest of this section is devoted to the much more challenging proof of the completeness of the equational theory MPA^{s∗} with respect to bisimulation equivalence, which we shall approach in several intermediate stages.

Lemma 16. Let P be an MPA^{s∗}(A) term such that P {↔ \atop ––}δ. Then A6 ⊢ P = δ.

Proof. A straightforward induction on the structure of P. □

The following definition introduces a class of processes in MPA^{s∗}(A) that will play an important role in the proof of our completeness theorem.

Definition 17. An MPA^{s∗}(A) term P is called a terminal cycle if P {↔ \atop ––}w^{∗}δ for some string w ∈ A^{+}. An MPA^{s∗}(A) term P is terminal iff P {↔ \atop ––}δ or P is a terminal cycle.

For example, an MPA^{s∗}(A) term of the form u(wu)^{∗}δ, where at least one of the strings u, v is non-empty, is a terminal cycle because it is bisimulation equivalent to the term (uw)^{∗}δ.

Lemma 18. Let P be an MPA^{s∗}(A) term and u ∈ A^{∗}. If the term uP is a terminal cycle, then so is P.

Proof. We prove the thesis by induction on the length of the string u. If u is empty, then the lemma follows immediately by convention. Otherwise, assume that u = au′ and uP is a terminal cycle. This means that uP {↔ \atop ––}v^{∗}δ for some v ∈ A^{+}. As uP →^{a} u′P, it must be the case that v = av′ for some v′ ∈ A^{∗}, and that u′P {↔ \atop ––}v′(av′)^{∗}δ. Repeated applications of the sound equation S4 give that u′P {↔ \atop ––}(v′a)^{∗}δ. Hence, the term u′P is itself a terminal cycle, and, by the inductive hypothesis, so is P. □

We remark here that the property of being a terminal cycle is not preserved by the action prefixing operation, i.e. the converse of the above lemma does not hold. For example, the term a^{∗}δ is obviously a terminal cycle, but b(a^{∗}δ) is not.

The following result, whose proof uses Thm. 2 in an essential way, states an important property of terminal cycles that will be used in proving the completeness of our axiom system for that sub-class of processes.

Lemma 19. Let v, w ∈ A^{+} and P ∈ MPA^{s∗}(A). Suppose that v^{∗}P {↔ \atop ––}w^{∗}δ. Then there exist a prime root string s ∈ A^{+} and natural numbers k, h such that v = s^{k} and w = s^{h}.

Proof. Assume that v^{∗}P {↔ \atop ––}w^{∗}δ. Let n =^{△} length(w) and m =^{△} length(v). As v^{∗}P {↔ \atop ––}w^{∗}δ, it follows that v^{n} = w^{m}. By Thm. 2, the strings v and w have unique prime root decompositions (s_{v}, k_{v}) and (s_{w}, k_{w}), respectively. Therefore the string v^{n}(= u^{m}) has prime root decompositions (s_{v}, nk_{v}) and (s_{w}, mk_{w}). Again by Thm. 2, these two root decompositions must be equal, i.e., it must be the case that s_{v} = s_{w} and nk_{v} = mk_{w}. To establish the thesis, it is thus sufficient to take s =^{△} s_{v}(= s_{w}), k =^{△} k_{v} and h =^{△} k_{w}. □

Lemma 20. Let P be a k-bounded MPA^{s∗}(A) term. Suppose that P is a terminal cycle. Then P {↔ \atop ––}s^{∗}δ for some prime root string s of length at most k.

Proof. Assume that P is a k-bounded terminal cycle. Then there exists a string v ∈ A^{+} such that P {↔ \atop ––}v^{∗}δ. Let (s, n) be the unique prime root decomposition for v given by Thm. 2. Using the sound equation S3, we derive that P {↔ \atop ––}s^{∗}δ. The thesis now follows from the following claim:

Claim. For every k-bounded term P and prime root string s,

P {↔ \atop ––}s^{∗}δ implies length(s) ≤ k .

This claim can be proven by structural induction on P. We only examine two of the possible forms P may take.

• Case: P ≡ aQ.

As P ≡ aQ{↔ \atop ––}s^{∗}δ, it is not hard to see that it must be the case that s = as′ and Q{↔ \atop ––}(s′a)^{∗}δ for some string s′. By Lem. 6, the string s′a is also a prime root. As Q is itself k-bounded, we may apply the inductive hypothesis to derive that length(as′) = length(s′a) ≤ k.

• Case: P ≡ v^{∗}Q.

As P ≡ v^{∗}Q{↔ \atop ––}s^{∗}δ and s is a prime root, we may apply Lem. 19 to derive that v = s^{h} for some natural number h. As P is k-bounded, the length of the string v is at most k. Thus length(s) ≤ k as desired.

□

Using the above results, we are now in a position to establish the completeness of our axiom system for terminal cycles.

Notation 21. We shall use TerCycles to denote the equational theory consisting of equations A3,A6,S2,S3,S4. As usual, for every positive integer k, TerCycles_{k} will stand for the equational theory consisting of the k-bounded instances of equations in TerCycles.

Lemma 22. Let P ∈ MPA^{s∗}(A) and w ∈ A^{+}. Assume that P {↔ \atop ––}w^{∗}δ. Then TerCycles ⊢ P = w^{∗}δ. Moreover, if P and w^{∗}δ are k-bounded, then TerCycles_{k} ⊢ P = w^{∗}δ.

Proof. Assume that P {↔ \atop ––}w^{∗}δ for some w ∈ A^{+}. We prove the thesis by induction on the structure of P. We proceed by a case analysis on the form P may take.

• Case: P ≡ δ.

Vacuous, as P {↮ \atop ––}w^{∗}δ.

• Case: P ≡ aP_{1}.

As P ≡ aP_{1}{↔ \atop ––}w^{∗}δ, the string w must be of the form aw′ for some w′ ∈ A^{∗}. In this case, it is not hard to see that P_{1}{↔ \atop ––}(w′a)^{∗}δ. By the inductive hypothesis, it follows that TerCycles ⊢ P_{1} = (w′a)^{∗}δ. So, TerCycles ⊢ P = a(w′a)^{∗}δ =^{S4} (aw′)^{∗}δ, as desired.

• Case: P ≡ P_{1} + P_{2}.

As P {↔ \atop ––}w^{∗}δ, it is easy to see that one of the following three cases must hold:

1. P_{1}{↔ \atop ––}δ and P_{2}{↔ \atop ––}w^{∗}δ, or

2. P_{2}{↔ \atop ––}δ and P_{1}{↔ \atop ––}w^{∗}δ, or

3. both P_{1} and P_{2} are bisimulation equivalent to w^{∗}δ.

The first two cases can be easily dealt with using Lem. 16, the inductive hypothesis and axiom A6. In the last case, using the induction hypothesis, we have that TerCycles ⊢ P_{i} = w^{∗}δ for i = 1, 2. So, TerCycles ⊢ P ≡ P_{1} + P_{2} = w^{∗}δ + w^{∗}δ =^{A3} w^{∗}δ.

• Case: P ≡ v^{∗}P_{1}, for some v ∈ A^{+}.

As P {↔ \atop ––}w^{∗}δ, by Lem. 19 there exists a prime root string s and natural numbers k, h such that v = s^{k} and w = s^{h}. We proceed by distinguishing two cases depending on whether P_{1} has any transition or not.

1. Case: P_{1} →^{a} P′_{1} for no a ∈ A and P′_{1} ∈ MPA^{s∗}(A). In this case P_{1}{↔ \atop ––}δ. Now Lem. 16 gives that A6 ⊢ P_{1} = δ. Therefore,

TerCycles ⊢ P =^{A6} v^{∗}δ
= (s^{k})^{∗}δ
=^{S3} s^{∗}δ
=^{S3} (s^{h})^{∗}δ
= w^{∗}δ

and we are done.

2. Case: P_{1} →^{a} P′_{1} for some a ∈ A and P′_{1} ∈ MPA^{s∗}(A). We claim that, in this case, P_{1}{↔ \atop ––}w^{∗}δ. To see that this does hold, note that, as P_{1} →^{a} P′_{1} and v^{∗}P_{1}{↔ \atop ––}w^{∗}δ, it must be the case that w = aw′ for some w′ ∈ A^{∗}, and that P′_{1}{↔ \atop ––}w′(aw′)^{∗}δ{↔ \atop ––}(w′a)^{∗}δ. Indeed, whenever P_{1} →^{b} P′ for some action b and MPA^{s∗}(A) process P′, it follows that a = b and P′{↔ \atop ––}(w′a)^{∗}δ. This implies

that P_{1}{↔ \atop ––}a(w′a)^{∗}δ{↔ \atop ––}(aw′)^{∗}δ, as claimed.

Now, as P_{1}{↔ \atop ––}w^{∗}δ, an application of the inductive hypothesis gives TerCycles ⊢ P_{1} = w^{∗}δ. Therefore,

TerCycles ⊢ P = v^{∗}(w^{∗}δ)
= (s^{k})^{∗}((s^{h})^{∗}δ)
=^{S3} (s^{k})^{∗}(s^{∗}δ)
=^{S5} s^{∗}δ
=^{S3} (s^{h})^{∗}δ
= w^{∗}δ

and we are done.

An inspection of the above proof shows that only k-bounded instances of the equations S2–S4 need be used in the proof if P and w^{∗}δ are both k-bounded. This completes the inductive argument, and the proof of the lemma. □

As an easy corollary of the above lemma, we can now prove that the equational theory TerCycles completely characterizes bisimulation equivalence over terminal cycles.

Corollary 23. Let P, Q be terms in MPA^{s∗}(A). Assume that P {↔ \atop ––}Q and P is a terminal cycle. Then TerCycles ⊢ P = Q. Moreover, if P and Q are k-bounded, TerCycles_{k} ⊢ P = Q.

Proof. Assume that P {↔ \atop ––}Q and P is a terminal cycle. By Def. 17, this means that P {↔ \atop ––}w^{∗}δ for some string w ∈ A^{+}. By Lem. 22 and the fact that bisimulation equivalence is an equivalence relation, we have that TerCycles ⊢ P = w^{∗}δ = Q, from which the thesis follows immediately by transitivity. An identical argument shows that if P and Q are k-bounded, then TerCycles_{k} ⊢ P = Q. In fact, by Lem. 20, in that case we can choose w to be a prime root string of length at most k. □

Terminal cycles are processes with very simple cyclic behaviour. Surprisingly, however, to the best of our knowledge, the results we have presented so far give the first systematic investigation of their properties in the literature. In particular, the completeness result in Corollary 23 appears to be new. As terminal cycles are strongly determinate processes in the sense of [27, Def. 11.2], by the main result in [11] and [27, Propn. 11.5], all the equivalences in the linear time-branching time spectrum considered in [16] coincide over the set of such processes. As a result, Corollary 23 gives a complete axiomatization of all the equivalences in van Glabbeek’s study [16] over terminal cycles.

The reader might have noticed that in establishing our completeness theorem for bisimulation equivalence over terminal cycles, we have never needed to use equation S1. This equation will, however, play a crucial rôle in the extension of the completeness result to the whole of the language MPA^{s∗}(A). This we now proceed to present.

Definition 24. For every MPA^{s∗}(A) term P we define its minimum distance to a terminal term by:

|P |_{min} =^{△} min{length(w) | ∃P′ : P →^{w} P′ and P′ is a terminal term} .

For example, |P |_{min} = 0 iff P is a terminal term, and |aaδ + a^{∗}δ|_{min} = 1 because aaδ + a^{∗}δ →^{a} a^{∗}δ is the shortest sequence of transitions from aaδ + a^{∗}δ leading to a terminal term.

The following lemma collects some basic properties of the minimum distance to terminal terms that will find application in the proof of the completeness theorem.

Lemma 25.

1. For every MPA^{s∗}(A) term P, |P |_{min} ∈ ℕ, i.e. | · |_{min} is well defined.

2. Let P and Q be MPA^{s∗}(A) terms. If P {↔ \atop ––}Q, then |P |_{min} = |Q|_{min}.

3. Let P be an MPA^{s∗}(A) term and let w ∈ A^{∗}. Assume that |P |_{min} > 0. Then |wP |_{min} = length(w) + |P |_{min}.

Proof. Statements 1 and 2 of the lemma are easily seen to hold. Here we present a proof of statement 3 by induction on the length of the string w.

Suppose that P is an MPA^{s∗}(A) term such that |P |_{min} > 0. Let w ∈ A^{∗}. We aim at showing that |wP |_{min} = length(w) + |P |_{min}. This is immediate if w is the empty string λ. For the inductive step, assume that w = aw′ for some action a and string w′. By the inductive hypothesis, we infer that:

(7)  |w′P |_{min} = length(w′) + |P |_{min} .

Note moreover that, as |P |_{min} > 0, by Lem. 18 the term aw′P cannot be terminal. We can now reason as follows:

|aw′P |_{min} = min{length(v) | ∃P′ : aw′P →^{v} P′ and P′ is a terminal term}

(Definition of | · |_{min})

= min{length(av) | ∃P′ : w′P →^{v} P′ and P′ is a terminal term}

(aw′P is not a terminal term)

= min{length(aw′u) | ∃P′ : P →^{u} P′ and P′ is a terminal term}

(7)

= length(aw′) + |P |_{min}

(Definition of | · |_{min})

and the inductive step follows. □

It is interesting to note that statement 3 in the previous lemma does not hold if the term P is a terminal cycle. As an example witnessing this fact, consider the term a(a^{∗}δ). Then |a(a^{∗}δ)|_{min} = 0 ≠ 1 + |a^{∗}δ|_{min}.

The following result is a variation on the so-called absorption lemma, a standard tool in proofs of completeness theorems for process algebras (cf., e.g., [18, 27]), and we shall use it heavily in the proof of our main result.

Lemma 26 (Operational Completeness). Let P be a MPA^{s∗}(A) term. If P →^{a} P′ then the two following statements hold:

• A3, S1 ⊢ aP′ ⊆ P, and

• if |P′| ≥ |P | then there exist a string w ∈ A^{∗} and an MPA^{s∗}(A) term P′′ such that P′ ≡ wP′′, A3, S1 ⊢ P′′ ⊆ P and |P′′| ≤ |P |.

Moreover, if P is k-bounded, then only k-bounded instances of axiom S1 need be used in the equational proofs.

Proof. We prove both statements by induction on the length of the proof of the transition P →^{a} P′. We proceed by a case analysis on the last rule used in such a proof.

• Case: P ≡ a.P′ →^{a} P′.

Trivially, A3 ⊢ aP′ ⊆ P and this establishes statement 1. Statement 2 is vacuous as |P′| < |P |.

• Case: P ≡ P_{1} + P_{2} →^{a} P′ because P_{i} →^{a} P′ for some i ∈ {1, 2}.

Assume without loss of generality that P_{1} →^{a} P′. To prove that statement 1 holds it is sufficient to note that the inductive hypothesis for this statement gives that A3, S1 ⊢ aP′ ⊆ P_{1}. By the form of P, A3, S1 ⊢ aP′ ⊆ P follows immediately.

We now show that statement 2 also holds. Assume that |P′| ≥ |P |. Trivially, |P′| > |P_{1}| also holds. We may thus apply the inductive hypothesis for statement 2 to derive that there exist a string w and a term P′′ such that P′ ≡ wP′′, A3, S1 ⊢ P′′ ⊆ P_{1} and |P′′| ≤ |P_{1}|. Clearly, it follows that A3, S1 ⊢ P′′ ⊆ P_{1} ⊆ P and |P′′| ≤ |P_{1}| < |P |.

• Case: P ≡ (av)^{∗}P_{1} →^{a} vP ≡ P′.

Statement 1 follows immediately by equation S7. To prove statement 2, it is sufficient to take P′′ =^{△} P and w =^{△} v.

• Case: P ≡ v^{∗}P_{1} →^{a} P′ because P_{1} →^{a} P′.

Statement 1 is immediate by induction and equation S6. To prove statement 2, assume that |P′| ≥ |P |. As |P | > |P_{1}|, we may apply the inductive hypothesis to infer that there exist a string w and a term P′′ such that P′ ≡ wP′′, A3, S1 ⊢ P′′ ⊆ P_{1} and |P′′| ≤ |P_{1}|. Therefore, as S6 ⊢ P_{1} ⊆ P, we conclude that A3, S1 ⊢ P′′ ⊆ P and |P′′| ≤ |P_{1}| < |P | as desired.

An inspection of the above cases shows that if P is k-bounded, then only k-bounded instances of equation S1 need be used in the proof. This completes the inductive argument and the proof of the lemma. □

We now establish a decomposition property of string iteration with respect to the relation of bisimulation equivalence. A similar decomposition property for the delay operation of Milner’s SCCS [25] with respect to a notion of strong bisimulation preorder was, to our knowledge, first shown by Hennessy in [18]. Our proof follows the one given in [1, Lem. 4.3].

Lemma 27. Let P, Q ∈ MPA^{s∗}(A) and w ∈ A^{+}. Then w^{∗}P {↔ \atop ––}w^{∗}Q iff w^{∗}P {↔ \atop ––}Q or P {↔ \atop ––}w^{∗}Q

or P {↔ \atop ––}Q.

Proof. The “if” implication follows immediately from the fact that {↔ \atop ––} is a congruence and the soundness of equation S2. To show the “only if” implication, it is sufficient to prove that:

(8)  w^{∗}P {↔ \atop ––}w^{∗}Q and w^{∗}P {↮ \atop ––}Q and P {↮ \atop ––}w^{∗}Q ⇒ P {↔ \atop ––}Q .

We prove that (8) holds. To this end, let us assume that w^{∗}P {↔ \atop ––}w^{∗}Q, w^{∗}P {↮ \atop ––}Q and P {↮ \atop ––}w^{∗}Q. By symmetry, to prove that P {↔ \atop ––}Q must hold, it is sufficient to show that, for all a ∈ A, P′ ∈ MPA^{s∗}(A):

(9)  P →^{a} P′ ⇒ ∃Q′ : Q →^{a} Q′ and P′{↔ \atop ––}Q′ .

This we now proceed to show. Assume that P →^{a} P′. By the operational semantics for MPA^{s∗}(A), this implies that w^{∗}P →^{a} P′. As w^{∗}P {↔ \atop ––}w^{∗}Q, it follows that w^{∗}Q →^{a} Q′ for some Q′ such that P′{↔ \atop ––}Q′. If Q →^{a} Q′, then we are done. Otherwise, it must be case that, for some string w′, w = aw′ and Q′ ≡ w′(w^{∗}Q). We show that this leads to a contradiction.

Assume that P →^{a} P′{↔ \atop ––}w′(w^{∗}Q), with w = aw′. Then:

P {↔ \atop ––} P + aP′  (By Lemmas 26(1) and 15)
{↔ \atop ––} P + aw′(w^{∗}Q) (P′{↔ \atop ––}w′(w^{∗}Q))
{↔ \atop ––} P + aw′(w^{∗}P) (w^{∗}P {↔ \atop ––}w^{∗}Q)
{↔ \atop ––} w^{∗}P  (Soundness of axiom S1 and w = aw′)
{↔ \atop ––} w^{∗}Q  (w^{∗}P {↔ \atop ––}w^{∗}Q)

This contradicts the assumption that P {↮ \atop ––}w^{∗}Q. □

The last stepping stone towards the proof of the completeness theorem we are after is the following lemma, which states some properties of bisimulation equivalence over MPA^{s∗}(A) terms which are not terminal.

Lemma 28. Let P, Q ∈ MPA^{s∗}(A). The following statements hold:

1. Assume that |P |_{min} > 0, v ∈ A^{∗} and avP {↔ \atop ––}Q. Then Q cannot have the form w^{∗}Q_{1} for any w ∈ A^{+} and MPA^{s∗}(A) term Q_{1}.

2. Let v, w ∈ A^{∗}. Assume that Q ≡ (aw)^{∗}R for some MPA^{s∗}(A) term R, |Q|_{min} > 0 and vP {↔ \atop ––}wQ. Then length(v) ≤ length(w) and P {↔ \atop ––}uQ for some u ∈ A^{∗} such that w = vu.

Proof. We prove the two statements separately.

1. Suppose that |P |_{min} > 0, v ∈ A^{∗} and avP {↔ \atop ––}Q. We prove that Q cannot have the form w^{∗}Q_{1} for any w ∈ A^{+} and MPA^{s∗}(A) term Q_{1}. To this end, assume, towards a contradiction, that Q ≡ w^{∗}Q_{1}. First of all, note that, as |P |_{min} > 0, Lem. 25(3) gives that:

(10)  |avP |_{min} = length(av) + |P |_{min} .

As avP {↔ \atop ––}Q, by Lem. 25(2) we derive that:

(11)  |avP |_{min} = |Q|_{min} .

Note that, from the above equalities, we can derive immediately that |Q|_{min} > 0. Furthermore, again from avP {↔ \atop ––}Q, it follows that w = aw′, for some w′ ∈ A^{∗}, and that vP {↔ \atop ––}w′Q. Using this information we can now derive that:

|Q|_{min} = |avP |_{min}  (11)
= length(av) + |P |_{min} (10)
= 1 + |vP |_{min}  (Lem. 25(3))
> |w′Q|_{min}  (Lem. 25(2) and vP {↔ \atop ––}w′Q)
≥ |Q|_{min}  (By Lem. 25(3) as |Q|_{min} > 0) .

This is clearly a contradiction.

2. Suppose that Q ≡ (aw)^{∗}R for some MPA^{s∗}(A) term R, |Q|_{min} > 0 and vP {↔ \atop ––}wQ. We prove, first of all, that length(v) ≤ length(w). To this end, assume, towards a contradiction, that length(v) > length(w). As vP {↔ \atop ––}wQ, w must be a proper prefix of v. This means that there exists a non-empty string u such that v = wu and uP {↔ \atop ––}Q. Because of the form Q takes, uP {↔ \atop ––}Q implies that u = (aw)^{k}au′ and P {↔ \atop ––}u′′Q for some k ≥ 0 and strings u′, u′′ such that w = u′u′′. By statements (2) and (3) of

Lemma 25, P {↔ \atop ––}u′′Q and |Q|_{min} > 0 imply that |P |_{min} = |u′′Q|_{min} > 0. Thus we

have that uP {↔ \atop ––}Q ≡ (aw)^{∗}R, u ∈ A^{+} and |P |_{min} > 0. This contradicts statement 1 of this lemma. Therefore it must be the case that length(v) ≤ length(w). The fact that P {↔ \atop ––}uQ for some u ∈ A^{∗} such that w = vu is now immediate.

□

We can now tackle the proof of the promised completeness theorem. Unfortunately, the proof of this result is combinatorial in nature and consists of the examination of a fairly large number of cases. For this reason, we have chosen to present the proof in a structured style following the spirit, albeit not the letter, of the proposal in [24]. We hope that this type of presentation will help the reader understand easily the details of the proof and judge its correctness, if he/she wishes to do so.

Theorem 29 (Completeness). For all MPA^{s∗}(A) terms P and Q, P {↔ \atop ––}Q implies MPA^{s∗} ⊢ P = Q. Moreover, if P and Q are k-bounded then MPA_{k}^{s∗} ⊢ P = Q.

Proof. We shall show that the following three statements hold for all P, Q ∈ MPA^{s∗}(A):

1. Suppose that w ∈ A^{+}, |P |_{min} > 0 and wP {↔ \atop ––}Q. Then there exists an MPA^{s∗}(A) term Q′ such that P {↔ \atop ––}Q′, MPA^{s∗} ⊢ Q = wQ′ and |Q′| + length(w) ≤ |Q|.

2. If P {↔ \atop ––}P + Q then MPA^{s∗} ⊢ Q ⊆ P.

3. If P {↔ \atop ––}Q then MPA^{s∗} ⊢ P = Q^{2}.

We prove these three statements simultaneously by complete induction on |P | + |Q|. To this end, let us assume, as our inductive hypothesis, that statements 1–3 hold for all MPA^{s∗}(A) terms P′, Q′ such that |P′| + |Q′| < |P | + |Q|. We now prove that they hold for P and Q. We examine each statement in turn.

1. Suppose that w ∈ A^{+}, |P |_{min} > 0 and wP {↔ \atop ––}Q. We show that the thesis for statement 1 above holds by a case analysis on the form Q may take. Throughout the proof for this statement, we let w = aw′ for some w′ ∈ A^{∗}.

• Case: Q ≡ δ. The claim is vacuously true because aw′P cannot be bisimilar to δ.

2Strictly speaking, it is not necessary to isolate this statement for the proof below to go through. In fact, all the uses of statement 3 made in the proof are implied by statement 2. However, we believe that the current formulation makes it easier to follow our arguments in detail.

• Case: Q ≡ bQ_{1}.

As aw′P is bisimulation equivalent to Q, it must be the case that a = b and w′P {↔ \atop ––}Q_{1}. We now proceed by distinguishing two cases, depending on whether the string w′ is empty or not.

– Case: w′ = λ.

The claim follows immediately by taking Q′ =^{△} Q_{1}.

– Case: w′ ∈ A^{+}.

In this case, we have that w′P {↔ \atop ––}Q_{1}, w′ ∈ A^{+} and |P |_{min} > 0. As |P | + |Q_{1}| < |P | + |Q|, we may apply the inductive hypothesis for statement 1 to derive that, for some MPA^{s∗}(A) term Q′,

P {↔ \atop ––}Q′ and MPA^{s∗} ⊢ Q_{1} = w′Q′ and |Q′| + length(w′) ≤ |Q_{1}| .

It is now a simple matter to show that this term Q′ satisfies all the constraints in the thesis of statement 1.

This completes the proof for this case.

• Case: Q ≡ Q_{1} + Q_{2}. As aw′P {↔ \atop ––}Q, one of the following three cases must hold:

– Q_{1}{↔ \atop ––}δ and Q_{2}{↔ \atop ––}aw′P, or

– Q_{2}{↔ \atop ––}δ and Q_{1}{↔ \atop ––}aw′P, or

– Q_{1}{↔ \atop ––}Q_{2}{↔ \atop ––}aw′P.

In fact, as the first two cases are symmetric, we may restrict ourselves, without loss of generality, to considering only the first and the third.

– Case: Q_{1}{↔ \atop ––}δ and Q_{2}{↔ \atop ––}aw′P.

As Q_{1}{↔ \atop ––}δ, an application of Lem. 16 gives that

A6 ⊢ Q_{1} = δ . (12)

As |P | + |Q_{2}| < |P | + |Q|, Q_{2}{↔ \atop ––}aw′P and |P |_{min} > 0, we may apply

the inductive hypothesis for statement 1 to derive that there exists an MPA^{s∗}(A) term Q′ such that P {↔ \atop ––}Q′, |Q′| + length(aw′) ≤ |Q_{2}| and

MPA^{s∗} ⊢ Q_{2} = aw′Q′ . (13)

Now,

MPA^{s∗} ⊢ Q = Q_{1} + Q_{2} (Q ≡ Q_{1} + Q_{2})
= δ + aw′Q′ (By (12) and (13))
=^{A6} aw′Q′

and |Q′| + length(aw′) ≤ |Q_{2}| < |Q|. This completes the proof for this case.

– Case: Q_{1}{↔ \atop ––}Q_{2}{↔ \atop ––}aw′P.

In this case, as |P | + |Q_{i}| < |P | + |Q| for i = 1, 2, we may apply the inductive hypothesis for statement 1 to derive that, for i = 1, 2, there exist MPA^{s∗}(A) terms Q′_{i} such that P {↔ \atop ––}Q′_{i}, |Q′_{i}| + length(aw′) ≤ |Q_{i}| and

MPA^{s∗} ⊢ Q_{i} = aw′Q′_{i} . (14)

Now, as |Q′_{i}| + length(aw′) ≤ |Q_{i}| < |Q| (i = 1, 2), it follows that |P | + |Q′_{i}| < |P | + |Q| for i = 1, 2. We may therefore apply the inductive hypothesis for statement 3 to the equivalences P {↔ \atop ––}Q′_{1} and P {↔ \atop ––}Q′_{2} to derive that: MPA^{s∗} ⊢ P = Q′_{1} = Q′_{2} . (15)

Choose Q′ =^{△} Q′_{1}. We have already seen that P {↔ \atop ––}Q′ and that |Q′| + length(aw′) < |Q|. Moreover,

MPA^{s∗} ⊢ Q = Q_{1} + Q_{2}  (Q ≡ Q_{1} + Q_{2})
= aw′Q′_{1} + aw′Q′_{2} (14)
= aw′Q′_{1} + aw′Q′_{1} (15)
=^{A3} aw′Q′_{1}

This completes the proof for this case. The proof for the case Q ≡ Q_{1} + Q_{2} is now complete.

• Case: Q ≡ v^{∗}Q_{1} for some v ∈ A^{+}. This case is vacuous by Lem. 28(1).

The proof of the inductive step for statement 1 is now complete.

2. Assume that P {↔ \atop ––}P + Q. We shall show that MPA^{s∗} ⊢ Q ⊆ P. To this end, we consider the following three cases:

(a) P is a terminal term, i.e. |P |_{min} = 0, or

(b) |P |_{min} > 0 and |Q|_{min} = 0, or

(c) |P |_{min} > 0 and |Q|_{min} > 0.

We examine each of these cases in turn.

(a) Case: P is a terminal term, i.e. |P |_{min} = 0. As |P |_{min} = 0, we have that either P {↔ \atop ––}δ or P is a terminal cycle. If P {↔ \atop ––}δ{↔ \atop ––}P + Q, then the claim is an immediate corollary of Lem. 16 and transitivity. If P is a terminal cycle, then the claim follows immediately from Corollary 23.

(b) Case: |P |_{min} > 0 and |Q|_{min} = 0. Again, as |Q|_{min} = 0, it follows that either Q{↔ \atop ––}δ or Q is a terminal cycle. We proceed by examining these possibilities in turn.

If Q{↔ \atop ––}δ, then

MPA^{s∗} ⊢ P =^{A3} P + δ
= P + Q (By Lem. 16)

and we are done. If Q is a terminal cycle, then Q{↔ \atop ––}(aw)^{∗}δ for some action a ∈ A and string w ∈ A^{∗}. (Note that, by Lem. 20, aw can be chosen to be a prime root string whose length does not exceed the iteration bound of Q.) By Lem. 22, it follows that:

(16) TerCycles ⊢ Q = (aw)^{∗}δ .

As {↔ \atop ––} is a congruence, we infer that P {↔ \atop ––}P + (aw)^{∗}δ. Since P + (aw)^{∗}δ →^{a} w(aw)^{∗}δ, there exists an MPA^{s∗}(A) term P′ such that

P →^{a} P′ and P′{↔ \atop ––}w(aw)^{∗}δ .

Now, it is easy to see that P′{↔ \atop ––}(wa)^{∗}δ, i.e. P′ is itself a terminal cycle. By Lem. 22, it follows that:

(17) TerCycles ⊢ P′ = (wa)^{∗}δ .

Now we reason as follows:

MPA^{s∗} ⊢ P = P + a.P′  (By Lem. 26(1), as P →^{a} P′)
= P + a.(wa)^{∗}δ (17)
=^{S4} P + (aw)^{∗}δ
= P + Q  (16)

This completes the proof for this case.

(c) Case: |P |_{min} > 0 and |Q|_{min} > 0. So far, induction has not played any rôle in the proof of this statement and we have been able to make do with general results about terminal MPA^{s∗}(A) terms. The inductive hypotheses will, however, play a crucial role in the proof of the inductive step for this case. We proceed by a case analysis on the form a term Q with |Q|_{min} > 0 may take.

• Case: Q ≡ Q_{1} + Q_{2}. First of all, note that P {↔ \atop ––}P + Q and Q ≡ Q_{1} + Q_{2} imply that P {↔ \atop ––}P + Q_{1} and P {↔ \atop ––}P + Q_{2}. As |P | + |Q_{i}| < |P | + |Q| for i = 1, 2, we may apply the inductive hypothesis for statement 2 to both these equalities to derive that, for i = 1, 2:

(18)  MPA^{s∗} ⊢ P = P + Q_{i} .

We now argue as follows:

MPA^{s∗} ⊢ P = P + Q_{2}  (18)
= P + Q_{1} + Q_{2} (18)
= P + Q  (Q ≡ Q_{1} + Q_{2})

and we are done.

• Case: Q ≡ a.R. As P {↔ \atop ––}P +Q and P +Q →^{a} R, there exists an MPA^{s∗}(A) term P′ such that P →^{a} P′ and P′{↔ \atop ––}R. We proceed by examining the relationship between the size of P′ and that of P.

– Case: |P′| ≤ |P |. In this case, it follows that |P′| + |R| < |P | + |Q|. Therefore we may apply the inductive hypothesis for statement 3 to the equivalence P′{↔ \atop ––}R to derive that:

MPA^{s∗} ⊢ P′ = R . (19)

We may now simply complete the proof thus:

MPA^{s∗} ⊢ P = P + a.P′ (By Lem. 26(1), as P →^{a} P′)
= P + a.R (19)
= P + Q (Q ≡ a.R)

– Case: |P′| > |P |. We proceed by a case analysis on the form P may take. As P →^{a} P′ and |P′| > |P |, there are only two possible cases to consider, namely P ≡ P_{1} + P_{2} and P ≡ w^{∗}T. We shall examine these in turn.

∗ Case: P ≡ P_{1} + P_{2} →^{a} P′{↔ \atop ––}R.

Assume, without loss of generality, that P_{1} →^{a} P′. Then it is easy

to see that P_{1}{↔ \atop ––}P_{1} + a.R. As |P_{1}| + |aR| < |P | + |aR|, we may

apply the inductive hypothesis for statement 2 to the equivalence P_{1}{↔ \atop ––}P_{1} + a.R to derive that:

MPA^{s∗} ⊢ a.R ⊆ P_{1}

from which it follows immediately that

MPA^{s∗} ⊢ a.R ⊆ P .

∗ Case: P ≡ w^{∗}T →^{a} P′{↔ \atop ––}R.

We proceed by examining the possible form of the transition P ≡ w^{∗}T →^{a} P′. By the operational semantics for MPA^{s∗}(A), there are two possibilities to consider:

· T →^{a} P′, or

· w = aw′ and P′ ≡ w′P, for some w′ ∈ A^{+}. (Note that, as |P′| > |P |, the string w′ cannot be empty.)

We proceed by examing these two possibilities in turn.

· Case: T →^{a} P′.

As T →^{a} P′{↔ \atop ––}R, it follows that T {↔ \atop ––}T + a.R. As |T | + |aR| <

|P | + |aR|, we may apply the inductive hypothesis for statement 2 to the equivalence T {↔ \atop ––}T + a.R to derive that:

MPA^{s∗} ⊢ a.R ⊆ T .

Using the derived equation S6, it follows immediately that

MPA^{s∗} ⊢ a.R ⊆ P .

· Case: w = aw′ and P′ ≡ w′P, for some w′ ∈ A^{+}. In this case, we have that w′ ∈ A^{+}, |P |_{min} > 0, and w′P {↔ \atop ––}R. As |R| < |Q|, we have that |R| + |P | < |Q| + |P |. We may therefore apply the inductive hypothesis for statement 1 to derive that, for some MPA^{s∗}(A) term R′,

P {↔ \atop ––}R′ and MPA^{s∗} ⊢ R = w′R′ and |R′| + length(w′) ≤ |R| .

As |R′| < |R| < |Q|, it follows that |P | + |R′| < |P | + |Q|. We may therefore apply the inductive hypothesis for statement 3 to the equivalence P {↔ \atop ––}R′ to derive that:

MPA^{s∗} ⊢ P = R′ . (20)

We now argue as follows:

MPA^{s∗} ⊢ P = (aw′)^{∗}T  (P ≡ (aw′)^{∗}T)
=^{S7} P + aw′P
= P + aw′R′ (20)
= P + aR  (MPA^{s∗} ⊢ R = w′R′)
= P + Q  (Q ≡ aR)

and we are done. The proof for the case P ≡ (aw)^{∗}T is now complete.

We have now examined all the possible forms that P may take when

P →^{a} P′ and |P′| > |P |.

This completes the proof for the case Q ≡ aR.

• Case: Q ≡ (aw)^{∗}R. First of all, note that, as P {↔ \atop ––}P +Q, it follows that P {↔ \atop ––}P +R. As |P |+|R| < |P | + |Q|, we may apply the inductive hypothesis for statement 2 to the equivalence P {↔ \atop ––}P + R to obtain that:

MPA^{s∗} ⊢ R ⊆ P . (21)

This equality will be used repeatedly in the arguments to follow. As P {↔ \atop ––}P + Q and Q →^{a} wQ, there exists an MPA^{s∗}(A) term P′ such that P →^{a} P′ and P′{↔ \atop ––}wQ. We proceed by considering two cases depending on whether |P′| < |P | or not.

– Case: |P′| < |P |. We proceed by considering two sub-cases, depending on whether w is the empty string or not. We examine these two possibilities in turn.

∗ Case: The string w is empty.

In this case, we have that P′{↔ \atop ––}Q ≡ a^{∗}R. As |P′| < |P |, it follows that |P′| + |Q| < |P | + |Q|. We may therefore apply the inductive hypothesis for statement 3 to the equivalence P′{↔ \atop ––}Q to derive that:

MPA^{s∗} ⊢ P′ = Q . (22)

We may now argue as follows:

MPA^{s∗} ⊢ P = P + aP′  (By Lem. 26(1), as P →^{a} P′)
= P + aQ  (22)
= P + R + aQ (21)
=^{S1} P + Q

and we are done.

∗ Case: w ∈ A^{+}.

In this case, we have that w ∈ A^{+}, P′{↔ \atop ––}wQ and |Q|_{min} > 0. As |P′| + |Q| < |P | + |Q|, we may apply the inductive hypothesis for statement 1 to derive that, for some MPA^{s∗}(A) term P′′,

(23)  P′′{↔ \atop ––}Q  and
(24)  MPA^{s∗} ⊢ P′ = wP′′ and

|P′′| + length(w) ≤ |P′| (25)

By (25) and the fact that |P′| < |P |, it follows that |P′′| < |P |. Therefore |P′′| + |Q| < |P | + |Q|, and we may apply the inductive hypothesis for statement 3 to (23) to derive that:

MPA^{s∗} ⊢ P′′ = Q . (26)

Now we argue that:

MPA^{s∗} ⊢ P = P + aP′  (By Lem. 26(1), as P →^{a} P′)
= P + awP′′  (24)
= P + awQ  (26)
= P + R + awQ (21)
=^{S1} P + Q

and we are done. This completes the proof for the case |P′| < |P |.

– Case: |P′| ≥ |P |. Assume that P →^{a} P′{↔ \atop ––}wQ and |P′| ≥ |P |. We proceed by a case analysis on the form P may take. Because of the constraints for this case, P may only take one of the following two forms:

∗ P ≡ P_{1} + P_{2} or

∗ P ≡ (bv)^{∗}T.

We examine these two cases in turn.

∗ Case: P ≡ P_{1} + P_{2}.

Assume, without loss of generality, that P_{1} →^{a} P′. As |P′| ≥ |P | > |P_{1}|, Lem. 26(2) gives, among other things, the existence of an MPA^{s∗}(A) process P′′ and of a string v ∈ A^{∗} such that:

(27)  P′ ≡ vP′′
(28)  |P′′| ≤ |P_{1}| .

As P′ ≡ vP′′{↔ \atop ––}wQ, |Q|_{min} > 0 and Q ≡ (aw)^{∗}R, by applying

Lem. 28(2) we derive that either:

· v = w and P′′{↔ \atop ––}Q, or

· vu = w and P′′{↔ \atop ––}uQ for some string u ∈ A^{+}. We proceed by examing these two cases in turn.

· Case: v = w and P′′{↔ \atop ––}Q

By (28) and the fact that P ≡ P_{1} + P_{2}, we infer that |P′′| < |P |. Therefore |P′′| + |Q| < |P | + |Q|, and we may apply the inductive hypothesis for statement 3 to the equivalence P′′{↔ \atop ––}Q to derive that: MPA^{s∗} ⊢ P′′ = Q . (29)

We may now argue as follows:

MPA^{s∗} ⊢ P = P + aP′  (By Lem. 26(1), as P →^{a} P′)
= P + awP′′  (v = w and (27))
= P + awQ  (29)
= P + R + awQ (21)
=^{S1} P + Q

and we are done. · Case: vu = w and P′′{↔ \atop ––}uQ for some string u ∈ A^{+}. By (28) and the fact that P ≡ P_{1} + P_{2}, we infer that |P′′| < |P |. Hence it follows that |P′′|+|Q| < |P |+|Q|. Therefore, as u ∈ A^{+}, P′′{↔ \atop ––}uQ and |Q|_{min} > 0, we may apply the inductive hypothesis for statement 1 to derive that, for some MPA^{s∗}(A) term P′′′, the following facts hold:

(30)  P′′′ {↔ \atop ––} Q
(31)  MPA^{s∗} ⊢ P′′ = uP′′′
(32)  |P′′′| + length(u) ≤ |P′′| .

By (32) and |P′′| < |P |, it follows that |P′′′| < |P |. Therefore |P′′′|+|Q| < |P |+|Q|, and we may apply the inductive hypothesis for statement 3 to equivalence (30) to derive that:

MPA^{s∗} ⊢ P′′′ = Q . (33)

Thus,

MPA^{s∗} ⊢ P = P + aP′  (By Lem. 26(1), as P →^{a} P′)
= P + avP′′  (27)
= P + avuP′′′ (31)
= P + awQ  (w = vu and (33))
= P + R + awQ (21)
=^{S1} P + Q

This completes the proof for the case P ≡ P_{1} + P_{2}.

∗ Case: P ≡ (bv)^{∗}T. In this case, we have that P ≡ (bv)^{∗}T →^{a} P′{↔ \atop ––}wQ and |P′| ≥ |P |. We proceed by examing the possible form of the transition P →^{a} P′. By the operational semantics for MPA^{s∗}(A), there are two cases to consider:

· T →^{a} P′, or

· b = a and P′ ≡ vP. We proceed by examining these two cases in turn.

· Case: T →^{a} P′.

As |P′| ≥ |P | > |T |, we may apply Lem. 26(2) to the transition T →^{a} P′ to derive that, among other things, for some string u ∈ A^{∗} and MPA^{s∗}(A) term P′′,

(34)  P′ ≡ uP′′
(35)  |P′′| ≤ |T | .

Since P′ ≡ uP′′{↔ \atop ––}wQ, |Q|_{min} > 0 and Q ≡ (aw)^{∗}R, Lem. 28(2)

gives that either

u = w and P′′{↔ \atop ––}Q, or

w = uu′ and P′′{↔ \atop ––}u′Q for some non-empty string u′ ∈ A^{+}. We proceed by examining these two cases in turn.

Case: u = w and P′′{↔ \atop ––}Q.

By (35) and the form P takes, it follows that |P′′| < |P |. Therefore |P′′| + |Q| < |P | + |Q|, and we may apply the inductive hypothesis for statement 3 to the equivalence P′′{↔ \atop ––}Q to derive that: MPA^{s∗} ⊢ P′′ = Q . (36)

We may now argue as follows:

MPA^{s∗} ⊢ P =^{S6} P + T
= P + T + aP′ (By Lem. 26(2), as T →^{a} P′)
= P + awP′′  (u = w and (34))
= P + awQ  (36)
= P + R + awQ (21)
=^{S1} P + Q

and we are done.

Case: w = uu′ and P′′{↔ \atop ––}u′Q for some non-empty string u′ ∈ A^{+}. By (35) and the form P takes, it follows that |P′′| < |P |. Hence

|P′′| + |Q| < |P | + |Q|. As P′′{↔ \atop ––}u′Q, u′ ∈ A^{+} and |Q|_{min} > 0, we

may therefore apply the inductive hypothesis for statement 1 to derive that, for some MPA^{s∗}(A) term P′′′:

(37)  P′′′ {↔ \atop ––} Q
(38)  MPA^{s∗} ⊢ P′′ = u′P′′′
(39)  |P′′′| + length(u′) ≤ |P′′| .

As |P′′′| < |P′′| < |P |, it follows that |P′′′| + |Q| < |P | + |Q|. We may therefore apply the inductive hypothesis for statement 3 to (37) to infer that: MPA^{s∗} ⊢ P′′′ = Q . (40)

Thus:

MPA^{s∗} ⊢ P =^{S6} P + T
= P + T + aP′ (By Lem. 26(2), as T →^{a} P′)
= P + auP′′  (34)
= P + auu′P′′′ (38)
= P + awQ  (w = uu′ and (40))
= P + R + awQ (21)
=^{S1} P + Q

and we are done. This completes the proof for the case T →^{a} P′. · Case: b = a and P′ ≡ vP. In this case, we have that P ≡ (av)^{∗}T, Q ≡ (aw)^{∗}R, |P |_{min} > 0, |Q|_{min} > 0 and vP {↔ \atop ––}wQ. By Lem. 28(2) and symmetry, it must be the case that v = w and P {↔ \atop ––}Q. By using Lem. 27, we may now derive, because of the form P and Q take, that:

T {↔ \atop ––}R or P {↔ \atop ––}R or T {↔ \atop ––}Q .

In each of the above cases, we may apply the inductive hypothesis for statement 3 and substitutivity to infer that at least one of the following equalities is provable from the theory MPA^{s∗}:

P = Q or (aw)^{∗}P = Q or P = (aw)^{∗}Q .

In each of the above cases we obtain, after possibly applying equation S2, that MPA^{s∗} ⊢ P = Q, from which MPA^{s∗} ⊢ Q ⊆ P follows immediately by A3. This completes the proof for this case.

The proof for the case P ≡ (bv)^{∗}T →^{a} P′ and |P′| ≥ |P | is now complete.

We have therefore examined all the possible cases arising when P →^{a}

P′{↔ \atop ––}wQ and |P′| ≥ |P |.

The proof of the inductive step for statement 2 when Q ≡ (aw)^{∗}R is complete.

We have therefore shown that statement 2 holds for P and Q.

3. Assume that P {↔ \atop ––}Q. Then P {↔ \atop ––}P + Q and Q{↔ \atop ––}Q + P. By statement 2, we infer that MPA^{s∗} ⊢ Q ⊆ P ⊆ Q, from which the thesis follows immediately.

An inspection of the above proof, and the fact that the language of k-bounded terms is closed under transitions by Lem. 8 ensure that if P and Q are k-bounded, then only kbounded equations need be used throughout. The proof of the theorem is now complete.

□

5 Bisimulation Equivalence is not Finitely Axiomatizable over MPA^{s∗}(A)

In the previous section we proved that the equational theory MPA^{s∗} completely characterizes bisimulation equivalence over the language MPA^{s∗}(A). Moreover, we showed that, for each positive integer k, the finite equational theory MPA_{k}^{s∗} gives a sound and complete axiomatization of bisimulation equivalence for terms with iteration bound at most k. This implies that bisimulation equivalence can be finitely axiomatized over MPA^{s∗}(A) terms provided that the length of all loops occurring in terms is bounded from above. The equational theory MPA^{s∗} that axiomatizes bisimulation equivalence over the whole of the language MPA^{s∗}(A) consists, however, of a countably infinite collection of equations. This immediately raises the question of whether one can improve upon our completeness result for MPA^{s∗}(A) by exhibiting a finite equational axiomatization of the relation of bisimulation equivalence over this language. We shall now prove that no such axiomatization can exist, unless the set of actions A is empty. To establish this negative result, we shall show that, if A is non-empty, for every finite collection of sound equations E there is a valid equivalence of the form

(41)  (a^{n})^{∗}δ {↔ \atop ––} (a^{m})^{∗}δ

that cannot be proven to hold from the equations in E. To this end, for every finite equational theory E, we shall find some property which is enjoyed by every equality E = F which is derivable from E, but not by some instance of (41). The reader familiar with [31] might have noticed that terms like those used in (41) play an important rôle in Sewell’s non-finite axiomatizability result for the language BPA_{δ}^{∗} (cf. [31, Thm. 6.6]). The strategy of our proof will, however, be very different from the one used by Sewell in the aforementioned reference.

To obtain the aforementioned negative result, we shall need to introduce a few technical tools which will be useful for our purposes. First of all, we shall prove an important property satisfied by every equation E = F which is sound with respect to {↔ \atop ––}; namely, we shall show that if E{↔ \atop ––}F and the set of actions A is non-empty, then E and F must have exactly the same variables occurring in them.

Definition 30. The set of strings prefixing occurrences of a variable x in a term E ∈ MPA^{s∗}(A, Var), notation Paths(x, E), is defined by structural recursion on terms thus:

Paths(x, δ) =^{△} ∅
Paths(x, y) =^{△} \{ \begin{matrix}\{λ\} & if x = y \\ ∅ & otherwise \end{matrix}
Paths(x, aE) =^{△} {as | s ∈ Paths(x, E)}
Paths(x, E + F) =^{△} Paths(x, E) ∪ Paths(x, F)
Paths(x, w^{∗}E) = Paths(x, E)

The following lemma, which can be easily shown by structural induction on terms, gives all the properties of the sets Paths(x, E) that we shall need for our purposes.

Lemma 31. For every E ∈ MPA^{s∗}(A, Var) and x ∈ Var, the following statements hold:

1. x ∈ Var(E) iff Paths(x, E) ≠ ∅.

2. Let σ be a closed substitution. Assume that s ∈ Paths(x, E) and σ(x) →^{a} P, for some action a ∈ A and P ∈ MPA^{s∗}(A). Then Eσ →^{sa} P.

We are now ready to prove that, if the set of actions A is non-empty, then two terms E and F can only be bisimulation equivalent if their sets of variables are identical.

Lemma 32. If the set of actions A is non-empty, then, for all E, F ∈ MPA^{s∗}(A, Var), E{↔ \atop ––}F implies Var(E) = Var(F).

Proof. We prove the contrapositive statement. Assume, without loss of generality, that there is a variable x ∈ Var(E) − Var(F). Under this assumption, we shall construct a closed substitution σ such that Eσ {↮ \atop ––}F σ. This will prove that E {↮ \atop ––}F.

Let x ∈ Var(E) − Var(F). As x ∈ Var(E), by Lem. 31(1) there exists a string s ∈ A^{∗} such that s ∈ Paths(x, E). Let σ_{δ} be the closed substitution mapping all the variables in Var to δ. By Lem. 9, the closed term F σ_{δ} has finitely many states. As A is non-empty, by Lem. 12 we may therefore find a term P ∈ MPA^{s∗}(A) which is not a state of F σ_{δ} up to bisimulation equivalence, i.e., a term P such that, for no state Q of F σ_{δ}, P {↔ \atop ––}Q. Define now a substitution σ by:

σ =^{△} σ_{δ}[x ↦ aP]

where a ∈ A. We claim that Eσ {↮ \atop ––}F σ. In fact, as s ∈ Paths(x, E) and σ(x) →^{a} P, Lem. 31(2) gives that Eσ →^{sa} P. On the other hand, as x ∉ Var(F), it follows that F σ ≡ F σ_{δ}, and, by construction, no state of F σ_{δ} is bisimulation equivalent to P.

We have therefore shown that E {↮ \atop ––}F, as desired. □

The above result does not hold if the set of actions A is empty. In fact, in that, admittedly pathological, case all the terms in the language MPA^{s∗}(∅) are equivalent to δ, and the equation x = y is sound (and complete) for bisimulation equivalence over that language. It is also interesting to remark that Lem. 32 does not hold in general for trace equivalence and maximal trace equivalence. (The interested reader is invited to consult the encyclopedic reference [16] for information on these equivalences.) For instance, if A = {a}, then it is not too hard to see that the terms a^{∗}(aδ) and a^{∗}(aδ) + P are maximal trace equivalent (and, a fortiori, trace equivalent) for every P ∈ MPA^{s∗}(A). This implies that, if the set of actions A is the singleton {a}, the equation

(42)  a^{∗}(aδ) = a^{∗}(aδ) + x

is sound for maximal trace equivalence. As implied by Lem. 32, equation (42) is, instead, not sound with respect to bisimulation equivalence. For instance, the terms a^{∗}(aδ) and a^{∗}(aδ) + aaδ are not bisimilar.

Definition 33. Let E = {E_{i} = F_{i} | 1 ≤ i ≤ n} (n ∈ ℕ) be a finite equational theory over the signature of MPA^{s∗}(A, Var). The iteration bound of E, notation IB(E), is given by:

IB(E) =^{△} max{IB(E_{i}), IB(F_{i}) | 1 ≤ i ≤ n} .

The following lemma is the key to our promised non-finite axiomatizability result. It states a property that is true of all the equalities that are provable from a finite equational theory E over the signature of MPA^{s∗}(A, Var), but that is not satisfied by all instances of equality (41). Intuitively, the lemma states that two terms E and F whose iteration bound is “large enough” can only be proven equal from the finite theory E iff they have the same iteration bound.

Lemma 34. Let A be a non-empty set of actions, and let E = {E_{i} = F_{i} | 1 ≤ i ≤ n} (n ∈ ℕ) be a sound, finite equational theory over the signature of MPA^{s∗}(A, Var). Let E, F ∈ MPA^{s∗}(A, Var). Assume that E ⊢ E = F. Then the following statements hold:

1. IB(E) > IB(E) iff IB(F) > IB(E);

2. if IB(E) > IB(E) and IB(F) > IB(E), then IB(E) = IB(F).

Proof. Let A be a non-empty set of actions, and let E = {E_{i} = F_{i} | 1 ≤ i ≤ n} (n ∈ ℕ) be a sound, finite equational theory over the signature of MPA^{s∗}(A, Var). Assume that E ⊢ E = F. We prove that both statements of the lemma hold, simultaneously by induction on the depth of the proof of the equality E = F from the theory E. We proceed by a case analysis on the last inference rule used in the proof. We shall give the details of the proof for all the cases, except those in which the equality E = F follows by reflexivity or symmetry. For each of the cases we consider the two statements in turn.

• Case: The equality E = F is proven by instantiating some equation (E_{i} = F_{i}) in the theory E, i.e., E ≡ E_{i}σ and F ≡ F_{i}σ for some equation (E_{i} = F_{i}) ∈ E and substitution σ.

1. First of all, note that, for every G ∈ MPA^{s∗}(A, Var) and substitution τ,

(43) IB(Gτ) = max(IB(G), max{IB(τ(x)) | x ∈ Var(G)}) .

Using the above equality, the claim is immediate from the following chain of logical equivalences:

IB(E) > IB(E) ⇔ IB(E_{i}σ) > IB(E)

(E ≡ E_{i}σ)

⇔ max(IB(E_{i}), max{IB(σ(x)) | x ∈ Var(E_{i})}) > IB(E)

(43)

⇔ max{IB(σ(x)) | x ∈ Var(E_{i})} > IB(E)

(IB(E) ≥ IB(E_{i}))

⇔ max{IB(σ(x)) | x ∈ Var(F_{i})} > IB(E)

(By Lem. 32, as E_{i} = F_{i} is sound)

⇔ max(IB(F_{i}), max{IB(σ(x)) | x ∈ Var(F_{i})}) > IB(E)

(IB(E) ≥ IB(F_{i}))

⇔ IB(F_{i}σ) > IB(E)

(43)

⇔ IB(F) > IB(E)

(F ≡ F_{i}σ)

2. Assume that IB(E) and IB(F) are both strictly larger than IB(E). We show that IB(E) = IB(F). This follows because

IB(E) = max{IB(σ(x)) | x ∈ Var(E_{i})}
(By (43) and IB(E) > IB(E) ≥ IB(E_{i}))
= max{IB(σ(x)) | x ∈ Var(F_{i})}
(By Lem. 32, as E_{i} = F_{i} is sound)
= IB(F)
(By (43) and IB(F) > IB(E) ≥ IB(F_{i}))

• Case: The equality E = F is proven using the transitivity rule, i.e., E ⊢ E = F because, for some G ∈ MPA^{s∗}(A, Var), E ⊢ E = G and E ⊢ G = F by shorter inferences.

1. By applying the inductive hypothesis for statement 1 to E ⊢ E = G and E ⊢ G = F, we derive that:

(44)  IB(E) > IB(E) ⇔ IB(G) > IB(E)
(45)  IB(G) > IB(E) ⇔ IB(F) > IB(E)

from which the claim follows immediately.

2. Assume that IB(E) > IB(E) and IB(F) > IB(E). By (44) and (45), we also have that IB(G) > IB(E). We may therefore apply the inductive hypothesis for statement 2 to the inferences E ⊢ E = G and E ⊢ G = F to derive that IB(E) = IB(G) = IB(F), as desired.

• Case: The equality E = F is proven using the substitutivity rule for action prefixing, i.e., E ⊢ E = F because, for some action a ∈ A and terms E′, F′ ∈ MPA^{s∗}(A, Var), E ≡ aE′, F ≡ aF′ and E ⊢ E′ = F′ by a shorter inference.

Both statements follow immediately by induction and the fact that, for every G ∈ MPA^{s∗}(A, Var), IB(aG) = IB(G).

• Case: The equality E = F is proven using the substitutivity rule for summation, i.e., E ⊢ E = F because, for some terms E′, E′′, F′, F′′ ∈ MPA^{s∗}(A, Var), E ≡ E′ + E′′, F ≡ F′ + F′′ and the equalities (E′ = F′) and (E′′ = F′′) are provable from E by shorter inferences.

1. Note, first of all, that, for all E_{1}, E_{2} ∈ MPA^{s∗}(A, Var),

(46) IB(E_{1} + E_{2}) = max(IB(E_{1}), IB(E_{2})) .

Now we may argue thus:

IB(E) > IB(E) ⇔ IB(E′) > IB(E) or IB(E′′) > IB(E) (46)
⇔ IB(F′) > IB(E) or IB(F′′) > IB(E) (By induction)
⇔ IB(F) > IB(E)  (46)

and we are done.

2. Assume that IB(E) > IB(E) and IB(F) > IB(E). By (46) we may assume, without loss of generality, that IB(E) = IB(E′). By the inductive hypothesis for statement 1, we derive that IB(F′) > IB(E). Therefore, using the inductive hypothesis for statement 2, we may infer that IB(E) = IB(E′) = IB(F′). By (46), the claim will now follow if we prove that

IB(F′′) ≤ IB(F′) .

As, by our assumptions IB(F′) = IB(E) > IB(E), this is immediate if IB(F′′) ≤ IB(E). Otherwise, we have that IB(F′′) > IB(E). By the inductive hypothesis for statement 1, we infer that IB(E′′) > IB(E). We may therefore apply the inductive hypothesis for statement 2 to derive that IB(F′′) = IB(E′′) ≤ IB(E) = IB(E′) = IB(F′), as desired. Hence we have proven that IB(E) = IB(F).

• Case: The equality E = F is proven using the substitutivity rule for string iteration, i.e., E ⊢ E = F because, for some string w ∈ A^{+} and terms E′, F′ ∈ MPA^{s∗}(A, Var), E ≡ w^{∗}E′, F ≡ w^{∗}F′ and the equality (E′ = F′) is provable from E by a shorter inference.

1. Note, first of all, that, for all G ∈ MPA^{s∗}(A, Var),

(47) IB(w^{∗}G) = max(length(w), IB(G)) .

The claim now follows immediately by this fact and the inductive hypothesis for statement 1.

2. Assume that IB(E) > IB(E) and IB(F) > IB(E). We shall prove that IB(E) = IB(F). We proceed by distinguishing two cases depending on whether IB(E′) > IB(E) or not.

– Case: IB(E′) > IB(E). In this case, the inductive hypothesis for statement 1 gives that IB(F′) > IB(E). Therefore we may apply the inductive hypothesis for statement 2 to the inference E ⊢ E′ = F′ to derive that:

IB(E′) = IB(F′) . (48)

The claim now follows from the following chain of equalities:

IB(E) = max(length(w), IB(E′)) (47)
= max(length(w), IB(F′)) (48)
= IB(F)  (47)

– Case: IB(E′) ≤ IB(E). In this case, the inductive hypothesis for statement 1 gives that IB(F′) ≤ IB(E) also holds. The claim now follows because, as IB(E) and IB(F) are strictly greater than IB(E) by the assumptions of the statement, it must be the case that

IB(E) = length(w) = IB(F) .

This completes the proof of the lemma. □

Using Lem. 34, we can finally prove that bisimulation equivalence cannot be finitely axiomatized over MPA^{s∗}(A), unless the set of actions A is empty.

Theorem 35. Assume that the set of actions A is non-empty. Then no finite collection of sound equations over the signature of MPA^{s∗}(A, Var) can be complete for bisimulation equivalence over the language MPA^{s∗}(A).

Proof. Assume that A is a non-empty set of actions. Let E be a finite collection of sound equations over the signature of MPA^{s∗}(A, Var). We exhibit a sound equality P = Q that E cannot prove, thus showing the incompleteness of the theory E.

Let k =^{△} IB(E). Consider the pair of terms P =^{△} (a^{k+1})^{∗}δ and Q =^{△} (a^{k+2})^{∗}δ. It is not hard to see that P {↔ \atop ––}Q. In fact, this follows from Lem. 15 and the fact that MPA^{s∗} ⊢ P = Q by using equation S3 twice. However, by Lem. 34(2), E ⊬ P = Q because IB(P) > k and IB(Q) > k, but IB(P) ≠ IB(Q). □

6 Extensions to BPA_{δϵ}^{s∗}(A)

The results that we have presented so far can be extended to the language BPA_{δϵ}^{s∗}(A), obtained by augmenting BPA_{δ} [4] with the empty process ϵ from [23] and with string

\begin{matrix}a →^{a} ϵ & ϵ →^{✓} δ \\ \frac{P →^{μ} P′}{P + Q →^{μ} P′} & \frac{Q →^{μ} Q′}{P + Q →^{μ} Q′} \\ \frac{P →^{a} P′}{P Q →^{a} P′Q} & \frac{P →^{✓} P′ Q →^{μ} Q′}{P Q →^{μ} Q′} \\ (aw)^{∗}P →^{a} w(aw)^{∗}P & \frac{P →^{μ} P′}{(aw)^{∗}P →^{μ} P′} \end{matrix}

Table 4: The operational rules for BPA_{δϵ}^{s∗}(A) (a ∈ A, μ ∈ A_{✓})

iteration. We shall spare the reader the tedious details of the proofs, and only indicate the extra ingredients needed for the proofs presented so far to go through over this language, when there are any.

The language of BPA_{δϵ}^{s∗}(A, Var) terms is generated by the following grammar:

E ::= a | δ | ϵ | x | E + F | EF | w^{∗}E

where a ∈ A, w ∈ A^{+} and x ∈ Var. The notion of k-bounded term introduced in Sect. 3 applies equally well to terms in the language BPA_{δϵ}^{s∗}(A, Var), and we shall take the liberty of talking about k-bounded BPA_{δϵ}^{s∗}(A, Var) terms in the technical statements of this section. The set of closed terms generated by the above grammar will be denoted by BPA_{δϵ}^{s∗}(A) (P, Q, P′ … ∈ BPA_{δϵ}^{s∗}(A)).

The operational semantics for the language BPA_{δϵ}^{s∗}(A) is given by the labelled transition system

(BPA_{δϵ}^{s∗}(A), A_{✓}, {→^{μ}| μ ∈ A_{✓}})

specified by the Plotkin-style operational rules in Table 4, where A_{✓} =^{△} A ∪ {✓} and ✓ is a fresh action symbol used to denote successful termination. The operational rules in Table 4 are by now completely standard; here we only remark that the operational treatment of sequential composition we adopt is taken from [17]. It is easy to see that whenever the transition P →^{✓} Q can be derived from the rules in Table 4, then Q ≡ δ.

Bisimulation equivalence over BPA_{δϵ}^{s∗}(A), denoted by {↔ \atop ––} with abuse of notation, is defined by extending the notion of bisimulation relation given in Def. 10 with the extra requirement that whenever P ℜ Q and P →^{✓} P′, then Q →^{✓} Q′ for some Q′.

As the rules in Table 4 are in tyft/tyxt-format [17], bisimulation equivalence is a congruence over the language BPA_{δϵ}^{s∗}(A). We shall now show how the results on axiomatizations of bisimulation equivalence presented in the previous sections can be extended to the language BPA_{δϵ}^{s∗}(A).

\begin{matrix}A4 & (x + y)z = xz + yz \\ A5 & (xy)z = x(yz) \\ A7 & δx = δ \\ A8 & xϵ = x \\ A9 & ϵx = x \\ S8 & (w^{∗}x)y = w^{∗}(xy) \end{matrix}

Table 5: The extra axioms for BPA_{δϵ}^{s∗}(A) (w ∈ A^{+})

Let BPA_{δϵ}^{s∗} denote the equational theory obtained by extending the one in Table 2 with the equations in Table 5. Equations A4, A5 and A7–A9 are familiar from the various flavours of the algebra BPA [4] with or without features like the deadlocked process δ and the empty process ϵ. Equation S8 is an instance of law SEI2 from [6]. Versions of this equation dealing with the so-called prefix iteration may be found in [13, 15]. By analogy with our previous terminology, we say that an equation (E = F) in the theory BPA_{δϵ}^{s∗} is k-bounded if both E and F are k-bounded BPA_{δϵ}^{s∗}(A, Var) terms.

Theorem 36. The axiom system BPA_{δϵ}^{s∗} is sound and complete for bisimulation equivalence over the language BPA_{δϵ}^{s∗}(A), i.e. for all BPA_{δϵ}^{s∗}(A) terms P and Q,

P {↔ \atop ––}Q ⇔ BPA_{δϵ}^{s∗} ⊢ P = Q.

Moreover, for k-bounded BPA_{δϵ}^{s∗}(A)-terms P and Q, if P {↔ \atop ––}Q then the equality P = Q can be proved by using only k-bounded equations in the theory BPA_{δϵ}^{s∗}.

Proof. (Sketch) We only give a hint on how the proof of Thm. 29 can be adapted to show the completeness of the theory BPA_{δϵ}^{s∗} for bisimulation equivalence over the language BPA_{δϵ}^{s∗}(A).

First of all, note that it is sufficient to prove completeness of the theory BPA_{δϵ}^{s∗} for bisimulation equivalence over a subset of BPA_{δϵ}^{s∗}(A), namely that of basic terms. A BPA_{δϵ}^{s∗}(A) term is said to be basic iff it can be generated by the following grammar:

P ::= δ | ϵ | aP | P + P | w^{∗}P .

Intuitively, basic terms are BPA_{δϵ}^{s∗}(A) terms in which action prefixing is used in lieu of general sequential composition. A straightforward argument by induction on the size of of BPA_{δϵ}^{s∗}(A) terms shows that, for every BPA_{δϵ}^{s∗}(A) term P, there exists a basic term Q such that

A4,A5,A7–A9,S8 ⊢ P = Q .

This statement justifies our previous claim that it is sufficient to show completeness for basic terms.

The fact that the theory BPA_{δϵ}^{s∗} is complete for bisimulation equivalence over basic terms can be shown by a painstaking reworking of the proof of Thm. 29 for this language.

Here we confine ourselves to remarking that in the reworking of the proof of the inductive step for the statement

P {↔ \atop ––}P + Q implies BPA_{δϵ}^{s∗} ⊢ Q ⊆ P

we make use of the following addition to Lem. 26, which shows how to absorb ✓-labelled transitions:

For all P, P′ ∈ BPA_{δϵ}^{s∗}(A), P →^{✓} P′ implies A3,A4,A9,S1 ⊢ ϵ ⊆ P .
□

As it was the case for the language MPA^{s∗}(A), the above result shows that, for every positive integer k, bisimulation equivalence can be finitely axiomatized over the language of k-bounded BPA_{δϵ}^{s∗}(A) terms. The equational theory BPA_{δϵ}^{s∗} that axiomatizes bisimulation equivalence over the whole of BPA_{δϵ}^{s∗}(A) is, however, infinite. A careful reworking of the proof of Thm. 35 shows that, unless the set of actions A is empty, no finite, complete axiomatization of bisimulation equivalence over BPA_{δϵ}^{s∗}(A) can exist

Theorem 37. Assume that the set of actions A is non-empty. Then no finite collection of sound equations over the signature of BPA_{δϵ}^{s∗}(A, Var) can be complete for bisimulation equivalence over the language BPA_{δϵ}^{s∗}(A).

Acknowledgements: The authors would like to thank Anna Ingólfsdóttir and Vladimiro Sassone for inspiring discussions on the subject of unique root decompositions for finite strings which led to the proof of Thm. 2.

References

[1] L. Aceto and A. Ingólfsdóttir, A complete equational axiomatization for prefix iteration with silent steps, Research Report RS–95–5, BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Department of Mathematics and Computer Science, Aalborg University, Jan. 1995.

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

[3] J. Baeten, J. Bergstra, and J. Klop, Decidability of bisimulation equivalence for processes generating context-free languages, J. Assoc. Comput. Mach., 40 (1993), pp. 653–682.

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

[5] J. Bergstra, I. Bethke, and A. Ponse, Process algebra with combinators, Report P9319, Programming Research Group, University of Amsterdam, Amsterdam, 1993.

[6] , Process algebra with iteration and nesting, Computer Journal, 37 (1994), pp. 243–258.

[7] J. Bergstra and J. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

[8] I. Copi, C. Elgot, and J. Wright, Realization of events by logical nets, J. Assoc. Comput. Mach., 5 (1958), pp. 181–196.

[9] F. Corradini, R. De Nicola, and A. Labella, Fully abstract models for nondeterministic Kleene algebras (extended abstract), 1995. To appear in the Proceedings of CONCUR 95.

[10] R. De Nicola and A. Labella, A completeness theorem for nondeterministic Kleene algebras, in Proceedings of MFCS ’94, vol. 841 of Lecture Notes in Computer Science, Springer-Verlag, 1994.

[11] J. Engelfriet, Determinacy → (observation equivalence = trace equivalence), Theoretical Comput. Sci., 36 (1985), pp. 21–25.

[12] W. Fokkink, A complete equational axiomatization for prefix iteration, Inf. Process. Lett., 52 (1994), pp. 333–337.

[13] , A complete axiomatization for prefix iteration in branching bisimulation, Logic Group Preprint Series 126, Dept. of Philosophy, Utrecht University, Jan. 1995.

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

[15] , A complete equational axiomatization for BPAδϵ with prefix iteration, 1995. Unpublished manuscript.

[16] R. van Glabbeek, The linear time – branching time spectrum, in Proceedings CONCUR 90, Amsterdam, J. Baeten and J. Klop, eds., vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990, pp. 278–297.

[17] J.F. Groote and F. Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation, 100 (1992), pp. 202–260.

[18] M. Hennessy, A term model for synchronous processes, Information and Control, 51 (1981), pp. 58–75.

[19] , Algebraic Theory of Processes, MIT Press, Cambridge, Massachusetts, 1988.

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

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

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

[23] C. Koymans and J. Vrancken, Extending process algebra with the empty process ϵ, Logic Group Preprint Series Nr. 1, CIF, State University of Utrecht, 1985.

[24] L. Lamport, How to write a proof, Research Report 94, Digital Equipment Corporation, Systems Research Center, Feb. 1993.

[25] R. Milner, Calculi for synchrony and asynchrony, Theoretical Comput. Sci., 25 (1983), pp. 267–310.

[26] , A complete inference system for a class of regular behaviours, J. Comput. System Sci., 28 (1984), pp. 439–466.

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

[28] I. Niven and H. Zuckerman, An introduction to the theory of numbers (2nd edition), John Wiley & Sons, 1960.

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

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

[31] P. Sewell, Bisimulation is not finitely (first order) equationally axiomatisable, in Proceedings 9^{th} Annual Symposium on Logic in Computer Science, Paris, France, IEEE Computer Society Press, 1994, pp. 62–70.

Recent Publications in the BRICS Report Series

RS-95-28 Luca Aceto and Jan Friso Groote. A Complete Equational Axiomatization for MPA with String Iteration. May 1995. 39 pp.

RS-95-27 David Janin and Igor Walukiewicz. Automata for the μcalculus and related results. May 1995. 11 pp. To appear in Mathematical Foundations of Computer Science: 20th Int. Symposium, MFCS ’95 Proceedings, LNCS, 1995.

RS-95-26 Faith Fich and Peter Bro Miltersen. Tables should be sorted (on random access machines). May 1995. 11 pp. To appear in Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS, 1995.

RS-95-25 S�ren B. Lassen. Basic Action Theory. May 1995. 47 pp.

RS-95-24 Peter �rb�k. Can you Trust your Data? April 1995. 15 pp. Appears in Mosses, Nielsen, and Schwartzbach, editors, Theory and Practice of Software Development. 6th International Joint Conference CAAP/FASE, TAPSOFT ’95 Proceedings, LNCS 915, 1995, pages 575�590.

RS-95-23 Allan Cheng and Mogens Nielsen. Open Maps (at) Work. April 1995. 33 pp.

RS-95-22 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part II: A Behavioural Semantics and Full Abstractness. April 1995. 33 pp.

RS-95-21 Jesper G. Henriksen, Ole J. L. Jensen, Michael E. J�rgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders B. Sandholm. MONA: Monadic Second-Order Logic in Practice. May 1995. 17 pp.

RS-95-20 Anders Kock. The Constructive Lift Monad. March 1995. 18 pp.

RS-95-19 Franc�ois Laroussinie and Kim G. Larsen. Compositional Model Checking of Real Time Systems. March 1995. 20 pp.

RS-95-18 Allan Cheng. Complexity Results for Model Checking. February 1995. 18pp.