BRICS RS-03-27 Aceto et al.: Nested Semantics over Finite Trees are Equationally Hard BRICS

Basic Research in Computer Science

Nested Semantics over Finite Trees are Equationally Hard

Luca Aceto Willem Jan Fokkink Rob J. van Glabbeek Anna Ingólfsdóttir

BRICS Report Series RS-03-27

ISSN 0909-0878 August 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Luca Aceto & Willem Jan Fokkink & Rob J.

van Glabbeek & Anna Ingólfsdóttir. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/03/27/

Nested Semantics over Finite Trees are Equationally Hard

Luca Aceto^{1}, Wan Fokkink^{2}, Rob van Glabbeek^{4} and Anna Ingólfsdóttir^{1,3}

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

          Aalborg Ø, Denmark, luca@cs.auc.dk, annai@cs.auc.dk

2 CWI, Department of Software Engineering, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands, wan@cwi.nl 3 deCODE Genetics, Sturlugata 8, 101 Reykjavík, Iceland, annai@decode.is 4 INRIA, Sophia Antipolis, France, rvg@cs.stanford.edu

Abstract. 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.

2000 Mathematics Subject Classification: 08A70, 03B45, 03C05, 68Q10, 68Q45, 68Q55, 68Q70. CR Subject Classification (1991): D.3.1, F.1.1, F.1.2, F.3.2, F.3.4, F.4.1. Keywords and Phrases: Concurrency, process algebra, BCCSP, nested simulation, possible futures, nested trace semantics, equational logic, complete axiomatizations, non-finitely based algebras, Hennessy-Milner logic.

1 Introduction

Labelled transition systems (LTSs) [23] are a fundamental model of concurrent computation, 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 semantics, 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} ⊑ a^{2m} + a^{m}  (m ≥ 0) ,

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

a(a^{m} + a^{2m}) + aa^{3m} ⊑ aa^{2m} + a(a^{m} + a^{3m})  (m ≥ 0) .

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 actions, 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, Ésik and Ingólfsdóttir [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.

2 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 x, y, z), a 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 + q 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 BCCSP 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

\frac{x ⟶^{a} x′}{x + y ⟶^{a} x′} \frac{y ⟶^{a} y′}{x + y ⟶^{a} y′} ax ⟶^{a} x

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 ⊑ u over the language BCCSP. An inequation p ⊑ q is derivable from E, notation E ⊢ p ⊑ 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):

t ⊑ t \frac{t ⊑ u u ⊑ v}{t ⊑ v} \frac{t ⊑ u}{σ(t) ⊑ σ(u)} \frac{t ⊑ u}{at ⊑ au}(a ∈ A)

\frac{t ⊑ u}{t + r ⊑ u + r} \frac{t ⊑ u}{r + t ⊑ r + u} .

Without loss of generality one may assume that substitutions happen first in inequational proofs, i.e., that the third rule may only be used when (t ⊑ u) ∈ E. In this case σ(t) ⊑ σ(u) is called a substitution instance of an axiom in E.

Equational logic is like inequational logic, but with the extra rule of symmetry:

\frac{t ⊑ u}{u ⊑ t} .

In equational logic, the formula t ⊑ 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

\begin{aligned}A1 & x + y & ≈ & y + x \\ A2 & (x + y) + z & ≈ & x + (y + z) \\ A3 & x + x & ≈ & x \\ A4 & x + 0 & ≈ & x \end{aligned}

not distinguish t + u and u + t, nor (t + u) + v and t + (u + v), nor t + 0 and t. This is justified because all of the behavioural equivalences we consider satisfy axioms A1, A2 and A4 in Table 2. In what follows, the symbol = will denote syntactic equality modulo axioms A1, A2 and A4. We use a summation ∑_{i∈{1,...,k}} t_{i} to denote t_{1} + ⋯ + t_{k}, where the empty sum represents 0. It is easy to see that, modulo the equations A1, A2 and A4, every BCCSP term t has the form ∑_{i∈I} x_{i} + ∑_{j∈J} a_{j}t_{j}, for some finite index sets I, J, terms a_{j}t_{j} (j ∈ J) and variables x_{i} (i ∈ I). The terms a_{j}t_{j} (j ∈ J) and variables x_{i} (i ∈ 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 ⊑ q is provable from an inequational axiom system E iff there is a sequence p_{1} ⊑ ⋯ ⊑ p_{k} (k ≥ 1) such that

– p = p_{1},

– q = p_{k} and

– p_{i} = C[σ(t)] ⊑ C[σ(u)] = p_{i+1} for some closed substitution σ, context C[ ] and pair of terms t, u with t ⊑ u an axiom in E (1 ≤ i < k).

In what follows, we shall refer to sequences of the form p_{1} ⊑ ⋯ ⊑ 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([ ] + p)] or to one of the form [ ] + p, for some action b and closed BCCSP term p.

2.3 Traces of BCCSP Terms

The transition relations ⟶^{a} (a ∈ 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} ∈ A^{∗} (k ≥ 0), and BCCSP terms t, t′, we write t ⟶^{s} t′ iff there exists a sequence of transitions

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

If t ⟶^{s} t′ holds for some BCCSP term t′, 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} t′ for some t′ with u = σ(t′),

(b) or there are sequences of actions s_{1}, s_{2} with s_{2} non-empty and s = s_{1}s_{2}, a term t′ and a variable x such that t ⟶^{s_{1}} x + t′ and σ(x) ⟶^{s_{2}} u.

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 p ⟶^{a} p′ imply that there is a transition q ⟶^{a} q′ with p′ R q′.

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:

– p →^{⊂}_{0} q for all p, q,

– p →^{⊂}_{n+1} q iff p R q for some simulation R with R^{−1} included in →^{⊂}_{n}.

The kernel of →^{⊂}_{n} (i.e., the equivalence →^{⊂}_{n} ∩ (→^{⊂}_{n})^{−1}) is 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, respectively. 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 preorder (n ≥ 1).

Proposition 1. Let p, q be closed BCCSP terms, and n ≥ 0. Then p →^{⊂}_{n+1} q iff

(1) for all p ⟶^{a} p′ there is a q ⟶^{a} q′ with p′ →^{⊂}_{n+1} q′, and

(2) q →^{⊂}_{n} p.

Proof. We prove the two implications separately.

– (⇒) Assume that p →^{⊂}_{n+1} q. By definition, p R q with R a simulation and R^{−1} included in →^{⊂}_{n}. So if p ⟶^{a} p′, then q ⟶^{a} q′ with p′ R q′, which implies

p′ →^{⊂}_{n+1} q′ .

Moreover, since R^{−1} is included in →^{⊂}_{n}, it follows that q →^{⊂}_{n} p.

– (⇐) We define p R q iff (1) for all p ⟶^{a} p′ there is a q ⟶^{a} q′ with p′ →^{⊂}_{n+1} q′, and

(2) q →^{⊂}_{n} p.

Suppose now that p R q. If p ⟶^{a} p′, then by the definition of R we have q ⟶^{a} q′ with p′ →^{⊂}_{n+1} q′. Since we have already proven the ‘only if’ implication, we may conclude that p′ R q′. 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 ∈ IN, the closed BCCSP terms p_{n} and q_{n} thus:

\begin{aligned}p_{0} & = & a^{2m−1}0 & q_{0} & = & a^{m−1}0 \\ p_{n+1} & = & ap_{n} + aq_{n} & q_{n+1} & = & ap_{n} . \end{aligned}

By induction on n ∈ IN and using Proposition 1, it is not hard to check that p_{n} →^{⊂}_{n} q_{n}, and thus that q_{n} →^{⊂}_{n+1} p_{n}.

The terms p_{n} and q_{n} (n ∈ 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} p′ and X = traces(p′), for some p′.

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}^{T}, and n-nested trace preorder, denoted by ⪯_{n}^{T}, are defined inductively over closed BCCSP terms thus:

– p =_{0}^{T} q and p ⪯_{0}^{T} q for every p, q;

– p =_{n+1}^{T} q iff for every sequence of actions s ∈ A^{∗}: • if p ⟶^{s} p′ then there is a q′ such that q ⟶^{s} q′ and p′ =_{n}^{T} q′, and

• if q ⟶^{s} q′ then there is a p′ such that p ⟶^{s} p′ and p′ =_{n}^{T} q′;

– p ⪯_{n+1}^{T} q iff for every sequence of actions s ∈ A^{∗}: • if p ⟶^{s} p′ then there is a q′ such that q ⟶^{s} q′ and p′ =_{n}^{T} q′.

Note that the relations =_{1}^{T} and =_{2}^{T} are just trace equivalence (the equivalence that equates two terms having the same traces—see [14,19]) and possible futures equivalence, respectively, whereas ⪯_{2}^{T} is the possible futures preorder. Moreover, it is easy to see that, for every n ≥ 0, the equivalence relation =_{n}^{T} is the kernel of the preorder ⪯_{n}^{T}.

The following result is well-known—see, e.g., the references [17,18].

Proposition 2. For every n ≥ 0, the relations →^{⊂}_{n}, ⇆_{n}, =_{n}^{T} and ⪯_{n}^{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}, ⇆_{n}, =_{n}^{T} and ⪯_{n}^{T} (n ≥ 0). The inequation t ⊑ u is sound with respect to ⪯, written t ⪯ u, iff σ(t) ⪯ σ(u) for every closed substitution σ.

For instance, the inequation x ⊑ 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

a(x + y) ⊑ a(x + y) + ax .

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 →^{⊂}_{n+1} u, then t ⇆_{n} u;

2. if t ⪯_{n+1}^{T} u, then t =_{n}^{T} u;

3. if t →^{⊂}_{n} u, then t ⪯_{n}^{T} u.

Proof. Statement (1) is due to Groote and Vaandrager in [17], and statement (2) follows immediately from the definitions of the relations ⪯_{n+1}^{T} and =_{n}^{T}. 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 ⪯_{n}^{T} q by induction on n. This is trivial if n = 0. Suppose therefore that p →^{⊂}_{n+1} q. Let s be a sequence of actions in A, and assume that p ⟶^{s} p′ for some p′. We aim at showing that q ⟶^{s} q′ for some q′ with p′ =_{n}^{T} q′.

Since p →^{⊂}_{n+1} q and p ⟶^{s} p′, using Proposition 1 and a simple induction on the length of s, we have that q ⟶^{s} q′ for some q′ with p′ →^{⊂}_{n+1} q′. By statement (1) of the proposition, we may infer that p′ ⇆_{n} q′. The inductive hypothesis now yields that p′ ⪯_{n}^{T} q′ ⪯_{n}^{T} p′. Since the relation =_{n}^{T} is the kernel of ⪯_{n}^{T}, we may conclude that p′ =_{n}^{T} q′, 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:

φ ::= ⊤ | φ ∧ φ | ¬φ | ⟨a⟩φ (a ∈ A) .

The satisfaction relation ⊧ is the binary relation relating closed BCCSP terms and Hennessy-Milner formulae defined by structural induction on formulae thus:

– p ⊧ ⊤, for every closed BCCSP term p,

– p ⊧ φ_{1} ∧ φ_{2} iff p ⊧ φ_{1} and p ⊧ φ_{2},

– p ⊧ ¬φ iff it is not the case that p ⊧ φ, and

– p ⊧ ⟨a⟩φ iff p ⟶^{a} p′ for some p′ such that p′ ⊧ φ.

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 L_{n} of n-nested Hennessy-Milner formulae inductively thus:

– L_{0} contains only the formulae ⊤ and ¬⊤, and

– L_{n+1} is given by the following grammar

φ ::= ⊤ | φ ∧ φ | ¬φ | ⟨a_{1}⟩ ⋯ ⟨a_{k}⟩ψ (k ≥ 0, a_{1} ⋯ a_{k} ∈ A^{∗} and ψ ∈ L_{n}) .

The following result is due to Hennessy and Milner [18].

Theorem 1. Let p, q be closed BCCSP terms, and let n ≥ 0. Then p =_{n}^{T} q iff p and q satisfy the same formulae in the language L_{n}.

Remark 1. Note that, for every n ≥ 0 and closed terms p, q, if each formula in L_{n} satisfied by p is also satisfied by q, then p and q satisfy the same formulae in the language L_{n}. Indeed, assume that each formula in L_{n} satisfied by p is also satisfied by q, and that q satisfies φ ∈ L_{n}. Using the closure of L_{n} with respect to negation, we have that q |̸= ¬φ, and therefore that p |̸= ¬φ. 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 ⪯_{n}^{T} q iff each formula in L_{n} satisfied by p is also satisfied by q.

To obtain a modal characterization of the n-nested trace preorders, consider the sub-languages M_{n} of L_{n} defined inductively thus:

– M_{0} contains only the formulae ⊤ and ¬⊤, and

– M_{n+1} is given by the following grammar

φ ::= ⊤ | φ ∧ φ | ⟨a_{1}⟩ ⋯ ⟨a_{k}⟩ψ (k ≥ 0, a_{1} ⋯ a_{k} ∈ A^{∗} and ψ ∈ L_{n}) .

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 ⪯_{n}^{T} q iff each formula in M_{n} 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 ∈ A^{∗} is a completed trace of a term t iff t ⟶^{s} t′ holds for some term t′ 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 ⪯_{n}^{T}, =_{n}^{T}, ⇆_{n}, and →^{⊂}_{n}, for n ≥ 2. If t ⪯ u, then

(a) lengths(t) ⊆ lengths(u),

(b) depth(t) = depth(u),

(c) norm(t) ≥ norm(u) and

(d) var(t) = var(u).

Proof. In light of Proposition 3, it is sufficient to prove that the claims hold for the possible futures preorder, viz. the relation ⪯_{2}^{T}.

We argue, first of all, that claims (a)–(c) hold when t ⪯_{2}^{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 lengths(t) = lengths(p) and lengths(u) = lengths(q). So it suffices to prove claims (a)–(c) with p and q in place of t and u, respectively. By Definition 6, we have that p ⪯_{2}^{T} q.

Assume now that n ∈ lengths(p). Then there are a sequence s ∈ A^{∗} of length n and a closed term p′ with no outgoing transitions such that p ⟶^{s} p′. As p ⪯_{2}^{T} q, there is a closed term q′ such that q ⟶^{s} q′ and p′ =_{1}^{T} q′. Recall that p′ =_{1}^{T} q′ if, and only if, p′ and q′ have the same traces. It therefore follows that q′ has no outgoing transitions, and that n ∈ lengths(q), which was to be shown.

Claim (c) follows immediately from (a). To see that claim (b) holds, observe that if p ⪯_{2}^{T} 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 ⪯_{2}^{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)) ≠ 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 depth(t) = depth(u) < m also holds.

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

depth(σ(t)) ≥ m and
depth(σ(u)) = depth(u) < m .

By statement (b) of the lemma, it follows that σ(t) ⪯_{2}^{T} σ(u) does not hold, contradicting our assumption that t ⪯_{2}^{T} u. □

Remark 2. Note that lengths(t) = lengths(u) and norm(t) = norm(u) both hold, if t =_{2}^{T} u.

The restriction that n ≥ 2 is necessary in the statement of Lemma 2(a) and (c). In fact, aa + a ⇆_{1} aa, but

lengths(aa + a) = {1, 2} ⊈ {2} = lengths(aa) and
norm(aa + a) < norm(aa) .

Statements (b) and (d) in Lemma 2 also hold for =_{1}^{T}. In fact, it is not hard to see that, for every t, u, if t ⪯_{1}^{T} 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 inequationally axiomatizable. The following lemma will play a key role in the proof of this statement.

Lemma 3. If p →^{⊂}_{2} a^{2m} + a^{m}, then either p ⇆_{2} a^{2m} or p ⇆_{2} a^{2m} + a^{m}.

Proof. The case m = 0 is trivial; we 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} p′. Since p →^{⊂}_{2} a^{2m} + a^{m}, either p′ →^{⊂}_{2} a^{2m−1} or p′ →^{⊂}_{2} a^{m−1}. By Lemma 2(b), p has depth 2m. So there is at least one transition

p ⟶^{a} p′ with p′ →^{⊂}_{2} a^{2m−1}.

If for all transitions p ⟶^{a} p′ we have p′ →^{⊂}_{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′′ with p′′ →^{⊂}_{2} a^{m−1} (and so a^{m−1} →^{⊂}_{2} p′′), then it follows that a^{2m} + a^{m} →^{⊂}_{2} p, and hence p ⇆_{2} a^{2m} + a^{m}. □

The idea behind our proof that the 2-nested simulation preorder is not finitely inequationally 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} ⊑ p_{1} ⊑ ⋯ ⊑ p_{k} from E with p_{k} →^{⊂}_{2} a^{2m} + a^{m}, we have that p_{k} ⇆_{2} a^{2m}. Since a^{2m} + a^{m} ↛^{⊂}_{2} a^{2m}, it follows that a^{2m} ⊑ a^{2m} + a^{m} cannot be derived from E. However, a^{2m} →^{⊂}_{2} a^{2m} + a^{m}.

The following lemma is the crux in the implementation of the aforementioned proof idea.

Lemma 4. Let t ⊑ u be sound modulo →^{⊂}_{2}. Let m be greater than the depth of t. Assume that C[σ(u)] →^{⊂}_{2} a^{2m} + a^{m}, for some 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} + a^{m} ↛^{⊂}_{2} C[σ(u)]. In fact, if C[σ(u)] →^{⊂}_{2} a^{2m} + a^{m} and a^{2m} + a^{m} ↛^{⊂}_{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} ↛^{⊂}_{2} C[σ(u)] by distinguishing two cases, depending on the form of the context C[ ].

– Case 1: Suppose C[ ] is of the form C′[b([ ] + r)]. In this case, we shall prove a^{2m} + a^{m} ↛^{⊂}_{2} C[σ(u)] by arguing that a^{m−1} ↛^{⊂}_{2} q′ holds for each q′ such that C[σ(u)] ⟶^{a} q′. To this end, consider a transition

C[σ(u)] ⟶^{a} q′ .

Then q′ = D[σ(u)] for some context D[ ], and, because of the form of the context C[ ], we may infer that

C[σ(t)] ⟶^{a} p′ = D[σ(t)] .

As σ(t) →^{⊂}_{2} σ(u) by the soundness of t ⊑ u with respect to →^{⊂}_{2}, and p′ →^{⊂}_{2} q′ by Proposition 2, Lemma 2(b) yields that p′ and q′ have the same depth. Since C[σ(t)] ⇆_{2} a^{2m}, it follows by Proposition 1that p′ →^{⊂}_{2} a^{2m−1}. So by Lemma 2(b), we have that

depth(p′) = depth(q′) = 2m − 1 .

As depth(a^{m−1}) ≠ 2m − 1, another application of Lemma 2(b) yields that

a^{m−1} ↛^{⊂}_{2} q′ .

Since this holds for all transitions C[σ(u)] ⟶^{a} q′, and a^{2m} +a^{m} ⟶^{a} a^{m−1}, using Proposition 1 we may therefore conclude that a^{2m} + a^{m} ↛^{⊂}_{2} C[σ(u)].

– Case 2: Suppose C[ ] is of the form [ ] + r. In this case, we shall prove a^{2m} +a^{m} ↛^{⊂}_{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 u contain exactly the same variables. We proceed with the proof by distinguishing two cases, depending on whether norm(σ(t)) = 0 or not.

• Case norm(σ(t)) = 0. In this case, t has the form ∑_{i∈I} x_{i} for some finite index set I, and variables x_{i} (i ∈ I) with norm(σ(x_{i})) = 0 for each i ∈ I. Since t ⊑ u is sound with respect to →^{⊂}_{2}, statements (c)–(d) in Lemma 2 yield that t = u modulo axiom A3. Since axiom A3 is sound with respect to ⇆_{2}, using Proposition 2 we may therefore conclude that

a^{2m} + a^{m} ↛^{⊂}_{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 norm(r) = 0. By the soundness of t ⊑ u with respect to →^{⊂}_{2}, and the assumption that norm(σ(t)) > 0, it follows that depth(σ(t)) = depth(σ(u)) > 0. Hence σ(u) ≠ 0, and therefore we have that norm(σ(u)) > 0. As σ(u) + r →^{⊂}_{2} a^{2m} + a^{m}, again using Lemma 2(c), we infer that

norm(σ(u)) ≥ m .

Since depth(t) < m and norm(σ(t)) ≥ 2m, for each variable x ∈ var(t) = var(u) we have norm(σ(x)) > m. By the fact that depth(u) = depth(t) < m and norm(σ(u)) ≥ m, each completed trace of σ(u) must become, after less than m transitions, a completed trace of a σ(x) with x ∈ var(u). Since for all x ∈ var(u) = var(t) 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} + a^{m} ↛^{⊂}_{2} σ(u) + r, which was to be shown. □

Remark 3. The inequation ax ⊑ ax + a^{1} is sound modulo →^{⊂}_{2}. However, a^{4} ⇆̸_{2} a^{4} + a^{1}. So the proviso in the statement of Lemma 4 that C[σ(u)] →^{⊂}_{2} a^{2m} + a^{m} cannot be omitted. (Note that a^{4} + a^{1} ↛^{⊂}_{2} a^{4} + a^{2}.)

Theorem 2. BCCSP modulo the 2-nested simulation preorder is not finitely inequationally axiomatizable.

Proof. Let E be a finite inequational axiomatization for BCCSP that is sound modulo →^{⊂}_{2}. Let m > max{depth(t) | t ⊑ u ∈ E}.

By Lemma 4, and using induction on the length of derivations, it follows that if the closed inequation a^{2m} ⊑ 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} ↛^{⊂}_{2} a^{2m}, it follows that a^{2m} ⊑ a^{2m} + a^{m} cannot be derived from E. Since a^{2m} →^{⊂}_{2} a^{2m} + a^{m}, we may conclude that E is not complete

modulo →^{⊂}_{2}. □

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 ⊑ q that can be derived from E the following invariant property holds:

If lengths(q) ⊆ {m + 1, 2m + 1, 3m + 1}, and there is a p′ such that p ⟶^{a} p′, norm(p′) = m and depth(p′) ≤ 2m, then there is a q′ such that q ⟶^{a} q′, norm(q′) = m and depth(q′) ≤ 2m.

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 ⊑ u be sound modulo ⪯. Let t = Σ_{i∈I}x_{i} + Σ_{j∈J}a_{j}t_{j} and u = Σ_{k∈K}y_{k} + Σ_{ℓ∈L}b_{ℓ}u_{ℓ}, and let x be a variable. Then

(a) {x_{i} | i ∈ I} ⊆ {y_{k} | k ∈ K}, and

(b) for each j ∈ J with x ∈ var(t_{j}) there is an ℓ ∈ L such that a_{j} = b_{ℓ}, x ∈ var(u_{ℓ}) and var(u_{ℓ}) ⊆ var(t_{j}).

Proof. Let t ⊑ 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 {x_{i} | i ∈ I}, but not in {y_{k} | k ∈ K}. We shall exhibit a closed substitution σ such that σ(t) ⪯̸ σ(u), contradicting our assumption that t ⊑ u is sound modulo ⪯. To this end, pick a positive integer m > depth(t). Since t ⊑ 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 x = x_{i} for some i ∈ I, we have that m ∈ lengths(σ(t)). On the other hand, m ∉ lengths(σ(u)) because, as x is not contained in {y_{k} | k ∈ K}, 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 ⊑ u is sound modulo ⪯.

– Proof of Claim (b): Assume, towards a contradiction, that there is a j ∈ J with x ∈ var(t_{j}) such that, for each ℓ ∈ L with a_{j} = b_{ℓ} either x ∉ var(u_{ℓ}) or var(u_{ℓ}) ⊈ var(t_{j}). We shall exhibit a closed substitution σ such that σ(t) ⪯̸_{2}^{T} σ(u), contradicting our assumption that t ⊑ u is sound modulo ⪯. Let m be a positive integer larger than depth(t). Since t ⊑ 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}} σ(t_{j}), by Lemma 1. Moreover, since x ∈ var(t_{j}) and

depth(t_{j}) ≤ depth(t) − 1 ≤ m − 2 ,

it is easy to see that

m ≤ depth(σ(t_{j})) ≤ 2m − 2 .  (1)

We claim that if σ(u) ⟶^{a_{j}} p, then depth(σ(t_{j})) ≠ depth(p). This shows that σ(t) ⪯̸_{2}^{T} σ(u) because no p with σ(u) ⟶^{a_{j}} p can have the same traces as σ(t_{j}) (see Remark 2), contradicting our assumption that t ⊑ 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}} p because σ(y_{k}) ⟶^{a_{j}} p, for some k ∈ K. In this case, by the definition of σ, we have that depth(p) ∈ {m − 1, 2m − 1}. By (1), we may infer that depth(σ(t_{j})) ≠ depth(p), as claimed.

• Case 2: σ(u) ⟶^{a_{j}} p because p = σ(u_{ℓ}) for some ℓ ∈ L such that a_{j} = b_{ℓ} and either x ∉ var(u_{ℓ}) or var(u_{ℓ}) ⊈ var(t_{j}). In this case, by the definition of σ and using that depth(u) < m, we have that depth(p) is either smaller than m − 1 (if x ∉ var(u_{ℓ}) and var(u_{ℓ}) ⊆ var(t_{j})) or larger than 2m − 1 (if var(u_{ℓ}) ⊈ var(t_{j})). 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 ⪯. Let m > max{depth(t), depth(u) | (t ⊑ u) ∈ E}.

We have that

a(a^{m} + a^{2m}) + aa^{3m} ⪯ aa^{2m} + a(a^{m} + a^{3m})

because both processes have the same possible futures. Nevertheless,

E ⊬ a(a^{m} + a^{2m}) + aa^{3m} ⊑ aa^{2m} + a(a^{m} + a^{3m}) .

This follows immediately from the following

Claim. Assume that E ⊢ p ⊑ q, lengths(q) ⊆ {m + 1, 2m + 1, 3m + 1}, and there is a p′ such that p ⟶^{a} p′, norm(p′) = m and depth(p′) ≤ 2m. Then there is a q′ such that q ⟶^{a} q′, norm(q′) = m and depth(q′) ≤ 2m.

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 p = C[σ(t)] and q = C[σ(u)] for a BCCSP context C[ ], a closed substitution σ, and an axiom (t ⊑ u) ∈ E. We proceed by distinguishing two sub-cases, depending on the form of the context C[ ].

– Case 1: Suppose C[ ] is of the form C′[b([ ] + r)]. Let p′ be as in the statement of the claim. Then p′ = D[σ(t)] for some context D[ ], and, because of the form of the context C[ ], we may infer that

q = C[σ(u)] ⟶^{a} q′ = D[σ(u)] .

By the soundness of E and the fact that ⪯ is preserved by the operators of BCCSP (Proposition 2), we have that p′ ⪯ q′. Therefore norm(q′) ≤ norm(p′) = m and depth(q′) = depth(p′) ≤ 2m both hold by statements (b) and (c) in Lemma 2. As norm(q) ≥ m + 1 it follows that norm(q′) = m, and we are done.

– Case 2: Suppose C[ ] is of the form [ ] + r. Let t = Σ_{i∈I}x_{i} + Σ_{j∈J}a_{j}t_{j} and u = Σ_{k∈K}y_{k} + Σ_{ℓ∈L}b_{ℓ}u_{ℓ}. Consider a transition σ(t) + r ⟶^{a} p′ 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′. Then q ⟶^{a} p′ and we are done.

• Case 2.2: Assume that σ(x_{i}) ⟶^{a} p′ for some i ∈ I. By Lemma 5(a) and the soundness of t ⊑ u with respect to ⪯, we have that x_{i} = y_{k} for some k ∈ K. It follows that q ⟶^{a} p′, and we are done.

• Case 2.3: Assume that p′ = σ(t_{j}) for some j ∈ J. As norm(σ(t_{j})) = m and

depth(t_{j}) < depth(t) < m ,

there must be a variable x ∈ var(t_{j}) such that 1 ≤ norm(σ(x)) ≤ m. By statement (b) in Lemma 5, there is an ℓ ∈ L such that a = b_{ℓ}, x ∈ var(u_{ℓ}) and var(u_{ℓ}) ⊆ var(t_{j}). Take q′ = σ(u_{ℓ}). Then q ⟶^{a} q′. Since x ∈ var(u_{ℓ}), we have that

norm(q′) ≤ depth(u_{ℓ}) + norm(σ(x)) < 2m .

Considering that

lengths(q) ⊆ {m + 1, 2m + 1, 3m + 1} ,

and thus lengths(q′) ⊆ {m, 2m, 3m}, it must be the case that norm(q′) = m. As depth(σ(t_{j})) ≤ 2m by assumption, it follows that depth(σ(y)) ≤ 2m for each y ∈ var(t_{j}). Since var(u_{ℓ}) ⊆ var(t_{j}), this also holds for each y ∈ var(u_{ℓ}). As depth(u_{ℓ}) < depth(u) < m, this implies that depth(σ(u_{ℓ})) < 3m. Considering that lengths(q′) ⊆ {m, 2m, 3m}, we may conclude that depth(q′) ≤ 2m. To sum up, we have proven that, also in this case, q ⟶^{a} q′, norm(q′) = m and depth(q′) ≤ 2m, which was to be shown. □

5 No Nested Semantics is Finitely Based

We now proceed to offer results to the effect that the language BCCSP modulo =_{n}^{T} or ⇆_{n}, for n ≥ 2, or ⪯_{n}^{T} 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 =_{n}^{T} (the coarsest relation amongst =_{n}^{T}, ⇆_{n}, ⪯_{n+1}^{T} and →^{⊂}_{n+1}) can prove all of the closed inequations of the form p ⊑ q, with p and q BCCSP terms over action a, that are sound with respect to →^{⊂}_{n+1} (the finest relation amongst =_{n}^{T}, ⇆_{n}, ⪯_{n+1}^{T} and →^{⊂}_{n+1}).

In the proof of this result, we shall make use of the modal characterization of the relation =_{n}^{T} 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 =_{n}^{T}, there is a formula ψ_{n} in the language L_{n+1} (see Definition 8) such that whenever E proves a closed inequation p ⊑ 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 q_{n} →^{⊂}_{n+1} p_{n}, where the terms p_{n} and q_{n} have been defined in Example 1. This will allow us to conclude that the sound inequation q_{n} ⊑ p_{n} cannot be derived from E, and thus that E is incomplete for =_{n}^{T}, ⇆_{n}, ⪯_{n+1}^{T} 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 aforementioned 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 inequational axiomatization E′ such that the closed substitution instances of the axioms of E are the same as the closed substantial substitution instances of the axioms of E′ (when equating any closed subterm of depth 0 with 0). This is done by including in E′ any 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 ∈ 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 ax + x does not have a unique depth allocation, as the variable x occurs both at depth 0 and at depth 1 in it, but ax + y 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} v + u.

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 ∈ lengths(σ(x)) then d + n ∈ lengths(σ(t)).

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 v = t and d = 0. Then, letting ε denote the empty string, we have that

t ⟶^{ε} v = v + 0 ,

and we are done.

∗ Assume that v occurs in t + t′ at depth d because v occurs in t or t′ 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} v + u. If d is positive, we may immediately conclude that t + t′ ⟶^{s} v + u. If d = 0, then t = v + u. It follows that t + t′ ⟶^{ε} v + u + t′, and we are done.

∗ Assume that v occurs in at (with a ∈ 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} v + u. We prove that v occurs in t at depth d by induction on d. Throughout the proof, we let t = ∑_{i∈I} x_{i} + ∑_{j∈J} a_{j}t_{j}.

∗ Base Case: d = 0. Since t ⟶^{ε} v + u, we have that

t = ∑_{i∈I} x_{i} + ∑_{j∈J} a_{j}t_{j} = v + u .

This means that v = ∑_{i∈I′} x_{i} + ∑_{j∈J′} a_{j}t_{j} for some I′ ⊆ I and J′ ⊆ J. Since v 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 0.

∗ Inductive Step: d > 0. Since

t = ∑_{i∈I} x_{i} + ∑_{j∈J} a_{j}t_{j} ⟶^{s} v + u ,

and s is non-empty, we have that s = a_{j}s′ and t_{j} ⟶^{s′} v + u, for some j ∈ J. By induction, v 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 ∈ 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} x + u for some sequence of actions s of length d and term u. By Lemma 1, we have that

σ(t) ⟶^{s} σ(x + u) = σ(x) + σ(u) .

As n ∈ lengths(σ(x)) by our assumptions, σ(x) ⟶^{s′} v for some sequence of actions s′ of length n and term v with no outgoing transitions. Since the length of

s′ is positive, it follows that σ(t) ⟶^{ss′} v holds, and thus that d + n ∈ 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)) ⊆ {n + m, n + 2m}, for some n ≥ 0. Then t has a unique depth allocation.

Proof. Suppose a variable x occurs at depths d_{1} and d_{2} in t. Let depth(σ(x)) = d. Since σ is a substantial substitution, d is positive. Then, by Lemma 6(2) and the proviso of Lemma 7, we have that

{d_{1} + d, d_{2} + d} ⊆ lengths(σ(t)) ⊆ {n + m, n + 2m} .

(The proof of the first inclusion uses that d > 0.) As |d_{1} − d_{2}| < m holds by our assumption that depth(t) < m and Lemma 6(1), this implies d_{1} = d_{2}. □

The proof above is the only one where we use that the substitutions are substantial.

Definition 13. For m, ℓ ≥ 0, define the operator ;_{m}a^{ℓ} on closed BCCSP terms recursively by

• (Σ_{i=1}^{k}a_{i}p_{i});_{m+1}a^{ℓ} = Σ_{i=1}^{k}a_{i}(p_{i};_{m}a^{ℓ}),

• (bp + q);_{0}a^{ℓ} = bp + q,

• 0;_{0}a^{ℓ} = a^{ℓ}0.

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 ;_{m}a^{ℓ} 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 ⪯_{1}^{T} proving an inequation p ⊑ 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

p ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m}¬⟨a⟩⊤ ⇔ p;_{n+m}a^{ℓ} ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m+ℓ}⊤ .

Proof. Note, first of all, that the following holds, for each k ∈ IN and closed BCCSP term q′:

∃q (p ⟶^{a} q ∧ q′ = q;_{k} a^{ℓ}) ⇔ p;_{k+1}a^{ℓ} ⟶^{a} q′.  (2)

We prove the lemma by induction on n + m.

– Case: n + m = 0. Then

p ⊧ ¬⟨a⟩⊤ ⇔ p = 0  (as p is over action a)
⇔ p;_{0} a^{ℓ} ⊧ ⟨a⟩^{ℓ}⊤ (because depth(p) < ℓ) .

– Case: n = 0, m > 0. Then

p ⊧ ⟨a⟩^{m}¬⟨a⟩⊤ ⇔ ∃q (p ⟶^{a} q ⊧ ⟨a⟩^{m−1}¬⟨a⟩⊤)
⇔ ∃q′ (p;_{m} a^{ℓ} ⟶^{a} q′ ⊧ ⟨a⟩^{m+ℓ−1}⊤)
⇔ p;_{m} a^{ℓ} ⊧ ⟨a⟩^{m+ℓ}⊤ ,

where the second equivalence follows by (2) and the inductive hypothesis, using that q′ = q;_{m−1} a^{ℓ} and depth(q) < m + ℓ − 1.

– Case: n > 0. Then,

p ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m}¬⟨a⟩⊤ ⇔ ∃q (p ⟶^{a} q |̸= (⟨a⟩¬)^{n−1}⟨a⟩^{m}¬⟨a⟩⊤)
⇔ ∃q′ (p;_{n+m} a^{ℓ} ⟶^{a} q′ |̸= (⟨a⟩¬)^{n−1}⟨a⟩^{m+ℓ}⊤)
⇔ p;_{n+m} a^{ℓ} ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m+ℓ}⊤ ,

where the second equivalence follows by (2) and the inductive hypothesis, using that q′ = q;_{n+m−1} a^{ℓ} and depth(q) < n + m + ℓ − 1. □

The following example shows that in Lemma 8 the hypothesis depth(p) < n + m + ℓ cannot be omitted.

Example 2. If ℓ > 0, then a^{m+ℓ} |̸= ⟨a⟩^{m}¬⟨a⟩⊤. On the other hand,

a^{m+ℓ};_{m} a^{ℓ} = a^{m+ℓ} ⊧ ⟨a⟩^{m+ℓ}⊤ .

Lemma 9. Let σ be a closed substitution, and let t be a BCCSP term with a unique depth allocation and depth(t) < k. Let σ′ be a closed substitution with σ′(x) = σ(x);_{k−d} a^{ℓ} whenever x occurs at depth d in t. Then

σ′(t) = σ(t);_{k} a^{ℓ} .

Proof. We apply induction on k.

– Base Case: k = 0. This base case is vacuous, since there is no term whose depth is smaller than 0.

– Inductive Step: k > 0. We begin by proving that σ′(v) = σ(v);_{k} a^{ℓ} for each summand v of t.

• Consider a summand x of t. Since x occurs at depth 0 in t, the definition of σ′ yields that σ′(x) = σ(x);_{k} a^{ℓ}.

• Consider a summand au of t. Since σ′(y) = σ(y);_{k−e−1} a^{ℓ} for variables y that occur at depth e in u, and depth(u) < k − 1, by induction we may infer that σ′(u) = σ(u);_{k−1} a^{ℓ}. Hence σ′(au) = a(σ(u);_{k−1} a^{ℓ}) = σ(au);_{k} a^{ℓ}. Since σ′(v) = σ(v);_{k} a^{ℓ} holds for all summands v of t, it follows that σ′(t) = σ(t);_{k} a^{ℓ}, which was to be shown. □

Remark 4. The assumption that depth(t) be smaller than k in the statement of the above lemma is necessary. Take, for instance, k = 1, t = a + x and σ(x) = a^{2}. Then, if ℓ is positive,

σ(t);_{1} a^{ℓ} = a^{ℓ+1} + a^{2} ≠ a + a^{2} = σ′(t) .

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 σ′ be a closed substitution with σ′(x) = σ(x);_{n+m−d} a^{ℓ} whenever x occurs at depth d in t. Then

σ(t) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m}¬⟨a⟩⊤ ⇔ σ′(t) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m+ℓ}⊤ .

Proof. Since depth(t) < n + m, Lemma 9 yields that σ′(t) = σ(t);_{n+m} a^{ℓ}. Since depth(σ(t)) < n + m + ℓ, Lemma 10 now follows directly from Lemma 8. □

Note that the formula (⟨a⟩¬)^{n}⟨a⟩^{m+ℓ}⊤ is contained in the language L_{n+1} that gives a modal characterization of the equivalence =_{n+1}^{T}. (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 L_{n+2} or none of them does.

Lemma 11. Let t_{1}, t_{2} be a pair of BCCSP terms with depth(t_{i}) < m, for i = 1, 2, such that the equation t_{1} ≈ t_{2} is sound for (n + 1)-nested trace equivalence, for some n ≥ 0. Furthermore, let σ be a closed substantial substitution with lengths(σ(t_{i})) ⊆ {n + m, n + 2m} for i = 1, 2. Then

σ(t_{1}) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m}¬⟨a⟩⊤ ⇔ σ(t_{2}) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m}¬⟨a⟩⊤ .

Proof. Since lengths(σ(t_{i})) ⊆ {n + m, n + 2m}, for i = 1, 2, we have that

lengths(σ(t_{1} + t_{2})) ⊆ {n + m, n + 2m}

also holds. Thus, by Lemma 7, the term t_{1} + t_{2} has a unique depth allocation. Let σ′ be a closed substitution with σ′(x) = σ(x);_{n+m−d} a^{m+1} whenever x occurs at depth d in t_{1} + t_{2}. Using Lemma 10 (with ℓ = m + 1) for the vertical arrows, and the soundness of t_{1} ≈ t_{2} for =_{n+1}^{T} and the modal characterization of =_{n+1}^{T} (Theorem 1) for the horizontal one, we obtain

σ(t_{1}) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m}¬⟨a⟩⊤ σ(t_{2}) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{m}¬⟨a⟩⊤
⇕  ⇕
σ′(t_{1}) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{2m+1}⊤ ⇔ σ′(t_{2}) ⊧ (⟨a⟩¬)^{n}⟨a⟩^{2m+1}⊤

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 n ≥ 2), and none of the n-nested simulation and trace preorders (for n ≥ 3) are finitely based over BCCSP.

Theorem 4. BCCSP modulo =_{n}^{T} or ⇆_{n}, for n ≥ 2, or ⪯_{n}^{T} 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

m > max{depth(t), depth(u) | (t ⊑ u) ∈ E} .

Let p_{n} and q_{n} be defined, for each n ∈ IN, as in Example 1. For ease of reference, we recall that:

\begin{aligned}p_{0} & = & a^{2m−1}0 & q_{0} & = & a^{m−1}0 \\ p_{n+1} & = & ap_{n} + aq_{n} & q_{n+1} & = & ap_{n} \end{aligned}

As argued in Example 1, for every n ≥ 1, we have that p_{n} →^{⊂}_{n} q_{n}, and thus

q_{n} →^{⊂}_{(n+1)} p_{n} .

Let ψ_{1} = ⟨a⟩^{m}¬⟨a⟩⊤ and ψ_{n+1} = ⟨a⟩¬ψ_{n}. Note that the formula ψ_{n} is contained in L_{n+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 p_{n} ⊧ ψ_{n} but q_{n} ⊧ ¬ψ_{n}.

We now proceed to use the fact that p_{n} ⊧ ψ_{n} but q_{n} ⊧ ¬ψ_{n} to argue that the inequation q_{n} ⊑ p_{n} cannot be proven from any finite set of equations that is sound for =_{n}^{T}. To this end, suppose that E is sound for =_{n}^{T} (which, by Proposition 3, is certainly the case if E is sound for ⇆_{n}, ⪯_{n+1}^{T} or →^{⊂}_{n+1}), where n ≥ 2. We show that E is incomplete for →^{⊂}_{n+1} (and thus certainly for =_{n}^{T}, ⇆_{n} and ⪯_{n+1}^{T} by Proposition 3), because E ⊬ q_{n} ⊑ p_{n}. This follows immediately from the following:

Claim. Assume that E ⊢ p ⊑ q and lengths(q) ⊆ {n + m − 1, n + 2m − 1}. Then

p ⊧ ψ_{n} ⇔ q ⊧ ψ_{n} .

In fact, using this claim, we can show that E ⊬ q_{n} ⊑ p_{n} as follows. Observe, first of all, that lengths(p_{n}) is included in {n + m − 1, n + 2m − 1}, for each n ∈ IN. (In fact, lengths(p_{n}) equals {n+m−1, n+2m−1}, for each n ≥ 1.) We have already observed that p_{n} ⊧ ψ_{n} but q_{n} ⊧ ¬ψ_{n}. Thus, by the above claim, the inequation q_{n} ⊑ p_{n} cannot be derived from E.

Proof of the claim. We use induction on the length of the derivation of p ⊑ q from E. The cases of reflexivity and transitivity are trivial, using the soundness of E with respect to =_{n}^{T} and that, by Lemma 2(a), p =_{n}^{T} q implies lengths(p) = lengths(q), for each n ≥ 2. The case that p ⊑ 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 ⊑ q it needs to be shown for p + r ⊑ q + r, for every closed BCCSP term r over action a, and for ap ⊑ aq. The first of these follows trivially by the observation that

p + r ⊧ ψ_{n} iff p ⊧ ψ_{n} or r ⊧ ψ_{n} .

For the second, the soundness of E yields p =_{n}^{T} q. Using the modal characterization of =_{n}^{T}, and that ψ_{n−1} is contained in L_{n}, we have that

p ⊧ ψ_{n−1} ⇔ q ⊧ ψ_{n−1} .

Since ψ_{n} = ⟨a⟩¬ψ_{n−1}, it follows that

ap ⊧ ψ_{n} ⇔ aq ⊧ ψ_{n} ,

which was to be shown. □

Remark 5. If E contains the axiom ax ⊑ ax + a, which is sound for →^{⊂}_{2}, we have that E ⊢ a^{2m} ⊑ a^{m−1}(a^{m+1} + a). As a^{m−1}(a^{m+1} + a) ⊧ ψ_{1} but a^{2m} |̸= ψ_{1}, the proof above, and the claim in particular, does not apply to ⪯_{2}^{T} and →^{⊂}_{2}.

Indeed, three different proofs appear to be needed to establish all of our non-finite axiomatizability 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 E_{PF} that contains the equations in Table 2, and the inequation

a(x + y) ⊑ ax + ay .  (3)

It is not too hard to see that E_{PF} is sound for the possible futures preorder. In fact, for all closed BCCSP terms p, q,

– the terms a(p + q) and ap + aq 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 E_{PF} is complete for the 2-nested simulation preorder over the collection of closed BCCSP terms over action a. The following lemma will play a key 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

E_{PF} ⊢ q ⊑ q + p .

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.

– Case p = 0. In this case, E_{PF} ⊢ q ≈ q + p follows immediately from axiom A4 in Table 2.

– Case p = ap′, for some p′. Assume that q = ∑_{j∈J} aq_{j}, for some finite index set J and closed terms q_{j} over action a (j ∈ J). Since depth(p) ≤ depth(q) by our assumptions, there is an index j ∈ J such that depth(p′) ≤ depth(q_{j}). By the inductive hypothesis, we have that

E_{PF} ⊢ q_{j} ⊑ q_{j} + p′ .

Hence,

\begin{aligned}E_{PF} ⊢ & aq_{j} & ⊑ & a(q_{j} + p′) \\ & & ⊑ & aq_{j} + ap′ & (By (3)) . \end{aligned}

The claim now follows using closure with respect to BCCSP contexts.

– Case p = p_{1} + p_{2}, for some p_{1}, p_{2} different from 0. Since depth(p) ≤ depth(q) by our assumptions, we have depth(p_{i}) ≤ depth(q) for i = 1, 2. By the inductive hypothesis, we may infer that

E_{PF} ⊢ q ⊑ q + p_{i} ,

for i = 1, 2. Thus,

E_{PF} ⊢ q ⊑ q + p_{2} ⊑ q + p_{1} + p_{2} ,

which was to be shown. □

We are now ready to prove that the axiom system E_{PF} 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

E_{PF} ⊢ p ⊑ q .

Proof. We prove the claim by induction on the depth of p. Let p = ∑_{i∈I} ap_{i} and q = ∑_{j∈J} aq_{j}, for some finite index sets I and J and closed terms p_{i} (i ∈ I) and q_{j} (j ∈ J) over action a. Note that, as p →^{⊂}_{2} q, the depth of q is equal to that of p (Lemma 2(b)).

Let i ∈ I. Then, since p →^{⊂}_{2} q, there is an index j_{i} such that p_{i} →^{⊂}_{2} q_{j_{i}} (Proposition 1). Since the depth of p_{i} is smaller than that of p, by our inductive hypothesis it follows that the inequation p_{i} ⊑ q_{j_{i}} can be proven from E_{PF} . Since this holds for each i ∈ I, we have that

E_{PF} ⊢ p ⊑ ∑_{i∈I} aq_{j_{i}} .

To conclude the proof, it suffices only to show that

E_{PF} ⊢ ∑_{i∈I} aq_{j_{i}} ⊑ q .

To this end, note that, since E_{PF} is sound with respect to the possible futures preorder, and the inequation p ⊑ ∑_{i∈I} aq_{j_{i}} is derivable from it, the terms p and ∑_{i∈I} aq_{j_{i}} have the same depth (Lemma 2(b)). As previously observed, p and q also have the same depth. Write now

q = ∑_{i∈I} aq_{j_{i}} + r ,

where r is the sum of all the summands of q not occurring in ∑_{i∈I} aq_{j_{i}}. By the previous observations, we have that

depth(r) ≤ depth(q) = depth(∑_{i∈I} aq_{j_{i}}) .

Lemma 12 now yields that

E_{PF} ⊢ ∑_{i∈I} aq_{j_{i}} ⊑ ∑_{i∈I} aq_{j_{i}} + r = q ,

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 equivalence. These were defined thus:

Definition 14. For every n ≥ 0, the relations =_{n}^{A} are defined inductively over closed BCCSP terms thus:

– p =_{0}^{A} q for every p, q;

– p =_{n+1}^{A} q iff for every action a ∈ A: • if p ⟶^{a} p′ then there is a q′ such that q ⟶^{a} q′ and p′ =_{n}^{A} q′, and

• if q ⟶^{a} q′ then there is a p′ such that p ⟶^{a} p′ and p′ =_{n}^{A} q′.

Note that, unlike the n-nested trace equivalences =_{n}^{T}, the relations =_{n}^{A} 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 =_{n}^{A}. Moreover, each of the =_{n}^{A} 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 =_{n}^{A} over 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 E_{n}, for n ≥ 0, with the following property:

Theorem 6. Let p, q be closed BCCSP terms. Then p =_{n}^{A} q if, and only if, Ax ∪ E_{n} ⊢ p ≈ q.

The axiom systems E_{n}, 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 {x_{1}, x_{2}, …}.

Definition 15. For each n ≥ 0, we define the axiom system E_{n} thus:

E_{0} = {x_{1} ≈ x_{2}} and
E_{n+1} = {a(t + x_{n+3}) ≈ a(u + x_{n+3}) | a ∈ A, (t ≈ u) ∈ E_{n}} .

Note that, if A is a finite set set containing, say, k actions, then the axiom system E_{n} contains k^{n} equations, for each n ≥ 0. Moreover, observe for later use that, for each n ≥ 0, the axioms in E_{n} only use variables x_{1}, …, x_{n+2}.

We shall now show that Theorem 6 does hold for the previously defined axiom systems E_{n}. Since the soundness of each of the axioms in E_{n} can easily be shown by induction on n, using the aforementioned congruence properties of the relations =_{n}^{A}, we shall limit ourselves to presenting a proof of the completeness of Ax ∪ E_{n} with respect to =_{n}^{A} over 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 ∪ E_{n} ⊢ p ≈ q. Then Ax ∪ E_{n+1} ⊢ ap ≈ aq, for each action a ∈ A.

Proof. Assume that Ax ∪ E_{n} ⊢ p ≈ q, for some closed BCCSP terms p, q. Recall that this means that there is a sequence p_{1} ≈ ⋯ ≈ p_{k} (k ≥ 1) such that

– p = p_{1},

– q = p_{k} and

– p_{i} = C[σ(t)] ≈ C[σ(u)] = p_{i+1} for some closed substitution σ, context C[ ] and pair of terms t, u with t ≈ u or u ≈ t an axiom in Ax ∪ E_{n} (1 ≤ i < k).

We prove that Ax ∪ E_{n+1} ⊢ ap ≈ aq, for each action a ∈ A, by induction on k.

– Base Case: k = 1. In this case we have that p = 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 ∪ E_{n+1}. Since ap_{k} = aq, to complete the proof, we are therefore left to prove that

Ax ∪ E_{n+1} ⊢ ap_{k−1} ≈ ap_{k} .  (4)

To this end, recall that

• p_{k−1} = C[σ(t)] and

• p_{k} = C[σ(u)], for some closed substitution σ, context C[ ] and pair of terms t, u with t ≈ u or u ≈ t an axiom in Ax ∪E_{n}. 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 E_{n} proceeds by a case analysis on the form of the context C[ ].

• Case 1: Suppose C[ ] is of the form C′[b([ ] + r)], for some action b and closed term r. In this case, it is sufficient to show that

Ax ∪ E_{n+1} ⊢ b(σ(t) + r) ≈ b(σ(u) + r)

as (4) will then follow by applying the rule of closure under BCCSP contexts repeatedly. To this end, let σ′ be the closed substitution that maps variable x_{n+3} to r, and acts like σ on all of the other variables. Using the axioms in Ax ∪ E_{n+1}, we have that

b(σ(t) + r) ≈ σ′(b(t + x_{n+3})) (as x_{n+3} ∉ var(t))
≈ σ′(b(u + x_{n+3})) (as b(t + x_{n+3}) ≈ b(u + x_{n+3}) ∈ E_{n+1})
≈ b(σ(u) + r) (as x_{n+3} ∉ var(u)) ,

which was to be shown.

• Case 2: Suppose C[ ] is of the form [ ] + r, for some closed term r.

In this case, letting σ′ be defined as above, and using the axioms in Ax ∪E_{n+1}, we have that

ap_{k−1} ≈ a(σ(t) + r)
≈ σ′(a(t + x_{n+3})) (as x_{n+3} ∉ var(t))
≈ σ′(a(u + x_{n+3})) (as a(t + x_{n+3}) ≈ a(u + x_{n+3}) ∈ E_{n+1})
≈ a(σ(u) + r) (as x_{n+3} ∉ var(u))
≈ ap_{k} ,

which was to be shown. The remaining case, viz. when u ≈ t an axiom in E_{n}, is similar. □

We are now ready to establish the completeness of Ax ∪ E_{n} with respect to =_{n}^{A} over 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 ∪ E_{n} is complete with respect to =_{n}^{A} over closed BCCSP terms, and that p =_{n+1}^{A} q holds for closed terms p, q. We shall now argue that the equation p ≈ q can be derived from the axiom system Ax ∪ E_{n+1}. Let p = ∑_{i∈I} a_{i}p_{i} and q = ∑_{j∈J} b_{j}q_{j}, for some finite index sets I and J and closed terms a_{i}p_{i} (i ∈ I) and b_{j}q_{j} (j ∈ J). Our order of business will now be to show that

Ax ∪ E_{n+1} ⊢ p ≈ p + q ≈ q .

By symmetry, it is sufficient to show that the equation p + q ≈ q is derivable from Ax ∪ E_{n+1}. To this end, let i ∈ I. Then, since p =_{n+1}^{A} q, there is an index j_{i} such that a_{i} = b_{j_{i}} and p_{i} =_{n}^{A} q_{j_{i}}. Since the axiom system Ax ∪E_{n} is complete with respect to =_{n}^{A} by our inductive hypothesis, it follows that the equation p_{i} ≈ q_{j_{i}} can be proven from Ax ∪E_{n}. By Lemma 13, the equation a_{i}p_{i} ≈ b_{j_{i}}q_{j_{i}} can be derived from Ax ∪E_{n+1}. As this holds for each index i ∈ I, it follows that p + q ≈ q is derivable from Ax ∪ E_{n+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ólfsdóttir 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.

References

1. L. Aceto, Z. Ésik and A. Ingólfsdóttir, On the two-variable fragment of the equational theory of the max-sum algebra of the natural numbers, in Proceedings of the 17th International Symposium on Theoretical Aspects of Computer Science, STACS 2000 (Lille), H. Reichel and S. Tison, eds., vol. 1770 of Lecture Notes in Computer Science, Springer-Verlag, Feb. 2000, pp. 267–278.

2. , The max-plus algebra of the natural numbers has no finite equational basis, Theoretical Comput. Sci., 293 (2003), pp. 169–188.

3. L. Aceto, W. Fokkink and A. Ingólfsdóttir, A menagerie of non-finitely based process semantics over BPA*—from ready simulation to completed traces, Mathematical Structures in Computer Science, 8 (1998), pp. 193–230.

4. , 2-nested simulation is not finitely equationally axiomatizable, in Proceedings of the 18th International Symposium on Theoretical Aspects of Computer Science, STACS 2001 (Dresden), vol. 2010 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2001, pp. 39–50.

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

6. J. Bergstra and J. W. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

7. , Process algebra for synchronous communication, Information and Computation, 60 (1984), pp. 109–137.

8. S. Blom, W. Fokkink and S. Nain, On the axiomatizability of ready traces, ready simulation and failure traces, in Proceedings 30th Colloquium on Automata, Languages and Programming—ICALP’03, Eindhoven, J. C. M. Baeten, J. K. Lenstra, J. Parrow and G. J. Woeginger, eds., vol. 2719 of Lecture Notes in Computer Science, Springer-Verlag, June 2003, pp. 109–118.

9. S. Christensen, Y. Hirshfeld and F. Moller, Bisimulation equivalence is decidable for basic parallel processes, in Proceedings CONCUR 93, Hildesheim, Germany, E. Best, ed., vol. 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 143–157.

10. S. Christensen, H. Hüttel and C. Stirling, Bisimulation equivalence is decidable for all context-free processes, Information and Computation, 121 (1995), pp. 143–148.

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

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

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

14. R. J. van Glabbeek, The linear time–branching time spectrum I. The semantics of concrete, sequential processes, in Handbook of Process Algebra, North-Holland, Amsterdam, 2001, pp. 3–99.

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

16. J. F. Groote and H. Hüttel, Undecidable equivalences for basic process algebra, Information and Computation, 115 (1994), pp. 354–371.

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

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

19. C. Hoare, Communicating sequential processes, in On the construction of programs – an advanced course, R. McKeag and A. Macnaghten, eds., Cambridge University Press, 1980, pp. 229–254.

20. , Communicating Sequential Processes, Prentice-Hall International, Englewood Cliffs, 1985.

21. H. Hüttel, Undecidable equivalences for basic parallel processes, in Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS’94), Sendai, Japan, April 19–22, 1994, M. Hagiya and J. C. Mitchell, eds., vol. 789 of Lecture Notes in Computer Science, Springer-Verlag, 1994, pp. 454–464.

22. P. C. Kannellakis and S. A. Smolka, CCS expressions, finite state processes, and three problems of equivalence, Information and Computation, 86 (1990), pp. 43–68.

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

24. H. Lin, An interactive proof tool for process algebras, in 9th Annual Symposium on Theoretical Aspects of Computer Science, vol. 577 of Lecture Notes in Computer Science, Cachan, France, 13–15 Feb. 1992, Springer, pp. 617–618.

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

26. W. Mitchell and D. Carlisle, Modal observation equivalence of processes, Technical Report UMCS-96-1-1, Manchester University, Computer Science Department, 1996.

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

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

29. D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, Karlsruhe, Germany, 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. V. Redko, On defining relations for the algebra of regular events, Ukrainskii Matematicheskii Zhurnal, 16 (1964), pp. 120–126. In Russian.

32. W. Rounds and S. Brookes, Possible futures, acceptances, refusals and communicating processes, in 22^{nd} Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, New York, 1981, IEEE, pp. 140–149.

33. P. Sewell, Nonaxiomatisability of equivalences over finite state processes, Annals of Pure and Applied Logic, 90 (1997), pp. 163–191.

34. S. K. Shukla, D. J. Rosenkrantz, H. B. Hunt, III and R. E. Stearns, The polynomial time decidability of simulation relations for finite state processes: a HORNSAT based approach, in Satisfiability problem: Theory and applications (Piscataway, NJ, 1996), vol. 35 of DIMACS Ser. Discrete Math. Theoret. Comput. Sci., Amer. Math. Soc., Providence, RI, 1997, pp. 603–641.

Recent BRICS Report Series Publications

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

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

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

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

RS-03-23 Korovin Margarita. Recent Advances in Σ-Definability over Continuous Data Types. June 2003. 26 pp.

RS-03-22 Ivan B. Damgård and Mads J. Jurik. Scalable Key-Escrow. May 2003. 15 pp.

RS-03-21 Ulrich Kohlenbach. Some Logical Metatheorems with Applications in Functional Analysis. May 2003. 55 pp.

RS-03-20 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. May 2003. 16 pp. Final version to appear in Leuschel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’03 Proceedings, 2003. This report supersedes the earlier BRICS report RS-03-11.

RS-03-19 Christian Kirkegaard, Anders Møller, and Michael I. Schwartzbach. Static Analysis of XML Transformations in Java. May 2003. 29 pp.

RS-03-18 Bartek Klin and Pawe� Sobociński. Syntactic Formats for Free: An Abstract Approach to Process Equivalence. April 2003. 41 pp.