Nested semantics over finite trees are equationally hard.
This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based.
Introduction
Labelled transition systems (LTSs) [23] are a fundamental model of concurrent com-
putation, which is widely used in light of its flexibility and applicability. In particular,
they are the prime model underlying Plotkin's Structural Operational Semantics [30]
and, following Milner's pioneering work on CCS [25], are by now the standard semantic
model for various process description languages.
LTSs model processes by explicitly describing their states and their transitions
from state to state, together with the actions that produced them. Since this view of
process behaviours is very detailed, several notions of behavioural equivalence and
preorder have been proposed for LTSs. The aim of such behavioural semantics is to
identify those (states of) LTSs that afford the same "observations", in some appropriate
technical sense. The lack of consensus on what constitutes an appropriate notion
of observable behaviour for reactive systems has led to a large number of proposals
for behavioural equivalences for concurrent processes. (See the study [14], where van
Glabbeek presents the linear time-branching time spectrum-a lattice of known behavioural
equivalences and preorders over LTSs, ordered by inclusion.)
One of the criteria that has been put forward for studying the mathematical tractability
of the behavioural equivalences in the linear time-branching time spectrum is that
they afford elegant, finite equational axiomatizations over fragments of process algebraic
languages. Equationally based proof systems play an important role in both the
practice and the theory of process algebras. From the point of view of practice, these
proof systems can be used to perform system verifications in a purely syntactic way,
and form the basis of axiomatic verification tools like, e.g., PAM [24]. From the theoretical
point of view, complete axiomatizations of behavioural equivalences capture the
essence of different notions of semantics for processes in terms of a basic collection
of identities, and this often allows one to compare semantics which may have been defined
in very different styles and frameworks. A review of existing complete equational
axiomatizations for many of the behavioural semantics in van Glabbeek's spectrum is
offered in [14]. The equational axiomatizations offered ibidem are over the language
BCCSP, a common fragment of Milner's CCS [25] and Hoare's CSP [20] suitable for
describing finite synchronization trees, and characterize the differences between behavioural
semantics in terms of a few revealing axioms.
The main omissions in this menagerie of equational axiomatizations for the behavioural
semantics in van Glabbeek's spectrum are axiomatizations for 2-nested simulation
semantics and possible futures semantics. The relation of 2-nested simulation
was introduced by Groote and Vaandrager [17] as the coarsest equivalence included in
completed trace equivalence for which the tyft/tyxt format is a congruence format. It
thus characterizes the distinctions amongst processes that can be made by observing
their termination behaviour in program contexts that can be built using a wide array
of operators. (The interested reader is referred to op. cit. for motivation and the basic
theory of 2-nested simulation.) 2-nested simulation can be decided over finite LTSs in
time that is quadratic in their number of transitions [34], and can be characterized by a
single parameterized modal logic formula [26]. However, no equational axiomatization
for it has ever been proposed, even for the language BCCSP. Possible futures seman-
tics, on the other hand, was proposed by Rounds and Brookes in [32] as far back as
1981, and it affords an elegant modal characterization in terms of a subset of Hennessy-
Milner logic-in fact, the modal characterization of possible futures equivalence is a
consequence of a more general, classic result due to Hennessy and Milner (see [18,
Theorem 2.2 and page 148]) that will find application in the technical developments
of this paper. As shown by Kannellakis and Smolka in [22], the problem of deciding
possible futures equivalence and all of the other n-nested trace equivalences (n  1)
from [18] over finite state processes is PSPACE-complete. However, possible futures
equivalence still lacks a purely equational axiomatization over BCCSP.
In this paper, we offer, amongst other results, a mathematical justification for the
lack of an equational axiomatization for the 2-nested simulation and possible futures
equivalence and preorder even for the language of finite synchronization trees. More
precisely, we show that none of these behavioural relations admits a finite (in)equational
axiomatization over the language BCCSP. These negative results hold in a very strong
form. Indeed, we prove that no finite collection of inequations that are sound with respect
to the 2-nested simulation preorder can prove all of the inequalities of the form
a 2m v a 2m
which are sound with respect to the 2-nested simulation preorder. Similarly, we establish
a result to the effect that no finite collection of (in)equations that are sound with respect
to the possible futures preorder or equivalence can be used to derive all of the sound
inequalities of the form
We then generalize these negative results to show that none of the n-nested simulation
or trace preorders and equivalences from [17,18] (for n  2) afford finite equational
axiomatizations over the language BCCSP.
The import of these results is that not only the equational theory of the n-nested
simulation and trace semantics is not finitely equationally axiomatizable, for n  2,
but neither is the collection of (in)equivalences that hold between BCCSP terms over
one action and without occurrences of variables. This state of affairs should be contrasted
with the elegant equational axiomatizations over BCCSP for most of the other
behavioural equivalences in the linear time-branching time spectrum that are reviewed
by van Glabbeek in [14]. Only in the case of additional, more complex operators,
such as iteration or parallel composition, or in the presence of infinite sets of ac-
tions, are these equivalences known to lack a finite equational axiomatization; see, e.g.,
[3,8,11,13,31,33]. Of special relevance for concurrency theory are Moller's results to
the effect that the process algebras CCS and ACP without the auxiliary left merge operator
from [6] do not have a finite equational axiomatization modulo bisimulation equivalence
[27,28]. Fokkink and Luttik have shown in [12] that the process algebra PA [7],
which contains a parallel composition operator based on pure interleaving without communication
and the left merge operator, affords an !-complete axiomatization that is
finite if so is the underlying set of actions. Aceto, -
Esik and Ing-olfsd-ottir [2] proved 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].
As shown in [17,18], the intersection of all of the n-nested simulation or trace
equivalences or preorders over image-finite labelled transition systems, and therefore
over the language BCCSP, is bisimulation equivalence. Hennessy and Milner proved
in [18] that bisimulation equivalence is axiomatized over the language BCCSP by the
four equations in Table 2. Thus, in light of the aforementioned negative results, this
fundamental behavioural equivalence, albeit finitely based over BCCSP, is the intersection
of sequences of relations that do not afford finite equational axiomatizations
themselves. This observation begs the question of whether bisimulation equivalence
over BCCSP is the limit of some sequence of finitely based behavioural equivalences
that have been presented in the literature. In op. cit. Hennessy and Milner introduced an
alternative sequence of relations that approximate bisimulation equivalence. These relations
are based on a "bisimulation-like" matching of the single steps that processes may
perform, whereas the n-nested trace equivalences require matchings of arbitrarily long
sequences of steps. We prove in this study that, unlike the n-nested trace equivalences,
these single-step based approximations of bisimulation equivalence are all finitely axiomatizable
over the language BCCSP, provided that the set of actions is finite.
The paper is organized as follows. We begin by presenting preliminaries on the
language BCCSP, (in)equational logic, and the notions of behavioural equivalence and
preorder studied in this paper (Sect. 2). Our main results on the non-existence of finite
(in)equational axiomatizations for the n-nested simulation and trace equivalence and
preorder (for n  2) are the topic of Sects. 3-5. In Sect. 3 we prove that the 2-nested
simulation preorder has no finite inequational axiomatization over the language BCCSP.
Sect. 4 presents a non-finite axiomatizability result for the possible futures preorder and
equivalence. We then offer a general result to the effect that all of the other n-nested
semantics considered in this study have no finite inequational axiomatization (Sect. 5).
The paper concludes with our proof of finite axiomatizability for the alternative approximations
of bisimulation equivalence introduced by Hennessy and Milner in [18]
(Sect. 6).
The work reported in this paper extends and improves upon the results presented
in [4], where it was shown that 2-nested simulation semantics and the 3-nested simulation
preorder are not finitely based over the language BCCSP. The aforementioned paper
also offered conditional axiomatizations for the nested simulation semantics. Since
we have been unable to obtain similar results for the nested trace semantics, we have
decided to omit those conditional axiomatizations from this presentation.
Preliminaries
We begin by introducing the basic definitions and results on which the technical developments
to follow are based.
2.1 The language BCCSP
The process algebra BCCSP is a basic formalism to express finite process behaviour.
Its syntax consists of (process) terms that are constructed from a countably infinite set
of (process) variables (with typical elements constant 0, a binary operator
called alternative composition, and unary prefixing operators a, where a ranges over
some non-empty set A of atomic actions. We shall use the meta-variables t; u; v to
range over process terms, and write var(t) for the collection of variables occurring in
the term t.
A process term is closed if it does not contain any variables. Closed terms will
be typically denoted by p; q; r. Intuitively, closed terms represent completely specified
finite process behaviours, where 0 does not exhibit any behaviour, p combines the
behaviours of p and q by offering an initial choice as to whether to behave like either
of these two terms, and ap can execute action a to transform into p. This intuition for
the operators of BCCSP is captured, in the style of Plotkin [30], by the transition rules
in

Table

1. These transition rules give rise to transitions between process terms. The
operational semantics for BCCSP is thus given by the labelled transition system [23]
whose states are terms, and whose A-labelled transitions are those that are provable
using the rules in Table 1. Based on this labelled transition system, we shall consider
terms modulo a range of behavioural equivalences that will be introduced in
Sect. 2.4.
A (closed) substitution is a mapping from process variables to (closed) BCCSP
terms. For every term t and (closed) substitution , the (closed) term obtained by re-
Table

1. Transition rules for BCCSP
placing every occurrence of a variable x in t with the (closed) term (x) will be written
(t).
In the remainder of this paper, we let a 0 denote 0, and a m+1 denote a(a m ). Following
standard practice in the literature on CCS and related languages, trailing 0's will
often be omitted from terms. A term over action a is a BCCSP term that may only
contain occurrences of the prefixing operator a. (We shall restrict our attention to these
terms in the technical developments presented in Section 5.) For example, the term a m
is over action a, for each m  0.
2.2 Inequational Logic
An axiom system is a collection of inequations t v u over the language BCCSP. An
inequation p v q is derivable from E, notation E ' p v q, if it can be proven from the
axioms in E using the rules of inequational logic (viz. reflexivity, transitivity, substitution
and closure under BCCSP contexts):
at v au
Without loss of generality one may assume that substitutions happen first in inequa-
tional proofs, i.e., that the third rule may only be used when (t v u) 2 E. In this case
called a substitution instance of an axiom in E.
Equational logic is like inequational logic, but with the extra rule of symmetry:
In equational logic, the formula t v u is normally written t  u. Without loss of
generality, one may assume that applications of symmetry happen first in equational
proofs. Therefore we can see equational logic as a special case of inequational logic,
namely by postulating that for each axiom in E also its symmetric counterpart is present
in E. In the remainder of this paper, we shall always tacitly assume this property of
equational axiom systems.
An example of an (equational) axiom system over the language BCCSP is given in

Table

2. As shown by Hennessy and Milner in [18], that axiom system is sound and
complete for bisimulation equivalence over the language BCCSP.
In the remainder of this paper, process terms are considered modulo associativity
and commutativity of +, and modulo absorption of 0 summands. In other words, we do

Table

2. Axioms for BCCSP
not distinguish t +u and u+ t, nor (t t. This is
justified because all of the behavioural equivalences we consider satisfy axioms A1,
and A4 in Table 2. In what follows, the
axioms A1, A2 and A4. We use a summation
where the empty sum represents 0. It is easy to see that, modulo the equations A1, A2
and A4, every BCCSP term t has the form
j2J a j t j , for some finite index
sets I ; J , terms a j t j (j 2 J) and variables x i (i 2 I). The terms a j t j (j 2 J) and
variables x i (i 2 I) will be referred to as the summands of t.
It is well-known (cf., e.g., Sect. 2 in [15]) that if an (in)equation relating two closed
terms can be proven from an axiom system E, then there is a closed proof for it.
In the proofs of some of our main results, it will be convenient to use a different
formulation of the notion of provability of an (in)equation from a set of axioms. This
we now proceed to define for the sake of clarity.
A context C[ ] is a closed BCCSP term with exactly one occurrence of a hole [
in it. For every context C[ ] and closed term p, we write C[p] for the closed term that
results by placing p in the hole in C[ ]. It is not hard to see that an inequation p v q is
provable from an inequational axiom system E iff there is a sequence
closed substitution , context C[ ] and
pair of terms t; u with t v u an axiom in
In what follows, we shall refer to sequences of the form p 1 v    v p k as inequational
derivations.
For later use, note that, using axioms A1, A2 and A4 in Table 2, every context can
be proven equal either to one of the form C[b([ or to one of the form [
some action b and closed BCCSP term p.
2.3 Traces of BCCSP Terms
The transition relations a naturally compose to determine the possible effects
that performing a sequence of actions may have on a BCCSP term.
Definition 1. For a sequence s = a 1    a k 2 A  (k  0), and BCCSP terms t; t 0 , we
there exists a sequence of transitions
holds for some BCCSP term t 0 , then s is a trace of t. We write traces(t) for
the set of traces of a term t.
The following lemma, whose proof is standard, relates the transitions of a term of the
form (t) to those of t and those of the terms (x), with x a variable occurring in t.
Lemma 1. For every BCCSP term t, substitution , and sequence of actions s, the
following statements hold:
1. if t s ! u for some term u, then (t) s ! (u);
2. if (t) s ! u for some term u, then
(a) either t s
(b) or there are sequences of actions s
and a variable x such that t s1
2.4 Behavioural Semantics
Labelled transition systems describe the operational behaviour of processes in great
detail. In order to abstract from irrelevant information on the way processes compute, a
wealth of notions of behavioural equivalence or approximation have been studied in the
literature on process theory. A systematic investigation of these notions is presented in
[14], where van Glabbeek presents the so-called linear time-branching time spectrum,
a lattice of known behavioural equivalences over labelled transition systems ordered by
inclusion. In this study, we shall investigate a fragment of the notions of equivalence
and preorder from op. cit., together with the family of the nested trace equivalences and
preorders (see Definition 5). These we now proceed to present.
Definition 2. A binary relation R between closed terms is a simulation iff p R q together
with imply that there is a transition q a ! q 0 with p 0 R q 0 .
Groote and Vaandrager introduced in [17] a hierarchy of n-nested simulation preorders
and equivalences for n  2. These are defined thus:
Definition 3. For n  0, we define the relation
!n inductively over closed BCCSP
terms thus:
!0 q for all p; q,
some simulation R with R 1 included in
!n .
The kernel of
!n (i.e., the equivalence
denoted by n .
The relation
!1 is the well-known simulation preorder [29]. The relations
!2 and
2 are the 2-nested simulation preorder and the 2-nested simulation equivalence, re-
spectively. Groote and Vaandrager have characterized 2-nested semantics as the largest
congruence with respect to the tyft/tyxt format of transition rules which is included in
completed trace semantics-see [17] for details.
In the remainder of this paper we shall sometimes use, instead of Definition 3, the
following more descriptive, fixed-point characterization of the n-nested simulation pre-order
(n  1).
Proposition 1. Let p; q be closed BCCSP terms, and n  0. Then p
(1) for all p a there is a q a ! q 0 with
!n p.
Proof. We prove the two implications separately.
Assume that p
q. By definition, p R q with R a simulation and R 1
included in
!n . So if p a
Moreover, since R 1 is included in
!n , it follows that q
!n p.
(1) for all p a there is a q a ! q 0 with
!n p.
Suppose now that p R q. If p a ! p 0 , then by the definition of R we have q a ! q 0
with
we have already proven the 'only if' implication, we may
conclude that p 0 R q 0 . So R is a simulation. Furthermore, by (2) above R 1 is
included in
!n . Hence, we have that p
!n+1 q, which was to be shown.
Example 1. Let m  1. Define, for each n 2 IN, the closed BCCSP terms pn and q n
thus:
By induction on n 2 IN and using Proposition 1, it is not hard to check that pn
and thus that q n
!n+1 pn .
The terms pn and q n (n 2 IN) defined above will play a crucial role in the proof of
Theorem 4 to follow.
Possible futures semantics was introduced by Rounds and Brookes in [32], and is
defined thus:
Definition 4. Let p be a closed BCCSP term. A possible future of p is a pair (s; X),
where s is a sequence of actions and X  A  , such that p s
for some p 0 .
Two closed terms p and q are related by the possible futures preorder (respectively,
possible futures equivalence), written p PF q (resp., p =PF q), if each possible future
of p is also a possible future of q (resp., if p and q have the same possible futures).
The last notions of semantics we shall consider in this paper are the families of the
n-nested trace equivalences and preorders. The n-nested trace equivalences were introduced
by Hennessy and Milner in [18, p. 147] as a a tool to define bisimulation
equivalence [25,29].
Definition 5. For every n  0, the relations of n-nested trace equivalence, denoted by
n , and n-nested trace preorder, denoted by  T
n , are defined inductively over closed
BCCSP terms thus:
0 q for every p; q;
n+1 q iff for every sequence of actions s 2 A  :
there is a q 0 such that q s ! q 0 and
if q s ! q 0 then there is a p 0 such that p s
n+1 q iff for every sequence of actions s 2 A  :
there is a q 0 such that q s ! q 0 and
Note that the relations = T
are just trace equivalence (the equivalence that
equates two terms having the same traces-see [14,19]) and possible futures equiva-
lence, respectively, whereas  T
2 is the possible futures preorder. Moreover, it is easy to
see that, for every n  0, the equivalence
n is the kernel of the preorder  T
n .
The following result is well-known-see, e.g., the references [17,18].
Proposition 2. For every n  0, the relations
n and  T
are preserved by
the operators of BCCSP.
The relations we have previously defined over closed BCCSP terms are extended to
arbitrary BCCSP terms thus:
Definition 6. Let t; u be BCCSP terms, and let  be any of
n and  T
(n  0). The inequation t v u is sound with respect to , written t  u, iff (t)  (u)
for every closed substitution .
For instance, the inequation x v y is sound with respect to all of the 0-nested semantics
defined above. Examples of (in)equations that are sound with respect to
!2 are those
in

Table

2 and
The following result collects some basic properties of nested simulation and nested
trace semantics that will be useful in the technical developments to follow.
Proposition 3. For all BCCSP terms t; u and n  0, the following statements hold:
1. if t
2. if t  T
3. if t
!n u, then t  T
u.
Proof. Statement (1) is due to Groote and Vaandrager in [17], and statement (2) follows
immediately from the definitions of the relations  T
n . We therefore limit
ourselves to presenting a proof of statement (3). To this end, observe, first of all, that in
light of Definition 6, it is sufficient to prove the claim for closed BCCSP terms. Assume
now that p
!n q, where p; q are closed BCCSP terms. We prove p  T
n q by induction
on n. This is trivial if Suppose therefore that p
s be a sequence of
actions in A, and assume that p s We aim at showing that q s ! q 0
for some q 0 with
using Proposition 1 and a simple induction on the
length of s, we have that q s
statement (1) of
the proposition, we may infer that p 0 n q 0 . The inductive hypothesis now yields that
n is the kernel of  T
n , we may conclude that
which was to be shown.
2.5 A Modal Characterization of Nested Trace Equivalence
In the proof of our main result in Sect. 5, we shall make use of the modal characterization
of the n-nested trace equivalences proposed by Hennessy and Milner in [18,
p. 148]. This we now introduce for the sake of completeness.
Definition 7. The set L of Hennessy-Milner formulae over alphabet A is defined by
the following grammar:
The satisfaction relation j= is the binary relation relating closed BCCSP terms and
Hennessy-Milner formulae defined by structural induction on formulae thus:
for every closed BCCSP term p,
it is not the case that p j= ', and
As an immediate consequence of the characterization theorem for bisimulation equivalence
over image-finite labelled transitions systems shown by Hennessy and Milner [18,
Theorem 2.2], two closed BCCSP terms are bisimulation equivalent if, and only if, they
satisfy the same formulae in L. We now introduce a family of sub-languages of L that
yield modal characterizations of the n-nested trace equivalences for every n  0.
Definition 8. For every n  0, we define the set Ln of n-nested Hennessy-Milner
inductively thus:
contains only the formulae > and :>, and
- Ln+1 is given by the following grammar
The following result is due to Hennessy and Milner [18].
Theorem 1. Let p; q be closed BCCSP terms, and let n  0. Then
satisfy the same formulae in the language Ln .
Remark 1. Note that, for every n  0 and closed terms p; q, if each formula in Ln
satisfied by p is also satisfied by q, then p and q satisfy the same formulae in the language
Ln . Indeed, assume that each formula in Ln satisfied by p is also satisfied by q,
and that q satisfies ' 2 Ln . Using the closure of Ln with respect to negation, we have
that q 6j= :', and therefore that p 6j= :'. It follows that p satisfies ', which was to be
shown.
Although tempting, it would therefore be incorrect to assume that, for every n  0
and closed terms p; q, it holds that p  T
each formula in Ln satisfied by p is also
satisfied by q.
To obtain a modal characterization of the n-nested trace preorders, consider the
sub-languages Mn of Ln defined inductively thus:
contains only the formulae > and :>, and
- Mn+1 is given by the following grammar
Following the lines of the proof of Theorem 2.2 in [18], the interested reader will have
little trouble in establishing that
For every n  0 and closed terms p; q, it holds that p  T
each formula in
Mn satisfied by p is also satisfied by q.
2.6 Lengths, Norm and Depth of Terms
We now present some results on the relationships between the lengths of the completed
traces, the depth and the norm of BCCSP terms that are related by the notions of semantics
considered in this paper. These will find important applications in the proofs of
our main results, and shed light on the nature of the identifications made by the nested
simulation and trace semantics.
Definition 9. A sequence s 2 A  is a completed trace of a term t iff t s ! t 0 holds for
some term t 0 without outgoing transitions. We write lengths(t) for the set of lengths of
the completed traces of a BCCSP term t.
Note that lengths(t) is non-empty for each BCCSP term t. Moreover, the only closed
BCCSP term that has a completed trace of length 0 is 0. (Recall that we consider terms
modulo absorption of 0-summands.)
Definition 10. The depth and the norm of a BCCSP term t, denoted by depth(t) and
norm(t), are the lengths of the longest and of the shortest completed trace of t, respectively

The following lemma states the basic relations between the behavioural semantics studied
in this paper and the lengths, depth and norm of terms that will be needed in the
technical developments to follow.
Lemma 2. Let  be any of  T
!n , for n  2. If t  u, then
(a) lengths(t)  lengths(u),
(c) norm(t)  norm(u) and
(d) var
Proof. In light of Proposition 3, it is sufficient to prove that the claims hold for the
possible futures preorder, viz. the relation  TWe argue, first of all, that claims (a)-(c) hold when t  T
u. To this end, note that,
by substituting 0 for the variables in t and u, we obtain closed terms p and q with
suffices to prove claims
(a)-(c) with p and q in place of t and u, respectively. By Definition 6, we have that
Assume now that n 2 lengths(p). Then there are a sequence s 2 A  of length n
and a closed term p 0 with no outgoing transitions such that p s ! p 0 . As p  T
2 q, there
is a closed term q 0 such that q s ! q 0 and
. Recall that p
only if,
have the same traces. It therefore follows that q 0 has no outgoing transitions,
and that n 2 lengths(q), which was to be shown.
(c) follows immediately from (a). To see that claim (b) holds, observe that if
2 q for closed BCCSP terms p and q, then, by Proposition 3(2), p and q have the
same non-empty finite sets of traces, and thus the same longest traces.
To prove claim (d), let t; u be BCCSP terms such that t  T
u. Assume, towards
a contradiction, that there is a variable x that occurs in only one of t and u. We shall
exhibit a closed substitution  such that depth((t)) 6= depth((u)), contradicting
statement (b) of the lemma.
To this end, observe, first of all, that without loss of generality, we may assume that
x occurs in t, say. Let m be a positive integer larger than depth(t). By claim (b) of the
lemma, we have that
Consider now the closed substitution  that maps x to a m , and all the other variables
to 0. Using structural induction, it is a simple matter to prove that
By statement (b) of the lemma, it follows that (t)  T
does not hold, contradicting
our assumption that t  T
Remark 2. Note that
The restriction that n  2 is necessary in the statement of Lemma 2(a) and (c). In
Statements (b) and (d) in Lemma 2 also hold for = T. In fact, it is not hard to see that,
for every t; u, if t  T
1 u then depth(t)  depth(u) and var (t)  var (u).
3 Non-finite Axiomatizability of the 2-nested Simulation Preorder
In this section we prove that the 2-nested simulation preorder is not finitely inequa-
tionally axiomatizable. The following lemma will play a key role in the proof of this
statement.
Lemma 3. If p
!2 a 2m
Proof. The case therefore focus on the case m > 0. We note, first
of all, that if q
!2 a k for some k  0, then, by Lemma 2(a), q has only the completed
trace a k ; clearly, this implies a k
!2 q, and hence a k  2 q.
Consider now a transition p a
!2 a 2m
!2 a 2m 1
or p 0
has depth 2m. So there is at least one transition
!2 a 2m 1 .
If for all transitions p a
!2 a 2m 1 , then it follows that p
!2 a 2m ,
and hence p  2 a 2m . On the other hand, if there exists a transition p a ! p 00 with
that a 2m
!2 p, and hence
The idea behind our proof that the 2-nested simulation preorder is not finitely inequa-
tionally axiomatizable is as follows. Assume a finite inequational axiomatization E for
BCCSP that is sound modulo
!2 . We show that, if m is sufficiently large, then, for all
closed inequational derivations a 2m v
!2 a 2m
we have that p k  2 a 2m . Since a 2m
6
!2 a 2m , it follows that a 2m v a 2m
cannot be derived from E. However, a 2m
!2 a 2m
The following lemma is the crux in the implementation of the aforementioned proof
idea.
Lemma 4. Let t v u be sound modulo
!2 . Let m be greater than the depth of t.
Assume that C[(u)]
!2 a 2m closed substitution . Then C[(t)]  2
a 2m implies C[(u)]  2 a 2m .
Proof. Let C[(t)]  2 a 2m ; we prove C[(u)]  2 a 2m . Since C[(u)]
!2 a 2m +a m ,
it is sufficient to show that a 2m
6
!2 C[(u)]. In fact, if C[(u)]
!2 a 2m
and a 2m
6
!2 C[(u)], by Lemma 3 it follows that C[(u)]  2 a 2m , which is to
be shown. We prove a 2m +a m
6
!2 C[(u)] by distinguishing two cases, depending on
the form of the context C[ ].
Case 1: Suppose C[ ] is of the form C
In this case, we shall prove a 2m
6
!2 C[(u)] by arguing that a m 1
6
holds for each q 0 such that C[(u)] a ! q 0 . To this end, consider a transition
because of the form of the context
C[ ], we may infer that
As (t)
!2 (u) by the soundness of t v u with respect to
!2 , and p 0
by Proposition 2, Lemma 2(b) yields that p 0 and q 0 have the same depth. Since
!2 a 2m 1 . So by Lemma 2(b),
we have that
As depth(a another application of Lemma 2(b) yields that
a
6
Since this holds for all transitions C[(u)] a ! q 0 , and a 2m +a m a using
Proposition 1 we may therefore conclude that a 2m
6
Case 2: Suppose C[ ] is of the form [
In this case, we shall prove a 2m +a m
6
!2 C[(u)] by arguing that norm(C[(u)])
is larger than m.
To this end, observe, first of all, that, as t
!2 u by our assumptions, statements
(b) and (d) in Lemma 2 imply that depth(t) = depth(u), and moreover that t and
contain exactly the same variables. We proceed with the proof by distinguishing
two cases, depending on whether not.
Case
In this case, t has the form
i2I x i for some finite index set I , and variables
sound with respect to
statements (c)-(d) in Lemma 2 yield
that sound with respect to  2 ,
using Proposition 2 we may therefore conclude that
a 2m
6
!2 a 2m  2 C[(t)]  2 C[(u)] ;
which was to be shown.
Case norm((t)) > 0.
Since (t)+r  2 a 2m , Lemma 2(c) yields that norm((t))  2m, and either
norm(r)  2m or By the soundness of t v u with respect to
!2 , and the assumption that norm((t)) > 0, it follows that
Hence (u) 6= 0, and therefore we have that norm((u)) >
As
!2 a 2m using Lemma 2(c), we infer that
Since depth(t) < m and norm((t))  2m, for each variable x
var (u) we have norm((x)) > m.
By the fact that each
completed trace of (u) must become, after less than m transitions, a completed
trace of a (x) with x 2 var(u). Since for all x 2 var
we have norm((x)) > m, it follows that norm((u)) > m. Since moreover
norm(r)  2m or norm(r) = 0, we have norm((u)+r) > m. As a 2m +a m
has norm m, by Lemma 2(a) we may conclude that a 2m
6
which was to be shown.
Remark 3. The inequation
!2 . However, a 4 6 2
. So the proviso in the statement of Lemma 4 that C[(u)]
!2 a 2m
cannot be omitted. (Note that a 4
6
Theorem 2. BCCSP modulo the 2-nested simulation preorder is not finitely inequa-
tionally axiomatizable.
Proof. Let E be a finite inequational axiomatization for BCCSP that is sound modulo
Eg.
By Lemma 4, and using induction on the length of derivations, it follows that if the
closed inequation a 2m v r can be derived from E and r
!2 a 2m +a m , then r  2 a 2m .
As Lemma 2(c) yields that a 2m +a m
6
!2 a 2m , it follows that a 2m v a 2m +a m cannot
be derived from E. Since a 2m
!2 a 2m may conclude that E is not complete
modulo
4 Possible Future Semantics is not Finitely Based
Throughout this section, we let  be either the possible futures preorder, or possible
futures equivalence. Our order of business in this section will be to prove that  has
no finite (in)equational axiomatization over BCCSP. The idea behind the proof of this
claim is as follows. Assume that E is a finite inequational axiomatization for BCCSP
that is sound modulo . We show that, if m is sufficiently large, then, for all closed
inequations p v q that can be derived from E the following invariant property holds:
If lengths(q)  fm+ 1g, and there is a p 0 such that p a
then there is a q 0 such that q a ! q 0 ,
However, we shall exhibit a pair of closed terms that are related by , and do not satisfy
the above property. This will allow us to conclude that E is not complete with respect
to .
The following lemma characterizes some properties of the inequations that are
sound with respect to  that will be useful in the proof of the main result of this section
(Theorem 3 to follow).
Lemma 5. Let the axiom t v u be sound modulo . Let
x be a variable. Then
(a) fy
(b) for each there is an ' 2 L such that a
and
Proof. Let t v u be sound modulo , and let x be a variable. We prove the two statements
of the lemma separately.
- Proof of Claim (a): Assume, towards a contradiction, that the variable x is contained
in fx but not in fy k j k 2 Kg. We shall exhibit a closed substitution
such that (t) 6 (u), contradicting our assumption that t v u is sound modulo
.
To this end, pick a positive integer m > depth(t). Since t v u is sound modulo ,
by Lemma 2(b) we have that m > depth(u) also holds. Consider the closed substitution
that maps x to a m , and all the other variables to 0. Since
I , we have that m 2 lengths((t)). On the other hand, m 62 lengths((u))
because, as x is not contained in fy k j k 2 Kg, every completed trace of (u) is
either one of u itself (and is thus shorter than m) or has a m has a proper suffix (and
is thus longer than m). By Lemma 2(a), it follows that (t)  (u) does not hold,
contradicting our assumption that t v u is sound modulo .
- Proof of Claim (b): Assume, towards a contradiction, that there is a j 2 J with
for each ' 2 L with a
We shall exhibit a closed substitution  such that (t) 6 T(u), contradicting our assumption that t v u is sound modulo .
Let m be a positive integer larger than depth(t). Since t v u is sound modulo
, by Lemma 2(b) we have that m > depth(u) also holds. Consider the closed
substitution mapping x to a m , all of the variables not occurring in t j to a 2m , and
all the other variables to 0. Note that (t)
a j
1. Moreover, since
it is easy to see that
We claim that if (u)
a j
This shows that
can have the same traces as
(see Remark 2), contradicting our assumption that t v u is sound modulo .
To prove our claim, we consider the possible origins of a transition (u)
a j
p.
Case 1: (u) a j
a j
K. In this case, by
the definition of , we have that depth(p) 2 fm 1g. By (1), we may
infer that depth((t j )) 6= depth(p), as claimed.
Case 2: (u) a j
such that a
and either x 62 var In this case, by the definition
of  and using that depth(u) < m, we have that depth(p) is either smaller
than larger than 2m 1
(if Again, by (1), we may infer that depth((t j
depth(p), as claimed.
This completes the proof.
We are now in a position to prove the promised result to the effect that possible futures
semantics is not finitely based over the language BCCSP.
Theorem 3. BCCSP modulo  is not finitely inequationally axiomatizable.
Proof. Let E be a finite equational axiomatization for BCCSP that is sound modulo .
Eg.
We have that
because both processes have the same possible futures. Nevertheless,
This follows immediately from the following
Claim. Assume that 1g, and there is
a p 0 such that p a 2m. Then there is a q 0 such
that q a
Proof of the claim. Using induction on the length of inequational derivations, the soundness
of E with respect to  and Lemma 2(a), it suffices to consider the case that
closed substitution ,
and an axiom We proceed by distinguishing two sub-cases, depending on
the form of the context C[ ].
Case 1: Suppose C[ ] is of the form C
be as in the statement of the claim. Then
and, because of the form of the context C[ ], we may infer that
By the soundness of E and the fact that  is preserved by the operators of BCCSP
(Proposition 2), we have that p 0  q 0 . Therefore norm(q 0
both hold by statements (b) and (c) in Lemma 2. As
and we are done.
Case 2: Suppose C[ ] is of the form [
Consider a transition
as in the statement of the claim. We distinguish three possible
cases, depending on the origin of this transition.
Case 2.1: Assume that r a ! p 0 . Then q a ! p 0 and we are done.
Case 2.2: Assume that I . By Lemma 5(a) and the
soundness of t v u with respect to , we have that x
It follows that q a ! p 0 , and we are done.
Case 2.3: Assume that p As norm((t j
there must be a variable x m. By
statement (b) in Lemma 5, there is an ' 2 L such that
have that
Considering that
and thus lengths(q 0 )  fm; 2m; 3mg, it must be the case that norm(q 0
As depth((t j ))  2m by assumption, it follows that depth((y))  2m
for each y 2 holds for each y 2
As depth(u ' ) < depth(u) < m, this implies that depth((u '
3m. Considering that lengths(q 0 )  fm; 2m; 3mg, we may conclude that
To sum up, we have proven that, also in this case, q a
and depth(q 0 )  2m, which was to be shown. 2
Nested Semantics is Finitely Based
We now proceed to offer results to the effect that the language BCCSP
n or
n , for n  2, or  T
n or
!n , for n  3, is not finitely equationally axiomatizable.
Rather than considering each of these behavioural relations in turn, we offer a general
proof of non-finite axiomatizability that applies to all of them at once. The general
strategy underlying such a proof is as follows. We prove that, for each n  2, no
finite collection of (in)equations that is sound with respect to = T
coarsest relation
n+1 and
!n+1 ) can prove all of the closed inequations of the form
action a, that are sound with respect to
(the finest relation amongst = T
n+1 and
In the proof of this result, we shall make use of the modal characterization of the
given in Theorem 1. More specifically, we shall show that, for each n  2
and finite axiom system E that is sound with respect to = T
n , there is a formula n in the
language Ln+1 (see Definition 8) such that whenever E proves a closed inequation p v
q, with p and q BCCSP terms over action a, then, subject to some technical conditions
on the lengths of the completed traces of q, it holds that p satisfies n if, and only if,
so does q. We shall, however, show that this property does not hold for the inequation
!n+1 pn , where the terms pn and q n have been defined in Example 1. This will
allow us to conclude that the sound inequation q n v pn cannot be derived from E, and
thus that E is incomplete
n+1 and
!n+1 .
The technical implementation of the above idea will be based upon an induction
on the length of the proof of closed inequations from the finite axiom system E. The
crucial step in this proof will be to show that, subject to technical conditions, the afore-mentioned
formula n is satisfied either by both terms in a substitution instance of an
axiom in E or by neither of them. This case will be tackled by Lemma 11 to follow. We
now introduce some technical notions, and preliminary results, that will be used in the
proof of this crucial lemma.
Definition 11. We call a substitution  substantial if depth((x)) > 0 for all variables
x.
For reasons of technical convenience, in the proofs of our non-finite axiomatizability
results presented in this section we will only allow for the use of closed substantial substitutions
in the rule of substitution. This does not limit the generality of those results
because every finite inequational axiomatization E can be converted into a finite inequa-
tional axiomatization E 0 such that the closed substitution instances of the axioms of
are the same as the closed substantial substitution instances of the axioms of
equating any closed subterm of depth 0 with 0). This is done by including in E 0 any
inequation that can be obtained from an inequation in E by replacing all occurrences of
any number of variables by 0.
Definition 12. Define the depths at which a subterm occurs in a BCCSP term as follows

t occurs in t at depth 0,
if v occurs in t or u at depth d, then v occurs in t + u at depth d,
if v occurs in t at depth d then v occurs in at (with a 2 A) at depth d + 1.
A BCCSP term t has a unique depth allocation if no variable occurs in t at two different
depths.
For example, the term does not have a unique depth allocation, as the variable
x occurs both at depth 0 and at depth 1 in it, but does.
The following lemma describes the interplay between the depths at which variables
occur in a term t, and the lengths of terms of the form (t), for some substantial substitution
.
Lemma 6. For every BCCSP term t and d  0, the following statements hold:
1. The term v occurs in t at depth d if, and only if, there are a term u and a sequence
of actions s of length d such that t s
2. Let x be a variable, and let  be a substitution. For every n > 0, if x occurs in t at
depth d and n 2 lengths((x)) then d
Proof. We prove the two statements separately. Recall that we consider equality of
terms modulo axioms A1, A2 and A4 in Table 2.
- Proof of statement 1. We show the two implications separately.
By induction on the definition of the depths at which v occurs in t.
Assume that v occurs in t at depth d because
letting " denote the empty string, we have that
and we are done.
Assume that v occurs in t at depth d because v occurs in t or t 0 at
depth d. Suppose, without loss of generality, that v occurs in t at depth d.
By induction, we have that there are a term u and a sequence of actions s
of length d such that t s u. If d is positive, we may immediately
conclude that t It follows that
and we are done.
Assume that v occurs in at (with a 2 A) at depth d+1 because v occurs in
t at depth d. By induction we have that there are a term u and a sequence
of actions s of length d such that t s ! v +u. It follows that at as ! v +u,
and we are done.
(() Assume that there are a term u and a sequence of actions s of length d
such that t s We prove that v occurs in t at depth d by induction on
d. Throughout the proof, we let
Base Case: u, we have that
i2I
This means that
I and J 0  J .
occurs in v at depth 0 by the first clause of Definition 12, using the
second clause of Definition 12 we may conclude that v occurs in t at depth
Inductive Step: d > 0. Since
i2I
and s is non-empty, we have that
occurs in t j at depth d 1, and therefore in a j t j at
depth d. Using the second clause of Definition 12 we may conclude that v
occurs in t at depth d.
- Proof of statement 2. Assume that x occurs in t at depth d, n 2 lengths((x)) for
some substitution , and n is positive. Since x occurs in t at depth d, by statement 1
of the lemma, we have that t s some sequence of actions s of length d
and term u. By Lemma 1, we have that
As n 2 lengths((x)) by our assumptions, (x) s 0
sequence of
actions s 0 of length n and term v with no outgoing transitions. Since the length of
s 0 is positive, it follows that (t) ss 0
thus that d+n 2 lengths((t)),
which was to be shown.
Lemma 7. Let t be a BCCSP term with depth(t) < m, and let  be a closed substantial
substitution such that lengths((t))  fn
a unique depth allocation.
Proof. Suppose a variable x occurs at depths d 1 and d 2 in t. Let
Since  is a substantial substitution, d is positive. Then, by Lemma 6(2) and the proviso
of Lemma 7, we have that
(The proof of the first inclusion uses that d > 0.) As jd 1 d 2 j < m holds by our
assumption that depth(t) < m and Lemma 6(1), this implies d
The proof above is the only one where we use that the substitutions are substantial.
Definition 13. For m; '  0, define the operator ; ma ' on closed BCCSP terms recursively
by
Recall that we consider terms modulo associativity and commutativity of +, and modulo
absorption of 0 summands. Hence any closed BCCSP term with depth 0 can be written
as 0. Thus, the operator ; ma ' adds a sequence of ' a-transitions to every state at depth
m from which no transitions are possible.
In the remainder of this section, we shall tacitly assume, without loss of generality,
that a is the only action occurring in terms. This is justified because the closed terms
that we shall use in our proof of Theorem 4 to follow are over action a, and it is easy to
see that every closed inequational derivation from an axiom system that is sound with
respect to  T
1 proving an inequation p v q, with p and q terms over action a, only uses
terms over action a.
Lemma 8. Let p be a closed BCCSP term, and let '; m;n  0. If depth(p) < n+m+'
then
Proof. Note, first of all, that the following holds, for each k 2 IN and closed BCCSP
9q (p a
We prove the lemma by induction on n +m.
(as p is over action a)
(because depth(p) <
where the second equivalence follows by (2) and the inductive hypothesis, using
that
where the second equivalence follows by (2) and the inductive hypothesis, using
that
The following example shows that in Lemma 8 the hypothesis depth(p) < n +m+ '
cannot be omitted.
Example 2. If ' > 0, then a m+' 6j= hai m :hai>. On the other hand,
a
Lemma 9. Let  be a closed substitution, and let t be a BCCSP term with a unique
depth allocation and depth(t) < k. Let  0 be a closed substitution with  0
occurs at depth d in t. Then
Proof. We apply induction on k.
Base Case: base case is vacuous, since there is no term whose depth is
smaller than 0.
Inductive Step: k > 0. We begin by proving that  0 for each summand
v of t.
Consider a summand x of t. Since x occurs at depth 0 in t, the definition of  0
yields that  0
Consider a summand au of t. Since  0 variables y that
occur at depth e in u, and depth(u) < k 1, by induction we may infer that
Hence  0
holds for all summands v of t, it follows that  0
which was to be shown. 2
Remark 4. The assumption that depth(t) be smaller than k in the statement of the
above lemma is necessary. Take, for instance,
if ' is positive,
Note that depth(t) = 1.
Lemma 10. Let  be a closed substitution, and let t be a BCCSP term with a unique
depth allocation, depth(t) < n+m and depth((t)) < n+m+', for some '; m;n  0.
Let  0 be a closed substitution with  0 occurs at depth
d in t. Then
Proof. Since depth(t) < yields that  0
now follows directly from Lemma 8.
Note that the formula (hai:) n hai m+' > is contained in the language Ln+1 that gives a
modal characterization of the equivalence = T
n+1 . (See Definition 8 and Theorem 1.)
The following lemma will be a key ingredient in the proof of Theorem 4 to follow.
As mentioned previously, it will be used to show that, subject to technical conditions,
terms related by closed substantial substitution instances of axioms in a finite axiom
system that is sound for (n 1)-nested trace equivalence, for n  1, either both satisfy
an appropriately chosen formula in the language Ln+2 or none of them does.
be a pair of BCCSP terms with depth(t i ) < m, for
such that the equation t 1  t 2 is sound for (n 1)-nested trace equivalence, for some
Furthermore, let  be a closed substantial substitution with lengths((t i
2. Then
Proof. Since lengths((t i we have that
also holds. Thus, by Lemma 7, the term has a unique depth allocation. Let  0 be
a closed substitution with  0 occurs at depth d in
for the vertical arrows, and the soundness
of
n+1 and the modal characterization of = T
(Theorem 1) for the
horizontal one, we obtain
This completes the proof of the lemma.
After this sequence of preparatory lemmas, we are now ready to prove the promised
result to the effect that none of the n-nested simulation and trace equivalences (for
2), and none of the n-nested simulation and trace preorders (for n  are finitely
based over BCCSP.
Theorem 4. BCCSP
n or n , for n  2, or  T
n or
!n , for n  3, is not
finitely equationally axiomatizable.
Proof. Let E be a finite inequational axiomatization for BCCSP. Pick a positive integer
m such that
Let pn and q n be defined, for each n 2 IN, as in Example 1. For ease of reference, we
recall that:
As argued in Example 1, for every n  1, we have that pn
!n q n , and thus
. Note that the formula n is contained
in Ln+1 , for each n  1, and that n+1 is the formula mentioned in the statement of
Lemma 11. By induction on n  1 one checks that pn
We now proceed to use the fact that pn to argue that the
inequation q n v pn cannot be proven from any finite set of equations that is sound for
. To this end, suppose that E is sound
(which, by Proposition 3, is certainly
the case if E is sound for n ,  T
n+1 or
2. We show that E is
incomplete for
(and thus certainly
n+1 by Proposition 3),
This follows immediately from the following:
Claim. Assume that E ' p v q and lengths(q)  fn +m
In fact, using this claim, we can show that E
first of
all, that lengths(p n ) is included in fn+m 1; n+ 2m 1g, for each n 2 IN. (In fact,
for each n  1.) We have already observed
that pn . Thus, by the above claim, the inequation q n v pn cannot
be derived from E.
Proof of the claim. We use induction on the length of the derivation of p v q from
E. The cases of reflexivity and transitivity are trivial, using the soundness of E with
respect
n and that, by Lemma 2(a),
for each n  2. The case that p v q is a closed substantial substitution instance of
an axiom in E has been dealt with by Lemma 11. What remains to consider is closure
under contexts: if the claim holds for p v q it needs to be shown for
every closed BCCSP term r over action a, and for ap v aq. The first of these follows
trivially by the observation that
For the second, the soundness of E yields
q. Using the modal characterization of
n , and that n 1 is contained in Ln , we have that
ap
which was to be shown.
Remark 5. If E contains the axiom which is sound for
!2 , we have that
the proof
above, and the claim in particular, does not apply to  T
2 and
!2 .
Indeed, three different proofs appear to be needed to establish all of our non-finite ax-
iomatizability results. In particular, the proofs of non-finite axiomatizability for the possible
futures and 2-nested simulation preorders are necessarily distinct, because if the
set of actions A is a singleton, then there is a finite axiom system that is sound for the
possible futures preorder and complete for the 2-nested simulation preorder. This we
now proceed to show.
Assume that a is the only action, and consider the axiom system EPF that contains
the equations in Table 2, and the inequation
ay
It is not too hard to see that EPF is sound for the possible futures preorder. In fact, for
all closed BCCSP terms p; q,
- the terms a(p have the same traces, and
- if a is the only action, then p + q has the same set of traces as either p or q.
It follows that equation (3) is sound with respect to the possible futures preorder, if a is
the only action.
We shall now show that EPF is complete for the 2-nested simulation preorder over
the collection of closed BCCSP terms over action a. The following lemma will play a
role in the proof of this result.
Lemma 12. Let p; q be closed BCCSP terms over action a. Assume that depth(p)
depth(q). Then
Proof. By induction on the sum of the "sizes" of the closed BCCSP terms p; q. We
proceed by a case analysis on the form p may take.
In this case, EPF ' q  q immediately from axiom A4 in

Table

2.
Assume that
finite index set
J and closed terms q j over action a (j 2 J ). Since depth(p)  depth(q) by our
assumptions, there is an index j 2 J such that depth(p 0 )  depth(q j ). By the
inductive hypothesis, we have that
Hence,
The claim now follows using closure with respect to BCCSP contexts.
different from 0. Since depth(p)  depth(q)
by our assumptions, we have depth(p i )  depth(q) for 2. By the inductive
hypothesis, we may infer that
2. Thus,
which was to be shown.
We are now ready to prove that the axiom system EPF is complete for the 2-nested
simulation preorder over closed BCCSP terms over action a.
Theorem 5. Let p; q be closed BCCSP terms over action a. Assume that p
!2 q. Then
Proof. We prove the claim by induction on the depth of p. Let
i2I ap i and
finite index sets I and J and closed terms p i (i 2 I) and
action a. Note that, as p
!2 q, the depth of q is equal to that of p
(Lemma 2(b)).
I . Then, since p
!2 q, there is an index j i such that p i
(Propo-
sition 1). Since the depth of p i is smaller than that of p, by our inductive hypothesis it
follows that the inequation
can be proven from EPF . Since this holds for each
I , we have that
i2I
To conclude the proof, it suffices only to show that
i2I
To this end, note that, since EPF is sound with respect to the possible futures preorder,
and the inequation p v
is derivable from it, the terms p and
have
the same depth (Lemma 2(b)). As previously observed, p and q also have the same
depth. Write now
i2I
where r is the sum of all the summands of q not occurring in
. By the previous
observations, we have that
i2I
Lemma 12 now yields that
i2I
i2I
completing the proof.
6 Finitely Based Approximations of Bisimulation Equivalence
The results presented in the previous sections show that none of the nested simulation
and trace equivalences afford finite equational axiomatizations over the language
BCCSP, even in the presence of a singleton action set. The only exceptions to this
rule are the 0-nested and 1-nested simulation and trace equivalences, which happen
to be the universal relation, simulation and trace equivalence. Interestingly, however,
as shown in [17,18], the intersection of all of the n-nested simulation or trace equivalences
or preorders over image-finite labelled transition systems, and therefore over the
language BCCSP, is bisimulation equivalence. Hennessy and Milner proved in [18] that
bisimulation equivalence is axiomatized over the language BCCSP by the equations in

Table

2. It follows that this fundamental behavioural equivalence, albeit finitely based
over BCCSP, is the limit of sequences of relations that do not afford finite equational
axiomatizations themselves. This is by no means the only example from process theory
of a "discontinuous" property of a behavioural equivalence-i.e., of a property that
"appears at the limit", but is not afforded by its finite approximations. Other examples
of this phenomenon may be found in, e.g., the study of decidability properties of behavioural
equivalences over classes of infinite state processes. For instance, as shown
in [5,9,10], bisimulation equivalence is decidable over the languages BPA and BPP, but
none of the other notions of behavioural equivalence in the linear time-branching time
spectrum is-see, e.g., the references [16,21].
It is a natural question to ask at this point whether bisimulation equivalence over
BCCSP is the limit of some sequence of finitely based behavioural equivalences that
have been presented in the literature. We shall now argue that this does hold, provided
that the set of actions is finite.
As stated in Sect. 2.4, the n-nested trace equivalences were introduced in [18,
p. 147] as a a tool to define bisimulation equivalence [25,29]. In op. cit. Hennessy and
Milner introduced another sequence of relations that approximate bisimulation equiva-
lence. These were defined thus:
Definition 14. For every n  0, the relations = A
are defined inductively over closed
BCCSP terms thus:
0 q for every p; q;
n+1 q iff for every action a 2 A:
there is a q 0 such that q a ! q 0 and
if q a ! q 0 then there is a p 0 such that p a
Note that, unlike the n-nested trace
n , the relations = A
n explore the behaviour
of BCCSP terms only up to "depth n". As shown by Hennessy and Milner,
over image-finite labelled transition systems, bisimulation equivalence is the intersection
of all of the relations = A
n . Moreover, each of the = A
n is preserved by the operators
of Milner's CCS, and a fortiori by those of BCCSP.
Our order of business will now be to offer a complete axiomatization of the relations
closed BCCSP terms. Let Ax denote the axiom system in Table 2. We shall
now show how to inductively construct a family of axiom systems En , for n  0, with
the following property:
Theorem 6. Let p; q be closed BCCSP terms. Then
The axiom systems En , for n  0, will be finite, if so is the set of actions A. In what
follows we assume that the set of variables is fx
Definition 15. For each n  0, we define the axiom system En thus:
and
Note that, if A is a finite set set containing, say, k actions, then the axiom system En
contains k n equations, for each n  0. Moreover, observe for later use that, for each
0, the axioms in En only use variables x
We shall now show that Theorem 6 does hold for the previously defined axiom
systems En . Since the soundness of each of the axioms in En can easily be shown by
induction on n, using the aforementioned congruence properties of the relations = A
we shall limit ourselves to presenting a proof of the completeness of Ax [ En with
respect to = A
closed BCCSP terms. The following lemma will be useful in such a
proof.
Lemma 13. Let n  0, and let p; q be closed BCCSP terms. Assume that Ax [ En '
for each action a 2 A.
Proof. Assume that Ax [ En ' p  q, for some closed BCCSP terms p; q. Recall that
this means that there is a sequence p 1
closed substitution , context C[ ] and
pair of terms t; u with t  u or u  t an axiom in Ax [ En (1  i < k).
We prove that Ax [ En+1 ' ap  aq, for each action a 2 A, by induction on k.
Base Case: 1. In this case we have that q. Thus the equation p  q is
provable from Ax , and so is ap  aq.
Inductive Step: k > 1. By the inductive hypothesis, the equation ap  ap k 1 is
provable from the axiom system Ax [ En+1 . Since ap to complete the
proof, we are therefore left to prove that
To this end, recall that
for some closed substitution , context C[ ] and pair of terms t; u with t  u or
an axiom in Ax [En . In case an axiom from Ax or its symmetric counterpart
was used, (4) follows immediately from the rule of closure under BCCSP contexts.
The proof for the case when t  u is an axiom in En proceeds by a case analysis
on the form of the context C[ ].
Case 1: Suppose C[ ] is of the form C action b and closed
term r.
In this case, it is sufficient to show that
as (4) will then follow by applying the rule of closure under BCCSP contexts
repeatedly.
To this end, let  0 be the closed substitution that maps variable xn+3 to r, and
acts like  on all of the other variables. Using the axioms in Ax [ En+1 , we
have that
which was to be shown.
Case 2: Suppose C[ ] is of the form [ for some closed term r.
In this case, letting  0 be defined as above, and using the axioms in Ax [En+1 ,
we have that
which was to be shown.
The remaining case, viz. when u  t an axiom in En , is similar.
We are now ready to establish the completeness of Ax [ En with respect to = A
closed BCCSP terms, for each n  0.
The proof is by induction on n. The base case is trivial since the equation x 1  x 2
can be used to prove every (closed) equation.
For the inductive step, assume that Ax [ En is complete with respect to = A
closed BCCSP terms, and that
n+1 q holds for closed terms p; q. We shall now
argue that the equation p  q can be derived from the axiom system Ax [ En+1 . Let
i2I a i p i and
finite index sets I and J and closed terms
a Our order of business will now be to show that
By symmetry, it is sufficient to show that the equation is derivable from
. To this end, let i 2 I . Then, since
n+1 q, there is an index j i such that
a
and
. Since the axiom system Ax[En is complete with respect to = A
by our inductive hypothesis, it follows that the equation
can be proven from
Ax [En . By Lemma 13, the equation a
can be derived from Ax [En+1 . As
this holds for each index i 2 I , it follows that p + q  q is derivable from Ax [ En+1 ,
which was to be shown.
The proof of Theorem 6 is now complete.

Acknowledgments

The work reported in this paper was partly carried out while Luca
Aceto was an invited professor at Reykjav-k University, Rob van Glabbeek was visiting
researcher at CWI and associate professor at the National ICT Australia, and Anna
Ing-olfsd-ottir was at Iceland Genomics Corporation. They thank these institutions for
their hospitality and the excellent working conditions. Luca Aceto is grateful to Sverrir
Thorvaldsson and his group at deCODE Genetics for their logistic support during the
final stages in the preparation of this paper.



--R





Decidability of bisimulation equivalence for processes generating context-free languages
Fixed point semantics in process algebras

On the axiomatizability of ready traces
Bisimulation equivalence is decidable for basic parallel processes

Mathematics Series (R.
An omega-complete equational specification of interleaving
The equational theory of pomsets
GLABBEEK, The linear time-branching time spectrum I
A new strategy for proving

Structured operational semantics and bisimulation as a congruence
Algebraic laws for nondeterminism and concurrency
in On the construction of programs - an advanced course

three problems of equivalence
Formal verification of parallel programs
An interactive proof tool for process algebras
Communication and Concurrency
Modal observation equivalence of processes
The importance of the left merge operator in process algebras

Concurrency and automata on infinite sequences
A structural approach to operational semantics
On defining relations for the algebra of regular events
in 22 nd Annual Symposium on Foundations of Computer Science
Nonaxiomatisability of equivalences over
III AND R.
--TR
Algebraic laws for nondeterminism and concurrency
Communicating sequential processes
The equational theory of pomsets
CCS expressions finite state processes, and three problems of equivalence
A new strategy for proving MYAMPERSANDohgr;-completeness applied to process algebra
Structured operational semantics and bisimulation as a congruence
Decidability of bisimulation equivalence for process generating context-free languages
Undecidable equivalences for basic process algebra
Bisimulation equivalence is decidable for all context-free processes
Formal verification of parallel programs
Communication and Concurrency
Undecidable Equivalences for Basic Parallel Processes
The Importance of the Left Merge Operator in Process Algebras
An omega-Complete Equational Specification of Interleaving
An Interactive Proof Tool for Process Algebras
On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers
2-Nested Simulation Is Not Finitely Equationally Axiomatizable
Bisimulation Equivalence is Decidable for Basic Parallel Processes
Concurrency and Automata on Infinite Sequences
The max-plus algebra of the natural numbers has no finite equational basis
A menagerie of non-finitely based process semantics over BPAMYAMPERSAND#x002A; ? from ready simulation to completed traces

--CTR
Luca Aceto , Wan Fokkink , Anna Ingolfsdottir , Sumit Nain, Bisimilarity is not finitely based over BPA with interrupt, Theoretical Computer Science, v.366 n.1, p.60-81, November 2006
possible futures;nested simulation;nested trace semantics;concurrency;non-finitely based algebras;hennessy-milner logic;complete axiomatizations;equational logic;BCCSP;process algebra