BRICS RS-00-20 Aceto et al.: 2-Nested Simulation is not Finitely Equationally Axiomatizable BRICS

Basic Research in Computer Science

2-Nested Simulation is not Finitely Equationally Axiomatizable

Luca Aceto Willem Jan Fokkink Anna Ingólfsdóttir BRICS Report Series RS-00-20 ISSN 0909-0878 August 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Luca Aceto & Willem Jan Fokkink & 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/00/20/

2-Nested Simulation is not Finitely Equationally Axiomatizable

Luca Aceto^{1}, Wan Fokkink^{2}, and Anna Ingólfsdóttir^{1}

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

Abstract. 2-nested simulation was introduced by Groote and Vaandrager [10] as the coarsest equivalence included in completed trace equivalence for which the tyft/tyxt format is a congruence format. In the linear time-branching time spectrum of van Glabbeek [8], 2-nested simulation is one of the few equivalences for which no finite equational axiomatization is presented. In this paper we prove that such an axiomatization does not exist for 2-nested simulation. Keywords: Concurrency, process algebra, basic CCS, 2-nested simulation, equational logic, complete axiomatizations.

1 Introduction

Labelled transition systems (LTSs) [11] 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 [19] and, following Milner’s pioneering work on CCS [15], 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. (Cf. the encyclopaedic study [8], where van Glabbeek presents the linear time-branching time spectrum—a lattice that contains all the 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 [12]. 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 behavioral semantics in van Glabbeek’s spectrum is offered in [8]. The equational axiomatizations offered ibidem are over Milner’s Basic CCS (abbreviated to BCCS in what follows), a fragment of CCS suitable for describing finite synchronization trees, and characterize the differences between behavioural semantics in terms of a few revealing axioms.

The main omission in this menagerie of equational axiomatizations for the behavioural semantics in van Glabbeek’s spectrum is an axiomatization for 2nested simulation semantics. 2-nested simulation was introduced by Groote and Vaandrager [10] 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 [22], and can be characterized by a single parameterised modal logic formula [16]. However, as previously mentioned, no equational axiomatization for it has ever been proposed, even for the language BCCS.

In this paper, we offer a possible mathematical justification for the lack of an equational axiomatization for the 2-nested simulation equivalence and preorder even for the language of finite synchronization trees [14]. More precisely, we show that neither of these two behavioural relations has a finite equational axiomatization over the language of BCCS. These 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 equations that are sound with respect to 2-nested simulation equivalence can be used to derive all of the sound equalities of the form

a(a^{2m} + a^{m}) ≈ a(a^{2m} + a^{m}) + a^{2m+1}  (m ≥ 0) .

The import of these two results is that not only the equational theory of 2-nested simulation is not finitely equationally axiomatizable, but neither is the collection of (in)equivalences that hold between BCCS terms over one action and without occurrences of variables. This state of affairs should be contrasted with the elegant equational axiomatizations over BCCS for most of the other behavioural equivalences in the linear time–branching time spectrum that are reviewed by van Glabbeek in [8]. Only in the case of additional, more complex operators, such as iteration, are these equivalences known to lack a finite equational axiomatization; see, e.g., [3, 6, 7, 20, 21]. Of special relevance for concurrency theory are Moller’s results to the effect that the process algebras ACP and CCS (without the auxiliary left merge operator from [5]) do not have a finite equational axiomatization modulo bisimulation equivalence [17, 18]. 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].

The paper is organized as follows. We begin by presenting preliminaries on the language BCCS and (in)equational logic (Sect. 2). We then proceed to define 2-nested simulation, and study some of its basic properties that play a major role in the proof of our main results (Sect. 3). The definition of 2-nested simulation suggests a natural conditional inference system for it. This is presented in Sect. 4. Our main results on the non-existence of finite (in)equational axiomatizations for 2-nested equivalence and preorder are the topic of Sects. 5 and 6. The paper concludes with a result to the effect that the 3-nested simulation preorder has no finite inequational axiomatization, and some open problems (Sect. 7).

2 Preliminaries

The language BCCS The process algebra BCCS [14] is a basic formalism to express finite process behaviour. Its syntax consists of (process) terms that are constructed from a countably infinite set of 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 nonempty set Act 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, and ap can execute action a to transform into p. This intuition for the operators of BCCS is captured, in the style of Plotkin [19], by the transition rules in Table 1. These transition rules give rise to transitions between process terms. The operational semantics for BCCS is thus given by the labelled transition system [11] whose states are terms, and whose Act-labelled transitions are those that are provable using the rules in Table 1.

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

Table 1. Transition rules for BCCS

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

Table 2. Axioms for BCCS

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

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 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 BCCS term t has the form ∑_{i∈I} x_{i} + ∑_{j∈J} a_{j}t_{j}, for some finite index sets I, J, terms t_{j} (j ∈ J) and variables x_{i} (i ∈ I).

Equational logic An axiom system is a collection of (in)equations over the language BCCS. We say that an equation t ≈ u (resp. an inequation t <_{∼} u) is derivable from an axiom system E if it can be proven from the axioms in E using the standard rules of equational (resp. inequational) logic. It is well-known (cf., e.g., Sect. 2 in [9]) 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 our main results (cf. Thms. 3 and 4), 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 BCCS 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 equation p ≈ q is provable from an equational 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 either t ≈ u or u ≈ t an axiom in E (1 ≤ i < k).

The obvious modification of the above observation applies to proofs of inequations from inequational axiom systems. In what follows, we shall refer to sequences of the form p_{1} ≈ ⋯ ≈ p_{k} (resp. p_{1} <_{∼} ⋯ <_{∼} p_{k}) as equational (resp. inequational) derivations.

For later use, note that, using axioms A1, A2 and A4 in Table 2, every context can be proven equal to either one of the form C[b([] + p)] or to one of the form [] + p, for some action b and closed BCCS term p.

3 2-nested simulation

In this paper, we shall study the (in)equational theory of 2-nested simulation semantics over BCCS. This is a behavioural semantics for processes that stems from [10], where it was characterized as the largest congruence with respect to the tyft/tyxt format of transition rules which is included in completed trace semantics.

Definition 1. A binary relation R between closed terms is a simulation iff p R q together with p →^{a} p′ implies that there is a transition q →^{a} q′ with p′ R q′.

For closed terms p, q, we write p ⊂_{→}^{1} q iff p R q with R a simulation. The kernel of ⊂_{→}^{1} (i.e., the equivalence ⊂_{→}^{1} ∩(⊂_{→}^{1})^{−1}) is denoted by ⇆^{1}.

The relation ⊂_{→}^{1} is the well-known simulation preorder [13].

Definition 2. For closed terms p, q, we write p ⊂_{→}^{2} q iff p R q with R a simulation and R^{−1} included in ⊂_{→}^{1}. The kernel of ⊂_{→}^{2} (i.e., the equivalence ⊂_{→}^{2} ∩(⊂_{→}^{2})^{−1}) is denoted by ⇆^{2}.

The relations ⊂_{→}^{2} and ⇆^{2} are the 2-nested simulation preorder and the 2-nested simulation equivalence, respectively. It is easy to see that ⊂_{→}^{2} is included in ⇆^{1}. In the remainder of this paper we will use, instead of Definition 2, the following more descriptive characterization of 2-nested simulation. To the best of our knowledge, this characterization is new.

Theorem 1. Let p, q be closed BCCS terms. Then p ⊂_{→}^{2} q iff

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

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

Proof. We prove the two implications separately.

(⇒) Let p ⊂_{→}^{2} q. By definition, p R q with R a simulation and R^{−1} included in ⊂_{→}^{1}. So if p →^{a} p′, then q →^{a} q′ with p′ R q′, which implies p′ ⊂_{→}^{2} q′. Moreover, since R^{−1} is included in ⊂_{→}^{1}, it follows that q ⊂_{→}^{1} p.

(⇐) We define p R q iff

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

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

Suppose p R q. If p →^{a} p′, then by the definition of R we have q →^{a} q′ with p′ ⊂_{→}^{2} q′. Since we have already proven the ‘only if’ implication, p′ R q′. So R is a simulation. Furthermore, by (2) R^{−1} is included in ⊂_{→}^{1}. Hence, p ⊂_{→}^{2} q. □

The transition rules in Table 1 are in tyft/tyxt format, that is a (pre)congruence format for ⊂_{→}^{2} and ⇆^{2} [10]. Hence, we immediately have that:

Lemma 1. The relations ⊂_{→}^{2} and ⇆^{2} are preserved by the operators of BCCS.

The relations ⊂_{→}^{2} and ⇆^{2} are extended to arbitrary BCCS terms thus:

Definition 3. Let t, u be BCCS terms. The inequation t <_{∼} u is sound with respect to ⊂_{→}^{2} iff σ(t) ⊂_{→}^{2} σ(u) holds for every closed substitution σ. Similarly, the equation t ≈ u is sound with respect to ⇆^{2} iff σ(t) ⇆^{2} σ(u) holds for every closed substitution σ.

Examples of (in)equations that are sound with respect to ⊂_{→}^{2} are those in Table 2 and

a(x + y) <_{∼} a(x + y) + ax .

3.1 Norm and depth

We now present some results on the depth and the norm of BCCS terms that are related in 2-nested simulation semantics. These will find important applications in the proofs of our main results, and shed light on the nature of the identifications made by 2-nested simulation semantics.

Definition 4. A sequence a_{1} ⋯ a_{k} ∈ Act^{∗} (k ≥ 0) is a termination trace of a term t iff there exists a sequence of transitions t = t_{0} →^{a_{1}} t_{1} →^{a_{2}} ⋯ →^{a_{k}} t_{k} with t_{k} a term without outgoing transitions.

Definition 5. The depth and the norm of a BCCS term t, denoted by depth(t) and norm(t), are the lengths of the longest and of the shortest termination trace of t, respectively.

Lemma 2. If p ⊂_{→}^{2} q, then

1. each termination trace of p is a termination trace of q;

2. depth(p) = depth(q); and

3. norm(p) ≥ norm(q).

Proof. We prove the three statements separately.

1. By induction on the depth of p.

[Base case] Let depth(p) = 0. Then p cannot perform any transitions, so the empty trace is the only termination trace of p. Since p ⊂_{→}^{2} q implies q ⊂_{→}^{1} p, it follows that q cannot perform any transitions either. Hence, the empty trace is also a termination trace of q.

[Inductive case] Consider a termination trace a_{1} ⋯ a_{k} of p; since depth(p) > 0 we have k > 0. Then p →^{a_{1}} p′ where a_{2} ⋯ a_{k} is a termination trace of p′. Since p ⊂_{→}^{2} q, there is a transition q →^{a_{1}} q′ with p′ ⊂_{→}^{2} q′. By the induction hypothesis a_{2} ⋯ a_{k} is a termination trace of q′. So a_{1} ⋯ a_{k} is a termination trace of q.

Table 3. Axiom for simulation

S x <_{∼}_{1} x + y

Table 4. Axiom for 2-nested simulation

2S y <_{∼}_{1} x ⇒ x <_{∼}_{2} x + y

2. p ⊂_{→}^{2} q implies p ⇆^{1} q, so clearly p and q must have equal depth.

3. By statement 1 in the lemma, the shortest termination trace of p is a termination trace of q. □

Remark: If p ⊂_{→}^{2} q, then q may afford more termination traces than p. As an example, consider the terms p = aa0 and q = p + a0. So if p ⊂_{→}^{2} q, then norm(p) may be strictly larger than norm(q).

4 A conditional axiomatization

The definition of 2-nested simulation immediately suggests an implicational proof system for the 2-nested simulation preorder. It is folklore that the axioms in Tables 2 and 3 give a complete axiomatization of the simulation preorder over the language BCCS [8]. To obtain a complete inference system for the 2-nested simulation preorder, it is sufficient to add the conditional axiom in Table 4 to the axiom system in Table 2. In axioms S and 2S, the relation symbol <_{∼}_{1} refers to inequations that are provable using the proof system for the simulation preorder, while the relation symbol <_{∼}_{2} refers to inequations that are provable using the proof system for the 2-nested simulation preorder. Not too surprisingly, we have that:

Theorem 2. A1-4+2S is sound and complete for BCCS modulo the 2-nested simulation preorder.

Proof. The soundness proof is left to the reader. We prove that A1-4+2S is complete modulo the 2-nested simulation preorder. Suppose p ⊂_{→}^{2} q. We prove, by induction on the depth of p, that p <_{∼} q can be derived from A1-4+2S.

Let p = ∑_{i∈I} a_{i}p_{i} and q = ∑_{j∈J} b_{j}q_{j}. Since p ⊂_{→}^{2} q, for every i ∈ I there is a j_{i} ∈ J such that a_{i} = b_{j_{i}} and p_{i} ⊂_{→}^{2} q_{j_{i}}. By the induction hypothesis, p_{i} <_{∼} q_{j_{i}} can be derived from A1-4+2S. Hence, ∑_{i∈I} a_{i}p_{i} <_{∼} ∑_{i∈I} a_{i}q_{j_{i}} can be proven from A1-4+2S.

Vice versa, since q ⊂_{→}^{1} p, for each l ∈ J there is an i_{l} ∈ I such that b_{l} = a_{i_{l}} = b_{j_{i_{l}}} and q_{l} ⊂_{→}^{1} p_{i_{l}} ⊂_{→}^{2} q_{j_{i_{l}}}. By completeness of A1-4+S for the simulation preorder, b_{l}q_{l} <_{∼} a_{i_{l}}q_{j_{i_{l}}} can be derived from A1-4+S. So a_{i_{l}}q_{j_{i_{l}}} <_{∼} a_{i_{l}}q_{j_{i_{l}}} + b_{l}q_{l} can be derived using 2S. Hence, ∑_{l∈J} a_{i_{l}}q_{j_{i_{l}}} <_{∼} ∑_{j∈J} b_{j}q_{j} can be proven from A1-4+2S. As the index set {j_{i_{l}} | l ∈ J} is included in the set {j_{i} | i ∈ I}, we can derive from A1-4+2S that

∑_{i∈I} a_{i}q_{j_{i}} ≈ ∑_{i∈I} a_{i}q_{j_{i}} + ∑_{l∈J} a_{i_{l}}q_{j_{i_{l}}} <_{∼} ∑_{i∈I} a_{i}q_{j_{i}} + ∑_{j∈J} b_{j}q_{j} ≈ ∑_{j∈J} b_{j}q_{j} = q .

By transitivity we conclude that p <_{∼} q can be derived from A1-4+2S. □

The aforementioned proof system for the 2-nested simulation preorder, albeit very natural, includes the conditional axiom 2S; moreover, the condition of this axiom contains an auxiliary relation symbol that is not defined inductively on the syntax of BCCS. This raises the question of whether there exists a finite purely (in)equational axiomatization of 2-nested simulation preorder and/or equivalence at least over the language BCCS. The remainder of this study is devoted to showing that no finite (in)equational axiomatization of 2-nested simulation exists over BCCS.

5 Inaxiomatizability 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. In the lemma, and in the remainder of this paper, we let a^{0} denote 0, and a^{m+1} denote a(a^{m}).

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 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(1), q has only the termination trace a^{k}; clearly, this implies a^{k} ⊂_{→}^{2} q.

Suppose now that 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(2), 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} (and so a^{2m−1} ⊂_{→}^{2} p′), then it follows that a^{2m} ⊂_{→}^{2} p. 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. □

The idea behind the proof that the 2-nested simulation preorder is not finitely inequationally axiomatizable is as follows. Assume a finite inequational axiomatization E for BCCS 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}. So a^{2m} <_{∼} a^{2m} + a^{m} cannot be derived from E. Note that a^{2m} ⊂_{→}^{2} a^{2m} + a^{m}.

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}. 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 that a^{2m}+a^{m} ⊄_{→}^{2} C[σ(u)] holds by distinguishing two cases, depending on the form of the context C[].

– Case 1: Suppose C[] is of the form C′[b([] + r)]. Consider a transition C[σ(u)] →^{a} q′. Since C[] is of the form C′[b([] + r)], clearly there is a transition C[σ(t)] →^{a} p′ where p′ can be obtained by replacing at most one subterm σ(u) of q′ by σ(t). Since σ(t) ⊂_{→}^{2} σ(u), by Lemma 2 σ(t) and σ(u) have the same depth; so p′ and q′ have the same depth as well. Since C[σ(t)] ⇆^{2} a^{2m}, it follows that p′ ⊂_{→}^{2} a^{2m−1}. So by Lemma 2(2), depth(p′) = depth(q′) = 2m − 1. As depth(a^{m−1}) ≠ 2m − 1, by Lemma 2(2) a^{m−1} ⊄_{→}^{2} q′. This holds for all transitions C[σ(u)] →^{a} q′, and

a^{2m} + a^{m} →^{a} a^{m−1}, so a^{2m} + a^{m} ⊄_{→}^{2} C[σ(u)].

– Case 2: Suppose C[] is of the form [] + r. As ρ(t) ⊂_{→}^{2} ρ(u) for all closed substitutions ρ, by Lemma 2(2) ρ(t) and ρ(u) have the same depth for all ρ. Clearly this implies that depth(t) = depth(u), and moreover that t and u contain exactly the same variables. Since σ(t)+r ⇆^{2} a^{2m}, by Lemma 2(3) norm(σ(t)) ≥ 2m and norm(r) ≥ 2m. As σ(u) + r ⊂_{→}^{2} a^{2m} + a^{m}, again by Lemma 2(3), we have 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 termination trace of σ(u) must become, after less than m transitions, a termination 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, we have norm(σ(u) + r) > m. As a^{2m} + a^{m} has norm m, by Lemma 2(3) we may conclude that a^{2m} + a^{m} ⊄_{→}^{2} σ(u) + r. □

Remark: The inequation ax <_{∼} ax+a^{1} is sound modulo ⊂_{→}^{2}. However, a^{4} ⇆̸^{2} a^{4}+ a^{1}. So the side condition 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 3. BCCS modulo the 2-nested simulation preorder is not finitely inequationally axiomatizable.

Proof. Let E be a finite, non-empty inequational axiomatization for BCCS 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 a^{2m} + a^{m} ⊄_{→}^{2} a^{2m} (Lemma 2(3)), 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}. □

6 Inaxiomatizability of 2-nested simulation equivalence

We now proceed to prove that the 2-nested simulation equivalence is not finitely equationally axiomatizable. The following lemma will play a key role in the proof of this statement.

Lemma 5. Let the inequational axiom u <_{∼} t be sound modulo ⊂_{→}^{2}. If t is of the form ∑_{i∈I} x_{i} + ∑_{j∈J} a_{j}t_{j} and u is of the form ∑_{k∈K} y_{k} + ∑_{ℓ∈L} b_{ℓ}u_{ℓ}, then

– {y_{k} | k ∈ K} ⊆ {x_{i} | i ∈ I}, and

– for each ℓ ∈ L there is a j ∈ J such that var(t_{j}) ⊆ var(u_{ℓ}).

Proof. Let m be greater than the depth of u.

Assume, towards a contradiction, that y_{k} ∉ {x_{i} | i ∈ I} for some k ∈ K. Let σ(y_{k}) = a^{m} and let σ(z) = 0 for z ≠ y_{k}. As σ(y_{k}) →^{a} a^{m−1}, it follows that σ(u) →^{a} a^{m−1}; so σ(u) has a termination trace of length m. On the other hand, σ(x_{i}) ⇆^{2} 0 for i ∈ I, and it is easy to see that no σ(a_{j}t_{j}) for j ∈ J has a termination trace of length m; so σ(t) does not have a termination trace of length m. As σ(u) ⊂_{→}^{2} σ(t) by the soundness of u <_{∼} t, this contradicts Lemma 2(1).

Assume, towards a contradiction, that there is an ℓ ∈ L such that var(t_{j}) ⊈ var(u_{ℓ}) for all j ∈ J. Let ρ(z) = 0 for z ∈ var(u_{ℓ}) and let ρ(z) = a^{m} for z ∉ var(u_{ℓ}). Since ρ(z) = 0 for z ∈ var(u_{ℓ}), clearly depth(ρ(u_{ℓ})) ≤ depth(u)−1 < m−1. On the other hand, for all transitions ρ(t) →^{c} p′ we have depth(p′) ≥ m−1. Namely, each transition of ρ(t) is of the form ρ(t) →^{a} a^{m−1} or ρ(t) →^{a_{j}} ρ(t_{j}); by assumption, for every j ∈ J, the term t_{j} contains a variable z ∉ var(u_{ℓ}), implying that depth(ρ(t_{j})) ≥ m. Since ρ(u) ⊂_{→}^{2} ρ(t) and ρ(u) →^{b_{ℓ}} ρ(u_{ℓ}), it follows that there is a transition ρ(t) →^{b_{ℓ}} q′ with ρ(u_{ℓ}) ⊂_{→}^{2} q′. Since depth(ρ(u_{ℓ})) < m − 1 and depth(q′) ≥ m − 1, this contradicts Lemma 2(2). □

Assume a finite equational axiomatization E for BCCS that is sound modulo ⇆^{2}. The idea behind the proof that E cannot be complete modulo ⇆^{2} is as follows. We show that, if m is sufficiently large, then, for all closed derivations a(a^{2m} + a^{m}) ≈ p_{1} ≈ ⋯ ≈ p_{k} from E, p_{k} →^{a} p′_{k} implies norm(p′_{k}) = m. Clearly, a(a^{2m} + a^{m}) + a^{2m+1} does not satisfy the latter property, so a(a^{2m} + a^{m}) ≈ a(a^{2m} + a^{m}) + a^{2m+1} cannot be derived from E. Note that a(a^{2m} + a^{m}) ⇆^{2} a(a^{2m} + a^{m}) + a^{2m+1}.

Theorem 4. BCCS modulo 2-nested simulation equivalence is not finitely equationally axiomatizable.

Proof. Let E be a finite, non-empty equational axiomatization for BCCS that is sound modulo ⇆^{2}. Let m > max{depth(t) | t ≈ u ∈ E}.

First we prove the following fact: Claim: Let t ≈ u ∈ E and let σ be a closed substitution such that C[σ(t)] only has termination traces of lengths m + 1 and 2m + 1. Suppose moreover that for every transition C[σ(t)] →^{b} p′ we have norm(p′) = m. Then, for every transition C[σ(u)] →^{c} q′ we have norm(q′) = m.

Proof of the claim. First of all, note that, as C[σ(t)] ⇆^{2} C[σ(u)], by Lemma 2(1) we know that C[σ(u)] only has termination traces of lengths m + 1 and 2m + 1. We now proceed with the proof by distinguishing two cases, depending on the form of the context C[].

– Case 1: Suppose C[] is of the form C′[d([] + r)].

Consider a transition C[σ(u)] →^{c} q′. Since C[] is of the form C′[d([] + r)], clearly there is a transition C[σ(t)] →^{c} p′ where p′ can be obtained by replacing at most one subterm σ(u) of q′ by σ(t). Since σ(t) ⇆^{2} σ(u), by Lemma 2(3) σ(t) and σ(u) have the same norm; so p′ and q′ have the same norm as well. By assumption norm(p′) = m, so norm(q′) = m.

– Case 2: Suppose C[] is of the form [] + r.

Let t be of the form ∑_{i∈I} x_{i} +∑_{j∈J} a_{j}t_{j} and let u be of the form ∑_{k∈K} y_{k} + ∑_{ℓ∈L} b_{ℓ}u_{ℓ}. Consider a transition σ(u)+r →^{c} q′. We distinguish three possible cases.

– Case 2.1: Let r →^{c} q′. Then σ(t) + r →^{c} q′, which implies norm(q′) = m.

– Case 2.2: Let σ(y_{k}) →^{c} q′ for some k ∈ K. By Lemma 5, y_{k} = x_{i} for some i ∈ I, so σ(x_{i}) →^{c} q′. Then σ(t) + r →^{c} q′, which implies norm(q′) = m.

– Case 2.3: Let q′ = σ(u_{ℓ}) for some ℓ ∈ L. By Lemma 5, var(t_{j}) ⊆ var(u_{ℓ}) for some j ∈ J. Since depth(t) < m, we have depth(t_{j}) < m. On the other hand, σ(t) + r →^{a_{j}} σ(t_{j}) implies norm(σ(t_{j})) = m. Hence, each termination trace of σ(t_{j}) (so in particular its shortest one) must become, after less than m transitions, a termination trace of a σ(x) with x ∈ var(t_{j}). So norm(σ(t_{j})) = m implies norm(σ(x)) ≤ m for some x ∈ var(t_{j}). Since x ∈ var(u_{ℓ}) and depth(u_{ℓ}) < m, we have norm(σ(u_{ℓ})) < 2m. Since σ(u) only has termination traces of lengths m + 1 and 2m + 1, and moreover σ(u) →^{b_{ℓ}} σ(u_{ℓ}), it follows that σ(u_{ℓ}) can only have termination traces of lengths m and 2m. Hence, norm(σ(u_{ℓ})) = m. (End of the proof of the claim)

Suppose now that p only has termination traces of lengths m + 1 and 2m + 1. Suppose moreover that for every transition p →^{b} p′ we have norm(p′) = m. By induction on the length of equational derivations from E, using the claim that we have just proven, it is easy to show that if p ≈ q can be derived from E, then for every transition q →^{c} q′ we have norm(q′) = m.

Concluding, a(a^{2m} + a^{m}) only has termination traces of lengths m + 1 and 2m + 1. Moreover, its only transition is a(a^{2m} + a^{m}) →^{a} a^{2m} + a^{m}, and a^{2m} + a^{m} has norm m. Finally, a(a^{2m} + a^{m}) + a^{2m+1} →^{a} a^{2m}, and a^{2m} does not have norm m. So a(a^{2m} + a^{m}) ≈ a(a^{2m} + a^{m}) + a^{2m+1} cannot be derived from E. Since a(a^{2m} + a^{m}) ⇆^{2} a(a^{2m} + a^{m}) + a^{2m+1}, we may conclude that E is not complete modulo ⇆^{2}. □

7 The 3-nested simulation preorder and beyond

Groote and Vaandrager [10] actually introduced a hierarchy of n-nested simulation preorders for n ≥ 2. The following definition generalizes Definition 2.

Definition 6. For n ≥ 1, p ⊂_{→}^{n+1} q iff p R q with R a simulation and R^{−1} included in ⊂_{→}^{n}. The kernel of ⊂_{→}^{n+1} is denoted by ⇆^{n+1}.

It is easy to see that ⊂_{→}^{n+1} is included in ⇆^{n}, for n ≥ 1. The characterization of the 2-nested simulation preorder in Theorem 1 generalizes to the n-nested simulation preorders for n ≥ 3. Also, the idea behind the conditional axiomatization for the 2-nested preorder (see Theorem 2) generalizes to the n-nested simulation preorders for n ≥ 3. The proofs of these results are omitted.

Theorem 5. For n ≥ 1, and for closed process terms p and q over BCCS,

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.

Definition 7. For n ≥ 1, let <_{∼}_{n+1} be the preorder generated by the equational axioms A1-4 together with y <_{∼}_{n} x ⇒ x <_{∼}_{n+1} x + y.

Theorem 6. For n ≥ 1, and for closed process terms p and q over BCCS,

p <_{∼}_{n} q iff p ⊂_{→}^{n} q.

It follows from the proof of Theorem 4 that there does not exist a finite inequational axiomatization for the 3-nested simulation preorder.

Theorem 7. BCCS modulo the 3-nested simulation preorder is not finitely inequationally axiomatizable.

Proof. Let E be a finite inequational axiomatization for BCCS that is sound modulo ⊂_{→}^{3}. Since ⊂_{→}^{3} is included in ⇆^{2}, clearly the equational axiomatization E′ = {t ≈ u | t <_{∼} u ∈ E} is sound modulo ⇆^{2}. Let m > max{depth(t) | t ≈ u ∈ E′}. In the proof of Theorem 4 it was shown that a(a^{2m} + a^{m}) ≈ a(a^{2m} + a^{m}) + a^{2m+1} cannot be derived from E′. Hence, a(a^{2m} + a^{m}) <_{∼} a(a^{2m} + a^{m}) + a^{2m+1} cannot be derived from E. Since a(a^{2m} +a^{m}) ⊂_{→}^{3} a(a^{2m} +a^{m})+a^{2m+1}, it follows that E is not complete modulo ⊂_{→}^{3}. □

We leave it as an open question whether there exist finite equational axiomatizations for n-nested simulation equivalence if n ≥ 3, and finite inequational axiomatizations for the n-nested simulation preorder if n ≥ 4.

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 STACS, H. Reichel and S. Tison, eds., vol. 1770 of Lecture Notes in Computer Science, Springer-Verlag, Feb. 2000, pp. 267–278.

2. L. Aceto, Z. Ésik, and A. Ingólfsdóttir, The max-plus algebra of the natural numbers has no finite equational basis, research report, BRICS, Department of Computer Science, Aalborg University, October 1999. Pp. 25. To appear in Theoretical Computer Science.

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. J. Baeten and J. Klop, eds., Proceedings CONCUR 90, Amsterdam, vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990.

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

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

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

8. R. van Glabbeek, The linear time – branching time spectrum, in Baeten and Klop [4], pp. 278–297.

9. J. F. Groote, A new strategy for proving ω–completeness with applications in process algebra, in Baeten and Klop [4], pp. 314–331.

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

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

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

13. R. Milner, An algebraic definition of simulation between programs, in Proceedings 2nd Joint Conference on Artificial Intelligence, William Kaufmann, 1971, pp. 481– 489.

14. , A Calculus of Communicating Systems, vol. 92 of Lecture Notes in Computer Science, Springer-Verlag, 1980.

15. , Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

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

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

18. , 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.

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

20. V. Redko, On defining relations for the algebra of regular events, Ukrainskii Matematicheskii Zhurnal, 16 (1964), pp. 120–126. In Russian.

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

22. S. K. Shukla, D. J. Rosenkrantz, H. B. Hunt III, and R. E. Stearns, A HORNSAT based approach to the polynomial time decidability of simulation relations for finite state processes, in DIMACS Workshop on Satisfiability Problem: Theory and Applications, D. Du, J. Gu, and P. M. Pardalos, eds., vol. 35 of DI-MACS Series in Discrete Mathematics and Computer Science, 1996, pp. 603–642.

Recent BRICS Report Series Publications

RS-00-20 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. 2-Nested Simulation is not Finitely Equationally Axiomatizable. August 2000. 13 pp.

RS-00-19 Vinodchandran N. Variyam. A Note on NP ∩ coNP/poly. August 2000. 7 pp.

RS-00-18 Federico Crazzolara and Glynn Winskel. Language, Semantics, and Methods for Cryptographic Protocols. August 2000. ii+42 pp.

RS-00-17 Thomas S. Hune. Modeling a Language for Embedded Systems in Timed Automata. August 2000. 26 pp. Earlier version entitled Modelling a Real-Time Language appeared in Gnesi and Latella, editors, Fourth International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS ’99 Proceedings of the FLoC Workshop, 1999, pages 259–282.

RS-00-16 Jiří Srba. Complexity of Weak Bisimilarity and Regularity for BPA and BPP. June 2000. 20 pp. To appear in Aceto and Victor, editors, Expressiveness in Concurrency: Fifth International Workshop EXPRESS ’00 Proceedings, ENTCS, 2000.

RS-00-15 Daniel Damian and Olivier Danvy. Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation. June 2000. Extended version of an article to appear in Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming, 2000.

RS-00-14 Ronald Cramer, Ivan B. Damgård, and Jesper Buus Nielsen. Multiparty Computation from Threshold Homomorphic Encryption. June 2000. ii+38 pp.

RS-00-13 Ondřej Klíma and Jiří Srba. Matching Modulo Associativity and Idempotency is NP-Complete. June 2000. 19 pp. To appear in Mathematical Foundations of Computer Science: 25th International Symposium, MFCS ’00 Proceedings, LNCS, 2000.

RS-00-12 Ulrich Kohlenbach. Intuitionistic Choice and Restricted Classical Logic. May 2000. 9 pp.

RS-00-11 Jakob Pagter. On Ajtai’s Lower Bound Technique for R-way Branching Programs and the Hamming Distance Problem. May 2000. 18 pp.