BRICS

Basic Research in Computer Science

On the Axiomatizability of Priority

Luca Aceto Taolue Chen Willem Jan Fokkink Anna Ingólfsdóttir

BRICS Report Series RS-06-1

ISSN 0909-0878 January 2006 BRICS RS-06-1 Aceto et al.: On the Axiomatizability of Priority Copyright \begin{matrix}c \\ ◯ \end{matrix} 2006, Luca Aceto & Taolue Chen & 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 IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark

Telephone: +45 8942 9300
Telefax: +45 8942 5601
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/06/1/

On the Axiomatizability of Priority

Luca Aceto^{1,2}, Taolue Chen^{3}, Wan Fokkink^{3,4}, and Anna Ingolfsdottir^{1,2}

1 Reykjavík University, School of Science and Engineering, Ofanleiti 2,

103 Reykjavík, Iceland

2 BRICS, Aalborg University, Department of Computer Science, Fr. Bajersvej 7E,

9220 Aalborg Ø, Denmark 3 CWI, Embedded Systems Group, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands

4 Vrije Universiteit, Section Theoretical Computer Science, Boelelaan 1081a,

1081 HV Amsterdam, The Netherlands

       luca@ru.is,chen@cwi.nl,wanf@cs.vu.nl,annai@ru.is

Abstract. This paper studies the equational theory of bisimulation equivalence over the process algebra BCCSP extended with the priority operator of Baeten, Bergstra and Klop. It is proven that, in the presence of an infinite set of actions, bisimulation equivalence has no finite, sound, ground-complete equational axiomatization over that language. This negative result applies even if the syntax is extended with an arbitrary collection of auxiliary operators, and motivates the study of axiomatizations using conditional equations. In the presence of an infinite set of actions, it is shown that, in general, bisimulation equivalence has no finite, sound, ground-complete axiomatization consisting of conditional equations over the language studied in this paper. Finally, sufficient conditions on the priority structure over actions are identified that lead to a finite, ground-complete axiomatization of bisimulation equivalence using conditional equations. Keywords and Phrases: Bisimulation equivalence, priority, equational logic, conditional equational logic, complete axiomatizations, non-finitely based algebras.

1 Introduction

Programming and specification languages often include constructs to specify mode switches (see, e.g., [19, 21]). Indeed, some form of mode transfer in computation appears in operating systems in the guise of interrupts, in programming languages as exceptions, and in the behaviour of control programs and embedded systems as discrete “mode switches” triggered by changes in the state of their environment. Such mode changes are often used to encode different levels of urgency amongst the actions that can be performed by a system as it computes, and implement variations on the notion of pre-emption.

In light of the ubiquitous nature of mode changes in computation, it is not surprising that classic process description languages include primitive operators to describe mode changes—for example, LOTOS [8, 18] offers the so-called disruption operator—or have been extended with variations on mode transfer operators. Examples of such operators that may be added to the process algebra CCS are discussed by Milner in [20, pp. 192–193], and Dsouza and Bloom offer in [13] some discussion on the benefits of adding one of those, viz. the checkpointing operator, to CCS.

One of the most widely studied, and natural, notions used to implement different levels of urgency between system actions is priority. (A thorough and clear discussion of the different approaches to the study of priority in process description languages may be found in [11].) In this paper, we consider the well-known priority operator Θ studied by Baeten, Bergstra and Klop [3] in the context of process algebra. (See [9–12] for later accounts of this operator in the setting of process description languages.) The priority operator Θ gives certain actions priority over others based on an irreflexive partial ordering relation < over the set of actions. Intuitively, a < b is interpreted as “b has priority over a”. This means that, in the context of the priority operator Θ, action a is preempted by action b. For example, if p is some process that can initially perform both a and b, then Θ(p) will initially only be able to execute the action b.

In their classic paper [3], Baeten, Bergstra and Klop provided a sound and ground-complete axiomatization for this operator modulo bisimulation equivalence. Their axiomatization uses predicates on actions (to express priorities between actions) and one extra auxiliary operator. Bergstra showed in the earlier paper [5] that, in case of a finite alphabet of actions, there exists a finite equational axiomatization for Θ, without action predicates and help operators. So, if the set of actions is finite, neither conditional equations nor auxiliary operators, as used in [3], are actually necessary to obtain a finite axiomatization of bisimulation equivalence over basic process description languages enriched with the priority operator. But, can Bergstra’s positive result be extended to a setting with a countably infinite collection of actions? Or are conditional equations and auxiliary operators necessary to obtain a finite axiomatization of bisimulation equivalence in the presence of an infinite collection of actions? (Note that infinite sets of actions are common in process calculi, and arise, for instance, in the setting of value- or name-passing calculi.) The aim of this paper is to provide a thorough answer to these questions in the setting of the process algebra BCCSP enriched with the priority operator Θ. In case of an infinite alphabet, we permit the occurrence of action variables in axioms.

The process algebra BCCSP contains only basic process algebraic operators from CCS and CSP, but is sufficiently powerful to express all finite synchronization trees. This paper considers the equational theory of BCCSP with the priority operator Θ from [3] modulo bisimulation equivalence. Our first main result is a theorem indicating that the use of conditional equations is indeed inevitable in order to offer a finite axiomatization of bisimulation equivalence over the basic process language we consider in this study. To this end, we prove that, in case of an infinite alphabet and in the presence of at least one priority relation a < b between a pair of actions, there is no finite equational axiomatization for BCCSP enriched with the priority operator (Theorem 2). This result even applies if one is allowed to add an arbitrary collection of help operators to the syntax. Theorem 2 offers a very strong indication that the use of conditional equations, where the conditions consist of action predicates, is essential for axiomatizing Θ, and cannot be circumvented by introducing auxiliary operators. (This is in contrast to the classic positive and negative results on the existence of finite equational axiomatizations for parallel composition offered in [6, 22, 23].)

The idea underlying the proof of Theorem 2 is that for each finite sound equational axiomatization E there is a pair of actions c, d that does not occur in E. If c and d are incomparable, then

Θ(c.0 + d.0) ≈ c.0 + d.0

is sound modulo bisimulation equivalence. However, using a simple renaming argument, we show that a derivation of this equation from E would give rise to a derivation of the unsound equation Θ(a.0+b.0) ≈ a.0+b.0. Likewise, if c < d, then

Θ(c.0 + d.0) ≈ d.0

is sound modulo bisimulation equivalence. But we prove that a derivation of this equation from E would give rise to a derivation of the unsound equation Θ(d.0 + c.0) ≈ c.0.

Having established that conditional equations are necessary in order to obtain a finite, ground-complete equational axiomatization of bisimulation equivalence, we then proceed to investigate whether, in the presence of an infinite set of actions, this equivalence can be finitely axiomatized using conditional equations, but without auxiliary operators like the unless operator used in [3]. We show that, in general, the answer to this question is negative. This we do by exhibiting a priority structure with respect to which bisimulation equivalence affords no finite, sound and ground-complete axiomatization in terms of conditional equations (Theorem 3). This shows that, in general, the use of auxiliary operators is indeed necessary to axiomatize bisimulation equivalence finitely, even using conditional equations and over the simple language considered in this study. The priority structure used in the proof of Theorem 3 consists of actions a_{i} and b_{i} for i ≥ 1 together with an action c, where a_{i} < b_{i} < c for each i ≥ 1. We prove that given a finite sound conditional axiomatization E, the sound equation

Θ(b_{1}.0 + ⋯ + b_{n}.0) ≈ b_{1}.0 + ⋯ + b_{n}.0

cannot be derived from E, for a sufficiently large n.

In contrast to the aforementioned negative results, we exhibit a countably infinite, ground-complete axiomatization for bisimulation equivalence over BCCSP with the priority operator in terms of conditional equations (Theorem 4). This axiomatization suggests that infinite collections of pairwise incomparable actions with respect to the priority relation < are the source of our negative result presented in Theorem 3. It is therefore natural to ask ourselves whether there are conditions that can be imposed on the poset of actions that are sufficient to guarantee that bisimulation equivalence be finitely axiomatizable using conditional equations, but without auxiliary operators. We conclude the technical developments in this paper by proposing some such sufficient conditions. The most general of these applies to all priority structures such that

1. the collection of the sizes of the finite, maximal anti-chains is finite,

2. there are only finitely many infinite, maximal anti-chains, and

3. for each infinite, maximal anti-chain A each element of A is above the same set of actions—that is, for each a, b ∈ A and action c, we have that c < a iff c < b.

Our results add the priority operator to the list of operators whose addition to a process algebra spoils finite axiomatizability modulo bisimulation equivalence; see, e.g., [1, 2, 22–24] for other examples of non-finite axiomatizability results over process algebras. Notably, in [2] two mode transfer operators from [4] are studied in the setting of the basic process algebra BPA. It is shown that, even in the presence of just one action, the interrupt operator does not have a finite equational axiomatization, while the disrupt operator does. In the interrupt operator, a process p can be interrupted by another process q; upon termination of q, process p resumes its computation. In the disrupt operator, a process p can be pre-empted by another process q, after which the execution of p is aborted.

This paper is organized as follows. Section 2 contains the preliminaries. In Section 3, the finite axiomatization for the priority operator Θ from [5] is presented. Section 4 contains a proof of a result to the effect that, in case of an infinite alphabet, there is no finite equational axiomatization for the priority operator modulo bisimulation equivalence, even in the presence of auxiliary operators. Finally, we show that, in the presence of an infinite set of actions, in general bisimulation equivalence does not afford a finite axiomatization in terms of conditional equations without the use of auxiliary operators (Section 5.1), and we identify sufficient conditions on the priority structure over actions that lead to the existence of a finite conditional axiomatization (Section 5.2).

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_{Θ}

Act denotes a non-empty alphabet of atomic actions, with typical elements a, b, c, d, e. Over Act we assume an irreflexive, transitive partial ordering < to express priorities between actions. Intuitively, a < b expresses that the action b has priority over the action a. We say that actions a_{1}, …, a_{n} are incomparable if they are distinct and a_{i} < a_{j} does not hold for all 1 ≤ i, j ≤ n.

The language of processes we shall consider in this paper, henceforth referred to as BCCSP_{Θ}, is obtained by adding the unary priority operator Θ from [3] to the basic process algebra BCCSP [14, 15]. The language is given by the following grammar:

t ::= 0 | a.t | t + t | Θ(t) | x | α.t ,

where a ranges over Act, x is a process variable and α is an action variable. Process and action variables range over given, disjoint countably infinite sets. We use x, y, z to range over the collection of process variables, and α, β as typical action variables.

We use t, u, v to range over the collection of open process terms 𝕋(BCCSP_{Θ}). A process term is closed if it does not contain any variables, and p, q, r, range over the set of closed terms T(BCCSP_{Θ}). The size of a term is its length in function symbols.

Remark 1. The reader familiar with [14, 15] might have already noticed that we consider a slightly extended syntax for BCCSP, in that we allow for the use of prefixing operators of the form α. , where α is an action variable. The use of action variables is natural in the presence of infinite sets of actions, and will allow us to formulate stronger versions of the negative results to follow.

A substitution maps each process variable to a process term, and each action variable to an action or action variable. A substitution is closed if it maps process variables to closed process terms and action variables to actions. For every term t and substitution σ, the term obtained by replacing occurrences of process variables x and action variables α in t with σ(x) and σ(α), respectively, is written σ(t). Note that σ(t) is closed if so is σ. For example, σ(α.x) = a.0 if σ(α) = a and σ(x) = 0.

In general, for each signature Σ—that is, a collection of function symbols together with their arity—, 𝕋(Σ) denotes the collection of open terms over Σ, and T(Σ) stands for the collection of closed terms over Σ. In Section 4, we shall consider signatures extending that for the language BCCSP_{Θ}.

The semantics of the operators is captured by the transition rules below, which give rise to Act-labelled transitions between closed terms. An Act-labelled transition between closed terms is a triple (p, a, p′), where p, p′ are closed terms and a ∈ Act. Henceforth, as usual, we shall use the suggestive notation p →^{a} p′ in lieu of (p, a, p′). A transition relation is a collection of Act-labelled transitions.

The operational semantics for the language BCCSP_{Θ} is given by the labelled transition system

(T(BCCSP_{Θ}), →) ,

where the transition relation → is the unique supported model of the following rules in the sense of [7]:

\overline{a.x →^{a} x} \frac{x_{1} →^{a} y}{x_{1} + x_{2} →^{a} y} \frac{x_{2} →^{a} y}{x_{1} + x_{2} →^{a} y} \frac{x →^{a} y x ↛^{b} for a < b}{Θ(x) →^{a} Θ(y)}

where a ranges over Act. It is well-known that the transition relation → is the one defined by structural induction over closed terms using the above rules.

Intuitively, closed terms in the language BCCSP_{Θ} represent finite process behaviours, where 0 does not exhibit any behaviour, p+q is the nondeterministic choice between the behaviours of p and q, and a.p executes action a to transform into p. Furthermore, the process graph of Θ(p) is obtained by eliminating all transitions q →^{a} q′ from the process graph of p for which there is a transition

q →^{b} q′′ with a < b.

We consider the language BCCSP_{Θ} modulo bisimulation equivalence.

Definition 1. A binary symmetric relation R over T(BCCSP_{Θ}) is a bisimulation if p R q together with p →^{a} p′ imply q →^{a} q′ for some q′ with p′ R q′. We write p \underline{↔} q if there is a bisimulation relating p and q. The relation \underline{↔} will be referred to as bisimulation equivalence or bisimilarity.

It is well-known that \underline{↔} is an equivalence relation. Moreover, the transition rules are in the GSOS format of [7]. Hence, bisimulation equivalence is a congruence with respect to all the operators in the signature of BCCSP_{Θ}, meaning that p \underline{↔} q implies C[p] \underline{↔} C[q] for each BCCSP_{Θ}-context C[].

We can therefore consider the algebra of the closed terms in T(BCCSP_{Θ}) modulo \underline{↔}. In Section 4, we shall offer results that apply to any signature Σ that extends that for BCCSP_{Θ}. To this end, we shall tacitly assume that all of the new operators in Σ also preserve bisimulation equivalence, and are semantically interpreted as operations over finite synchronization trees [20].

2.2 Equational Logic

An axiom system is a collection of equations t ≈ u over the language BCCSP_{Θ}. An equation t ≈ u is derivable from an axiom system E, notation E ⊢ t ≈ u, if it can be proven from the axioms in E using the rules of equational logic (viz. reflexivity, symmetry, transitivity, substitution and closure under BCCSP_{Θ} contexts):

\overline{t ≈ t}  \frac{t ≈ u}{u ≈ t}  \frac{t ≈ u u ≈ v}{t ≈ v}  \frac{t ≈ u}{σ(t) ≈ σ(u)}

\frac{t ≈ u t′ ≈ u′}{t + t′ ≈ u + u′} \frac{t ≈ u}{a.t ≈ a.u} \frac{t ≈ u}{α.t ≈ α.u} \frac{t ≈ u}{Θ(t) ≈ Θ(u)}

Without loss of generality one may assume that substitutions happen first in equational proofs, i.e., that the rule

\frac{t ≈ u}{σ(t) ≈ σ(u)}

may only be used when t ≈ u ∈ E. Moreover, by postulating that for each axiom in E also its symmetric counterpart is present in E, we can disregard applications of symmetry in equational proofs. In the remainder of this paper, we shall tacitly assume that our equational axiom systems are closed with respect to symmetry. Furthermore, it is well-known (cf., e.g., Section 2 in [16]) that if an equation relating two closed terms can be proven from an axiom system E, then there is a closed proof for it. (A proof is closed if it only mentions closed terms.) We shall only consider questions related to the provability of closed equations from an axiom system. Therefore, in light of the previous observation, we can restrict ourselves to considering closed proofs.

Definition 2. An equation t ≈ u is sound with respect to \underline{↔} if σ(t) \underline{↔} σ(u) holds for each closed substitution σ. An axiom system E is called sound over some language modulo \underline{↔} if E ⊢ t ≈ u implies t \underline{↔} u, for all terms t, u in the language. Conversely, E is called ground-complete if p \underline{↔} q implies E ⊢ p ≈ q, for all closed terms p, q in the language.

Our order of business in the remainder of this paper will be to offer a thorough study of the equational theory of the language BCCSP_{Θ} modulo bisimulation equivalence. We begin our investigation by considering the case in which the set of actions Act is finite in the following section. We then move on to investigate the equational properties of bisimulation equivalence over BCCSP_{Θ} when the set of actions is infinite (Sections 4 and 5).

3 |Act | < ∞

In this section, we assume that the action set is finite. The axiom system in Table 1 was put forward by Jan Bergstra in [5]. Note that in the case of a finite action set, this axiom system is finite, since then the axiom schemas PR2–4 give rise to finitely many equations.

A1  x + y ≈ y + x
A2  x + (y + z) ≈ (x + y) + z
A3  x + x ≈ x
A4  x + 0 ≈ x
PR1  Θ(0) ≈ 0
PR2  Θ(a.x + a.y + z) ≈ Θ(a.x + z) + Θ(a.y + z)
PR3  Θ(a.x + b.y + z) ≈ Θ(b.y + z)  (a < b)
PR4 Θ(a_{1}.x_{1} + ⋯ + a_{n}.x_{n}) ≈ a_{1}.Θ(x_{1}) + ⋯ + a_{n}.Θ(x_{n})
(a_{1}, …, a_{n} incomparable)

Table 1. Axiomatization in case of |Act| < ∞

Theorem 1 (Bergstra [5]). The axiom system consisting of the equations (A1)–(A4) and (PR1)–(PR4) is sound and ground-complete for BCCSP_{Θ} modulo \underline{↔}.

Proof. (Sketch) Since \underline{↔} is a congruence with respect to BCCSP_{Θ}, soundness can be checked for each axiom separately. This is an easy exercise.

Next observe that, using (PR1)–(PR4), one can remove all occurrences of Θ from closed terms. Then ground-completeness follows from the well-known ground-completeness of (A1)–(A4) for BCCSP modulo \underline{↔} (see, e.g., [17]). ⊓ ⊔

In the remainder of this paper, process terms are considered modulo associativity and commutativity of +. In other words, we do not distinguish t+u and u+t, nor (t + u) + v and t + (u + v). We use a summation ∑_{i=1}^{n} t_{i} to denote t_{1} + ⋯ + t_{n}, where the empty sum represents 0. Such a summation is said to be in head normal form if each term t_{i} is of the form a_{i}.t′_{i} or α_{i}.t′_{i} for some action a_{i} or action variable α_{i}, and term t′_{i}.

It is easy to see that modulo the axioms (A1) and (A2), every term t in the language BCCSP_{Θ} has the form ∑_{i∈I} t_{i}, for some finite index set I, and terms t_{i} (i ∈ I) that are do not have the form t′ + t′′. The terms t_{i} (i ∈ I) will be referred to as the summands of t. For example, the term Θ(a.0 + b.0) has only itself as summand.

Remark 2. Note that the axiom system in Table 1 is not strong enough to prove all of the sound equations over the language BCCSP_{Θ} modulo bisimulation equivalence. For instance, as our readers can check, the equation

Θ(Θ(x) + y) ≈ Θ(x + y)

is sound modulo bisimulation equivalence irrespective of the cardinality of the set of actions Act and of the ordering relation <. That equation, however, cannot be proven from those in Table 1.

4 |Act | = ∞

In this section, we deal with the case that the action set is infinite. Our main result is that bisimulation equivalence does not afford a finite equational axiomatization over the language BCCSP_{Θ}, provided that Act contains at least two actions a, b with a < b. (Otherwise, the equation Θ(x) ≈ x would be sound, and the priority operator could be eliminated from all terms.) This negative result even applies if BCCSP_{Θ} is extended with an arbitrary collection of operators (over finite synchronization trees) for which bisimulation equivalence is a congruence.

The idea behind the proof of our main result of this section is that a finite axiom system E can mention only finitely many action names. So, since Act is infinite, we can find a pair c, d of distinct actions that do not occur in E. If c and d are incomparable, then the equation Θ(c.0 + d.0) ≈ c.0 + d.0 is sound; if c < d, then Θ(c.0 + d.0) ≈ d.0 is sound. In the first case, we show that an equational proof of Θ(c.0 + d.0) ≈ c.0 + d.0 from E would give rise to a proof of the unsound equation Θ(a.0 + b.0) ≈ a.0 + b.0 from E. This follows by a simple renaming argument, using that c and d do not occur in E. Likewise, in the second case, a proof of Θ(c.0 + d.0) ≈ d.0 from E would give rise to a proof of the unsound equation Θ(d.0 + c.0) ≈ c.0 from E.

To present the formal proof of the aforementioned negative result, first we introduce the action renaming mentioned in the proof idea sketched above.

Definition 3. Let A ⊆ Act, and let Σ be a signature that includes the set of operators in BCCSP_{Θ}. We extend each renaming function ρ : A → Act to a function ρ : 𝕋(Σ) → 𝕋(Σ) as follows, where f is any operator that is not of the form a. .

ρ(0) =^{def} 0
ρ(a.t) =^{def} \{ \begin{matrix}ρ(a).ρ(t) if a ∈ A \\ a.ρ(t) if a ∉ A \end{matrix}
ρ(f(t_{1}, …, t_{n})) =^{def} f(ρ(t_{1}), …, ρ(t_{n}))
ρ(x) =^{def} x
ρ(α.t) =^{def} α.ρ(t)

For each substitution σ, the substitution ρ(σ) is defined by ρ(σ)(x) =^{def} ρ(σ(x)) and

ρ(σ)(α) =^{def} \begin{cases}ρ(σ(α)) & if σ(α) ∈ A \\ σ(α) & otherwise . \end{cases}

The following lemma states that renaming of actions that are not mentioned in an axiom system E preserves provability.

Lemma 1. Let A ⊆ Act and ρ : A → Act. Let Σ be a signature that includes the set of operators in BCCSP_{Θ}. Let E be a collection of equations over Σ, and assume that all of the actions a ∈ A do not occur in E. Then E ⊢ p ≈ q implies E ⊢ ρ(p) ≈ ρ(q).

Proof. The proof is by induction on the depth of a closed proof of the equation p ≈ q from E. We proceed by a case analysis on the last rule used in the proof of p ≈ q from E. The case of reflexivity is trivial, and that of transitivity follows immediately by using the induction hypothesis. Below we only consider the other cases, namely the instantiation of an axiom and closure under contexts. (Since we are dealing with closed proofs, closure with respect to prefixing by action variables need not be considered.)

– Case E ⊢ p ≈ q because σ(t) = p and σ(u) = q for some equation t ≈ u ∈ E and closed substitution σ. Then ρ(p) = ρ(σ(t)) = ρ(σ)(ρ(t)). According to the proviso of the lemma, no action a ∈ A occurs in t, so clearly ρ(t) = t. Similarly, ρ(q) = ρ(σ(u)) = ρ(σ)(ρ(u)) = ρ(σ)(u). Since t ≈ u ∈ E, by substitution instance, E ⊢ ρ(σ)(t) ≈ ρ(σ)(u). In other words, E ⊢ ρ(p) ≈ ρ(q), which was to be shown.

– Case E ⊢ p ≈ q because p = a.p′ and q = a.q′ where E ⊢ p′ ≈ q′. If a ∈ A, then ρ(p) = ρ(a).ρ(p′) and ρ(q) = ρ(a).ρ(q′); otherwise, ρ(p) = a.ρ(p′) and ρ(q) = a.ρ(q′). In either case, by induction, E ⊢ ρ(p′) ≈ ρ(q′). By context closure, E ⊢ ρ(p) ≈ ρ(q).

– Case E ⊢ p ≈ q because p = f(p_{1}, …, p_{n}) and q = f(q_{1}, …, q_{n}), for some operator f in the signature that is not of the form a. , where E ⊢ p_{i} ≈ q_{i} for i = 1, …, n. By definition, ρ(p) = f(ρ(p_{1}), …, ρ(p_{n})) and ρ(q) = f(ρ(q_{1}), …, ρ(q_{n})). By induction, E ⊢ ρ(p_{i}) ≈ ρ(q_{i}) for i = 1, …, n. By context closure, E ⊢ ρ(p) ≈ ρ(q). ⊓ ⊔

We are now in a position to show the first main result of this paper.

Theorem 2. Let |Act| = ∞, and a < b for some a, b ∈ Act. Let Σ be a signature consisting of the operators in BCCSP_{Θ}, together with auxiliary operators for which bisimulation equivalence is a congruence. Then bisimulation equivalence has no finite, sound and ground-complete axiomatization over T(Σ).

Proof. We need to show that no finite axiom system is both sound and groundcomplete for T(Σ) modulo \underline{↔}. Let E be a finite axiom system over T(Σ) that is sound modulo \underline{↔}. Fix a pair of distinct actions c, d ∈ Act that do not occur in E. We can select c, d such that either they are incomparable, or c < d. In the first case, the following equation is sound modulo \underline{↔}:

Θ(c.0 + d.0) ≈ c.0 + d.0 .

Assume, towards a contradiction, that this equation can be derived from E. Consider the renaming function ρ defined as: ρ(c) = a and ρ(d) = b. Since c, d do not occur in E, Lemma 1 yields that E ⊢ ρ(Θ(c.0+d.0)) ≈ ρ(c.0+d.0). That is, E ⊢ Θ(a.0 + b.0) ≈ a.0 + b.0, which is not sound modulo \underline{↔}, since a < b. This contradicts the soundness of E.

In the second case, the following equation is sound modulo \underline{↔}:

Θ(c.0 + d.0) ≈ d.0 .

Again, assume, towards a contradiction, that this equation can be derived from E. Consider the renaming function ρ defined as: ρ(c) = d and ρ(d) = c. Since c, d do not occur in E, Lemma 1 yields that E ⊢ ρ(Θ(c.0 + d.0)) ≈ ρ(d.0). That is, E ⊢ Θ(d.0 + c.0) ≈ c.0, which is not sound modulo \underline{↔}. Once more, this contradicts the soundness of E.

In either case, we can conclude that the axiom system E is not groundcomplete. ⊓ ⊔

5 Axiomatizing Priority over an Infinite Action Set, Conditionally

Theorem 2 offers very strong evidence that, in the presence of an infinite set of actions, equational logic is inherently not sufficiently powerful to achieve a finite axiomatization of bisimilarity over closed terms in the language BCCSP_{Θ}. Indeed, that result holds true even in the presence of an arbitrary number of auxiliary operators.

In the presence of action variables, it is natural to view our language as consisting of two sorts: one for actions and the other for processes. This is all the more true because the set of actions has the structure of a partial order, and we should like to express axioms over processes that reflect the influence that this poset structure on actions has on the behaviour of processes. In case our set of actions is finite, this can be done by means of a finite number of equations that are instances of (PR3) and (PR4) in Table 1.

In the presence of an infinite action set, however, the axiom schemas (PR3) and (PR4), as well as (PR2), have infinitely many instances. One way to capture their effects finitely is to take seriously the idea that, in the presence of action variables, the equation schemas (PR3) and (PR4) can be phrased as conditional equations thus:

(CPR3) (α < β) ⇒ Θ(α.x + β.y + z) ≈ Θ(β.y + z)

(CPR4)_{n} ( ⋀_{1≤i,j≤n}¬(α_{i} < α_{j})) ⇒

Θ(α_{1}.x_{1} + ⋯ + α_{n}.x_{n}) ≈ α_{1}.Θ(x_{1}) + ⋯ + α_{n}.Θ(x_{n}) (n ≥ 0) .

In both of the above conditional equations, we use predicates over actions to restrict the applicability of the equation on the right-hand side of the implication. In general, henceforth in this study we shall consider conditional equations of the form

P ⇒ t ≈ u ,

where P is a predicate over actions, and t ≈ u is an equation over the language BCCSP_{Θ}. In what follows, we shall assume that predicates over actions are expressed using formulae in first-order logic with equality and the binary relation symbol <.

The semantics of a predicate P is given by the collection of closed substitutions that satisfy it. The definition of the collection of closed substitutions that satisfy a predicate P is entirely standard, and we omit the details. For example, a closed substitution σ satisfies the predicate α < β if, and only if, σ(α) < σ(β) holds in the poset (Act, <). We sometimes write σ(P) = true if the closed substitution σ satisfies the predicate P. We say that a predicate is satisfiable if some closed substitution satisfies it. If P is a tautology, then we simply write t ≈ u. For instance, a version of of equation (PR2) with action variables will be written thus:

(CPR2) Θ(α.x + α.y + z) ≈ Θ(α.x + z) + Θ(α.y + z) .

Note that equation (PR1) in Table 1 is just (CPR4)_{0}. Moreover, since < is irreflexive, the conditional equation (CPR4)_{1} reduces to

Θ(α.x) ≈ α.Θ(x) .  (1)

(Note that the above equation can be derived from each of the (CPR4)_{n} with n ≥ 1 and axiom (A3) in Table 1.)

A conditional equation P ⇒ t ≈ u is sound with respect to bisimilarity, if σ(t) \underline{↔} σ(u) holds for each closed substitution σ that satisfies the predicate P. It is not hard to see that:

Lemma 2. For each partial order of actions (Act, <), the conditional equations (CPR2), (CPR3) and (CPR4)_{n} (n ≥ 0) are sound modulo bisimilarity over the language BCCSP_{Θ}.

A proof of an equation from a set of conditional axioms E in conditional equational logic uses the same rules presented in Section 2.2. However, the rule for substitution instance now reads

\frac{P ⇒ t ≈ u}{σ(t) ≈ σ(u)} (σ(P) = true) ,

where P ⇒ t ≈ u is one of the conditional equations in the set E. Again, by postulating that for each conditional equation P ⇒ t ≈ u in E also its symmetric counterpart P ⇒ (u ≈ t) is present in E, we can disregard applications of symmetry in conditional equational proofs.

A natural question to ask at this point, and one that we shall address in the remainder of this study, is whether, unlike standard equational logic, conditional equations suffice to obtain a finite, ground-complete axiomatization of bisimulation equivalence over the language BCCSP_{Θ}.

In their classic paper [3], Baeten, Bergstra and Klop offered a finite, conditional, ground-complete axiomatization of bisimilarity over the language BPA_{δ} with the priority operator. Their axiomatization, however, relied upon the introduction of a binary auxiliary operator, the so-called unless operator ◁. Operationally, the behaviour of the unless operator is specified by the rules

\frac{x →^{a} x′ y ↛^{b} for a < b}{x ◁ y →^{a} x′} ,

where a ∈ Act.

In the setting of BCCSP_{Θ}, and using action variables in lieu of concrete action names, the relation between the priority operator and the unless operator is expressed by the conditional equations in Table 2. It is not too hard to see that those conditional equations, together with (A1)–(A4) in Table 1, yield a groundcomplete, finite, conditional equational axiomatization of bisimulation equivalence. Therefore, even in the presence of an infinite set of actions, bisimulation equivalence affords a finite, ground-complete axiomatization using conditional equations at the price of introducing a single auxiliary operator. But, if the set of actions is infinite, is the use of an auxiliary operator like the unless operator necessary to obtain a finite axiomatizability result for bisimulation equivalence over BCCSP_{Θ} using conditional equations? We address this question in what follows. In particular, we first show that, in general, the use of auxiliary operators

Θ(α.x) ≈ α.x
Θ(0) ≈ 0
Θ(x + y) ≈ (Θ(x) ◁ y) + (Θ(y) ◁ x)
¬(α < β) ⇒ (α.x) ◁ (β.y) ≈ α.x
(α < β) ⇒ (α.x) ◁ (β.y) ≈ 0
(α.x) ◁ 0 ≈ α.x
0 ◁ (α.x) ≈ 0
(x + y) ◁ z ≈ (x ◁ z) + (y ◁ z)
x ◁ (y + z) ≈ (x ◁ y) ◁ z

Table 2. Axioms for Θ in the presence of ◁

is indeed necessary to obtain a finite, ground-complete axiomatization of bisimulation equivalence using conditional equations. This we do in Section 5.1 by exhibiting a poset of actions for which no finite set of sound conditional equations is ground-complete with respect to bisimulation equivalence over BCCSP_{Θ}. This negative result, however, does not entail that, in the presence of an infinite set of actions, auxiliary operators are always needed to give a finite, ground-complete axiomatization of bisimulation equivalence over the language BCCSP_{Θ}. In fact, we then isolate sufficient conditions on the priority structure over actions that guarantee the finite axiomatizability of bisimulation equivalence over the language BCCSP_{Θ} using conditional equations (Section 5.2).

5.1 A Negative Result

Our order of business will now be to prove that, in the presence of an infinite set of actions, in general auxiliary operators are indeed necessary in order to obtain a finite ground-complete axiomatization of bisimulation equivalence over the language BCCSP_{Θ}. In this section, Act = {a_{i}, b_{i} | i ≥ 1}∪{c}, where a_{i} < b_{i} < c for each i ≥ 1, and these are the only inequalities. Moreover, for convenience, we consider terms not only modulo associativity and commutativity of +, but also modulo the sound equations x + 0 ≈ x and Θ(Θ(x) + y) ≈ Θ(x + y)— see Remark 2. So we can assume, without loss of generality, that terms contain neither redundant 0 summands nor nested occurrences of Θ.

We will prove the following claim, which will be used to argue that bisimulation equivalence has no finite, ground-complete axiomatization over the language BCCSP_{Θ} consisting of conditional equations (Theorem 3 to follow).

Claim. Let E be a finite collection of conditional equations that is sound modulo \underline{↔}. Let n ≥ 2 be larger than the size of any term in the equations of E. Then from E we cannot derive the equation

Θ(Φ_{n}) ≈ Φ_{n} ,

where Φ_{n} denotes ∑_{i=1}^{n} b_{i}.0.

Note that the equation above is sound modulo \underline{↔}, because the actions b_{i} (i ≥ 1) are pairwise incomparable.

First we establish a technical lemma.

Lemma 3. Let P ⇒ t ≈ u be a conditional equation that is sound modulo \underline{↔}, where P is satisfiable. If some process variable x occurs as a summand in t, then x also occurs as a summand in u.

Proof. Since P is satisfiable, there exists a closed substitution σ such that σ(P) = true. Take some action d ∈ Act that does not occur in σ(u); such an action exists because Act is infinite. Consider the closed substitution σ′ that maps x to d.(b_{1}.0 + c.0), each other process variable to 0, and agrees with σ on action variables. As P ⇒ t ≈ u is sound modulo \underline{↔} and σ′(P) = σ(P) = true, we have that σ′(t) \underline{↔} σ′(u). Since x is a summand of t and σ′(t) →^{d} b_{1}.0 + c.0, it follows that σ′(u) →^{d} q \underline{↔} b_{1}.0 + c.0 for some q. Since d does not occur in σ(u) and b_{1} < c, it is not hard to see that x must be a summand of u. ⊓ ⊔

The following lemma is the crux in the proof of our claim. It states a property of closed terms that holds for all of the closed instantiations of axioms in any finite, sound collection of conditional equations. As we shall see later on, this property is also preserved by arbitrary conditional equational proofs from a finite, sound collection of conditional equations (Proposition 1).

Lemma 4. Let P ⇒ t ≈ u be a conditional equation that is sound modulo \underline{↔}. Let σ be a closed substitution with σ(P) = true. Assume that:

– n is larger than the size of t, where n ≥ 2; and

– the summands of σ(t) are all bisimilar to either Φ_{n} or 0.

Then the summands of σ(u) are all bisimilar to either Φ_{n} or 0.

Proof. First, suppose that all summands of σ(t) are bisimilar to 0. Then σ(t) \underline{↔} 0, so the soundness of P ⇒ t ≈ u together with σ(P) = true yields σ(u) \underline{↔} 0. This means that all summands of σ(u) are bisimilar to 0, and we are done.

So we can assume that some summand of σ(t) is bisimilar to Φ_{n}. Then σ(t) \underline{↔} σ(u) \underline{↔} Φ_{n}, by the proviso of the lemma and the soundness of P ⇒ t ≈ u.

We know that we can write t = ∑_{i∈I} t_{i} and u = ∑_{j∈J} u_{j} for some nonempty, finite index sets I and J, where the terms t_{i} and u_{j} are of the form x, a.v, α.v or Θ(v). By the proviso of the lemma, for each i ∈ I, the summands of σ(t_{i}) are all bisimilar to Φ_{n} or 0. Since n ≥ 2, for each i ∈ I, the term t_{i} is not of the form a.v or α.v. Hence either it is a process variable x, or it is of the form

Θ( ∑_{ℓ∈L_{i}} d_{iℓ}.t′_{iℓ} + ∑_{m∈M_{i}} α_{m}.t′′_{im} + ∑_{k∈K_{i}} z_{ik})

(modulo the equations x+0 ≈ x and Θ(Θ(x)+y) ≈ Θ(x+y)). Let I′ ⊆ I be the set of indices of summands of t that have the above form. Observe that K_{i} ≠ ∅ for each i ∈ I′ such that σ(t_{i}) is bisimilar to Φ_{n} (because n is larger than the size of t). Note moreover that summands t_{i} of t having the above form such that σ(t_{i}) \underline{↔} 0 must have L_{i} = M_{i} = ∅, and for such summands σ(z_{ik}) \underline{↔} 0 for each k ∈ K_{i}.

Let us assume, towards a contradiction, that there is an index j ∈ J such that σ(u_{j}) has a summand that is bisimilar neither to Φ_{n} nor to 0. We proceed by a case analysis on the form of u_{j}.

1. Case u_{j} = x. By assumption, σ(x) has a summand that is bisimilar neither to Φ_{n} nor to 0. Since P ⇒ t ≈ u is sound modulo \underline{↔} and P is satisfiable (because σ(P) = true by the proviso of the lemma), by Lemma 3, t also has x as a summand. Consequently σ(t) has a summand that is bisimilar neither to Φ_{n} nor to 0. This contradicts one the assumptions of the lemma.

2. Case u_{j} = a.u′_{j} or u_{j} = α.u′_{j}. Since σ(u) \underline{↔} Φ_{n}, we have that a = b_{h} or σ(α) = b_{h} for some 1 ≤ h ≤ n. Define the substitution σ′ as

σ′(y) = \{ \begin{matrix}c.0 & if y = z_{ik} for some i ∈ I′ and k ∈ K_{i} \\ 0 & otherwise \end{matrix}

for process variables y, and let σ′ agree with σ on action variables. Then

σ′(t) ↛^{b_{h}}, because

– c > b_{h},

– K_{i} ≠ ∅ for every i ∈ I′ with σ(t_{i}) \underline{↔} Φ_{n},

– L_{i} = M_{i} = ∅ for every i ∈ I′ with σ(t_{i}) \underline{↔} 0 and

– t does not contain summands of the form b_{h}.v or α.v. On the other hand, as σ and σ′ agree on action variables, σ′(u_{j}) →^{b_{h}} σ′(u′_{j}). It

follows that σ′(u) →^{b_{h}} σ′(u′_{j}), and thus σ′(t) \underline{↔} / σ′(u). Since σ′(P) = σ(P) = true, this contradicts the soundness of P ⇒ t ≈ u modulo \underline{↔}.

3. Case u_{j} = Θ(u′). Then u_{j} consists of a single summand, so by assumption, σ(u_{j}) \underline{↔} / Φ_{n} and σ(u_{j}) \underline{↔} / 0. Since σ(u) \underline{↔} Φ_{n}, and terms are considered modulo the equations x + 0 ≈ x and Θ(Θ(x) + y) ≈ Θ(x + y), we can take u′ to be of the form

∑_{ℓ∈L} e_{ℓ}.u′_{ℓ} + ∑_{m∈M} β_{m}.u′′_{m} + ∑_{k∈K} y_{k} ,

for some finite index sets L, M, K. We distinguish two cases.

(a) For each i ∈ I′ with σ(t_{i}) \underline{↔} / 0 there is a k_{i} ∈ K_{i} such that z_{ik_{i}} is not a summand of u′. Define the substitution σ′ as

σ′(y) = \{ \begin{matrix}c.0 & if y = z_{ik_{i}} for some i ∈ I′ with σ(t_{i}) \underline{↔} / 0, or \\ & if y is a summand of t with σ(y) \underline{↔} / 0 \\ σ(y) & otherwise \end{matrix}

for process variables y, and let σ′ agree with σ on action variables. It is not hard to see that σ′(t) ↛^{b_{i}} for i = 1, …, n (because c > b_{i} and t has no summand of the form a.v or α.v). On the other hand, since σ(u_{j}) \underline{↔} / 0 and σ(u) \underline{↔} Φ_{n}, there is an h with 1 ≤ h ≤ n such that σ(u′) →^{b_{h}}. Furthermore, σ(u′) ↛^{c}. By assumption, z_{ik_{i}} is not a summand of u′ for each i ∈ I′ with σ(t_{i}) \underline{↔} / 0. Moreover, for any variable summand y of t with σ(y) \underline{↔} / 0, y is not a summand of u′, because by assumption σ(y) \underline{↔}

Φ_{n} while σ(u′) \underline{↔} / Φ_{n}. So σ(u′) →^{b_{h}} and σ(u′) ↛^{c} imply σ′(u′) →^{b_{h}} and

σ′(u′) ↛^{c}. It follows that σ′(u_{j}) →^{b_{h}}, and so σ′(u) →^{b_{h}}. Hence σ′(t) \underline{↔} / σ′(u). Since σ′(P) = σ(P) = true, this contradicts the fact that P ⇒ t ≈ u is sound modulo \underline{↔}.

(b) \{z_{i_{0}k} | k ∈ K_{i_{0}}\} ⊆ \{y_{k} | k ∈ K\}, for some i_{0} ∈ I′ with σ(t_{i_{0}}) \underline{↔} / 0. In this case, K is non-empty since, as previously observed, K_{i_{0}} is nonempty. By the proviso of the lemma, σ(t_{i_{0}}) \underline{↔} Φ_{n}, so (since n is larger than the size of t_{i_{0}}) there is a k_{0} ∈ K_{i_{0}} with σ(z_{i_{0}k_{0}}) \underline{↔} / 0. Furthermore, by the assumption for case 3 of the proof, σ(u_{j}) \underline{↔} / 0 and σ(u_{j}) \underline{↔} / Φ_{n}. Therefore, there is an h with 1 ≤ h ≤ n such that σ(Θ(u′)) ↛^{b_{h}}. Define the substitution σ′ as

σ′(y) = \{ \begin{matrix}a_{h}.0 & if y = z_{i_{0}k_{0}} \\ σ(y) & otherwise \end{matrix}

for process variables y, and let σ′ agree with σ on action variables. We argue that σ′(t) ↛^{a_{h}}. To this end, observe, first of all, that, since σ(Θ(u′)) ↛^{b_{h}}, we have σ(∑_{k∈K} y_{k}) ↛^{b_{h}}, and so σ(z_{i_{0}k_{0}}) ↛^{b_{h}}. We are now ready to show that no summand of σ′(t) affords an a_{h}-labelled transition. We consider three exhaustive possibilities:

i. Let i ∈ I′ with z_{i_{0}k_{0}} ∉ {z_{ik} | k ∈ K_{i}}. Then clearly σ′(t_{i}) ↛^{a_{h}}.

ii. Let i ∈ I′ with z_{i_{0}k_{0}} ∈ \{z_{ik} | k ∈ K_{i}\}. Then σ(t_{i}) \underline{↔} / 0 because σ(z_{i_{0}k_{0}}) \underline{↔} / 0, so by assumption σ(t_{i}) \underline{↔} Φ_{n}. This implies σ(t_{i}) →^{b_{h}}, so since σ(z_{i_{0}k_{0}}) ↛^{b_{h}}, it follows that σ′(t_{i}) →^{b_{h}}. Since the outermost function symbol of t_{i} is Θ, we can conclude that σ′(t_{i}) ↛^{a_{h}}.

iii. Finally, since σ(z_{i_{0}k_{0}}) \underline{↔} / 0 and σ(z_{i_{0}k_{0}}) ↛^{b_{h}}, the proviso of the lemma

yields that z_{i_{0}k_{0}} cannot be a summand of t. Since t has no other types of summands, from the three cases above we can conclude that σ′(t) ↛^{a_{h}}. On the other hand, σ′(Θ(u′)) →^{a_{h}}, be-

cause σ(Θ(u′)) ↛^{b_{h}} and z_{i_{0}k_{0}} ∈ {y_{k} | k ∈ K}. Hence σ′(u) →^{a_{h}}, and so

σ′(t) \underline{↔} / σ′(u). Since σ′(P) = σ(P) = true, this contradicts the fact that P ⇒ t ≈ u is sound modulo \underline{↔}.

In summary, the assumption that, for some j ∈ J, the term σ(u_{j}) has a summand that is bisimilar neither to Φ_{n} nor to 0, leads to a contradiction. This completes the proof. ⊓ ⊔

The following proposition states that the property of closed instantiations of sound conditional equations mentioned in the above lemma is preserved under equational derivations from a finite collection of sound equations. This is the key to the promised proof of our claim.

Proposition 1. Let E be a finite collection of conditional equations that is sound modulo \underline{↔}. Let n ≥ 2 be larger than the size of any term in the equations of E. Assume, furthermore, that

– E ⊢ p ≈ q; and

– the summands of p are all bisimilar to Φ_{n} or 0.

Then the summands of q are all bisimilar to Φ_{n} or 0.

Proof. By induction on the depth of the closed proof of the equation p ≈ q from E. We proceed by a case analysis on the last rule used in the proof of p ≈ q from E.

– E ⊢ p ≈ q because σ(t) = p and σ(u) = q for some conditional equation P ⇒ t ≈ u ∈ E and closed substitution σ with σ(P) = true. The claim follows immediately from Lemma 4.

– E ⊢ p ≈ q because p = p′ + p′′ and q = q′ + q′′ for some p′, q′, p′′, q′′ such that E ⊢ p′ ≈ q′ and E ⊢ p′′ ≈ q′′. Since the summands of p are all bisimilar to Φ_{n} or 0, the same holds for p′ and p′′. By induction, the summands of q′ and q′′ are all bisimilar to Φ_{n} or 0. The claim now follows because the summands of q are those of q′ and q′′.

– E ⊢ p ≈ q because p = a.p′ and q = a.q′ for some p′, q′ such that E ⊢ p′ ≈ q′. This case is vacuous, because n ≥ 2 and p \underline{↔} Φ_{n}.

– E ⊢ p ≈ q because p = α.p′ and q = α.q′ for some p′, q′ such that E ⊢ p′ ≈ q′. This case is vacuous, because p and q are closed.

– E ⊢ p ≈ q because p = Θ(p′) and q = Θ(q′) for some p′, q′ such that E ⊢ p′ ≈ q′. The claim is immediate, because both p and q consist of a single summand, and p \underline{↔} q by the soundness of E. ⊓ ⊔

Theorem 3. Let Act = {a_{i}, b_{i} | i ≥ 1} ∪ {c}, where a_{i} < b_{i} < c for each i ≥ 1, and these are the only inequalities. Then bisimulation equivalence has no ground-complete axiomatization over BCCSP_{Θ} consisting of a finite set of sound conditional equations.

Proof. Let E be a finite collection of conditional equations that is sound modulo \underline{↔}. Let n ≥ 2 be larger than the size of any term in the equations of E. According to Proposition 1, from E we cannot derive Θ(Φ_{n}) ≈ Φ_{n}. This equation is sound modulo \underline{↔}, and therefore E is not ground-complete. ⊓ ⊔

Remark 3. Note that Theorem 3 applies to conditional equations of the form P ⇒ t ≈ u where P is an “arbitrary” predicate—that is any subset of the collection of closed substitutions. It is therefore not limited to predicates that can be expressed in a given language.

5.2 Positive Results

In the previous section, we have offered an example of a priority structure (Act, <) with respect to which it is impossible to give a finite, ground-complete axiomatization of bisimulation equivalence over BCCSP_{Θ} in terms of conditional equations without recourse to auxiliary operators. That result, however, does not imply that auxiliary operators are always necessary to achieve a finite basis of conditional equations for bisimulation equivalence. Our aim in this section is to substantiate this claim by providing some general conditions over the priority structure (Act, <) that are sufficient to guarantee the existence of a finite, ground-complete conditional axiomatization of bisimulation equivalence over BCCSP_{Θ}.

Definition 4. An anti-chain in a poset (Act, <) is a subset of Act consisting of pairwise incomparable actions. The width of a poset (Act, <) is the least upper bound of the cardinalities of its anti-chains. A poset (Act, <) has finite width if its width is finite.

Example 1. The poset of actions we considered in Section 5.1 has uncountably many infinite, maximal anti-chains. (Each such anti-chain can, in fact, be obtained by picking exactly one of a_{i} and b_{i} for each i ≥ 1.) The width of that poset is therefore infinite.

We now offer a countably infinite, ground-complete, conditional axiomatization of bisimulation equivalence over BCCSP_{Θ}. Such an axiomatization reduces to a finite one if the poset of actions has finite width.

Theorem 4. Let (Act, <) be an infinite poset of actions. Then the following statements hold.

1. The axiom system consisting of the conditional equations (CPR2), (CPR3) and (CPR4)_{n} (n ≥ 0), together with equations (A1)–(A4) in Table 1 is ground-complete for bisimilarity over the language BCCSP_{Θ}.

2. Assume that the width of (Act, <) is k. Then the axiom system consisting of the conditional equations (CPR2), (CPR3), and (CPR4)_{k}, together with equations (A1)–(A4) and (PR1) in Table 1, is ground-complete for bisimilarity over the language BCCSP_{Θ}. Therefore bisimilarity has a finite, groundcomplete axiomatization using conditional equations if (Act, <) has finite width.

Proof. We only present a sketch of the proof for statement 2. (That for statement 1 follows similar lines.)

First of all, observe that it suffices only to show that, if the cardinality of each anti-chain in (Act, <) is at most k, the conditional equations (CPR2), (CPR3), (CPR4)_{k} and (PR1) can be used to remove all occurrences of Θ from closed terms. Indeed, if we can do so, then ground-completeness follows from the wellknown ground-completeness of (A1)–(A4) for BCCSP modulo \underline{↔} (see, e.g., [17]).

To prove that all occurrences of Θ can be removed from closed terms, assume that we have a closed term p that does not contain occurrences of Θ. We show that Θ(p) can be proven equal to a term q that does not contain occurrences of Θ by induction on the size of p. To this end, note that, modulo associativity and commutativity of +, the term p can be written ∑_{i=1}^{n} a_{i}.p_{i} for some n ≥ 0, actions a_{i} and closed terms p_{i} that do not contain occurrences of Θ.

If n = 0, then equation (PR1) yields that Θ(0) ≈ 0, and we are done. If n = 1, then the claim follows using (1) and the induction hypothesis. (Recall that, since k ≥ 1, equation (1) is derivable from (CPR4)_{k}.) Consider now the case when n ≥ 2. We proceed by examining the following three sub-cases:

– there are i, j such that 1 ≤ i < j ≤ n and a_{i} = a_{j},

– there are i, j such that 1 ≤ i, j ≤ n and a_{i} < a_{j}, and

– the collection of actions {a_{1}, …, a_{n}} is an anti-chain in the poset (Act, <).

The first two sub-cases are handled using the inductive hypothesis, and the conditional equations (CPR2) and (CPR3), respectively.

If the proviso for the third sub-case applies, then we know that n ≤ k. Using equation (A3) if n < k, we can therefore reason as follows:

Θ(∑_{i=1}^{n} a_{i}.p_{i}) ≈ Θ(∑_{i=1}^{n} a_{i}.p_{i} + \underbrace{a_{n}.p_{n} + ⋯ + a_{n}.p_{n}}_{(k − n) times})

≈ ∑_{i=1}^{n} a_{i}.Θ(p_{i}) (By (CPR4)_{k} and possibly (A3))

≈ ∑_{i=1}^{n} a_{i}.q_{i} (By the inductive hypothesis)

for some closed terms q_{1}, …, q_{n} that do not contain occurrences of Θ.

Using this result, a simple argument by structural induction over closed terms shows that each closed term in the language BCCSP_{Θ} is provably equal to one that does not contain occurrences of the Θ operator, and we are done. ⊓ ⊔

So bisimilarity affords a finite, ground-complete axiomatization that uses conditional equations if the poset (Act, <) has finite width. (Moreover, the conditional equations making up the axiom systems used in Theorem 4 only involve predicates over actions that can be expressed as conjunctions of, possibly negated, atomic formulae of the form α < β.) A natural question to ask at this point is whether this result holds for more general priority structures. We now proceed to address this question in some detail.

Let us begin by observing that there are priority structures with infinite antichains that do allow for a finite equational axiomatization of bisimilarity over the language BCCSP_{Θ}. Consider, by way of example, the flat priority structure ({⊥, a_{0}, a_{1}, …}, <), where the only ordering relations are given by ⊥ < a_{i} for each i ≥ 0. Membership of the countably infinite anti-chain {a_{0}, a_{1}, …} can be characterized syntactically by the predicate

P (α) = ∀β. ¬(α < β) .

(Alternatively, if we consider actions as constant symbols, we could write P (α) = ⊥ < α^{5}.) We can therefore write the following conditional equation that allows us to reduce the number of summands within the scope of a Θ operator:

P (α) ∧ P (β) ⇒ Θ(α.x + β.y + z) ≈ Θ(α.x + z) + Θ(β.y + z) .  (2)

It is not hard to see that the above equation is sound. (In fact, the soundness of this equation will follow from the more general result in Lemma 5.) Moreover, following the lines of the proof sketch for Theorem 4(2), one can argue that, together with (PR1), (CPR2), (CPR3) and (1), this equation can be used to remove all occurrences of Θ from closed terms. It follows that:

Proposition 2. Consider the priority poset ({⊥, a_{0}, a_{1}, …}, <), where the only ordering relations are given by ⊥ < a_{i} for each i ≥ 0. Then the axiom system consisting of the conditional equations (2), (CPR2), (CPR3) and (1), together with equations (A1)–(A4) and (PR1) in Table 1, is ground-complete for bisimilarity over the language BCCSP_{Θ}.

As another example, consider the priority structure

A = ({a_{0}, a_{1}, …} ∪ {b_{0}, b_{1}, c}, <) ,

where the relation < is the least transitive relation satisfying

b_{i} < a_{j} for all i ∈ {0, 1}, j ≥ 0 and
a_{j} < c for each j ≥ 0 .

This poset has one non-trivial maximal finite anti-chain, namely {b_{0}, b_{1}}, and one maximal countably infinite anti-chain, namely

A = {a_{0}, a_{1}, …} .

Membership of A is characterized by the predicate P_{A} defined thus:

P_{A}(α) = ∃β_{1}, β_{2}. β_{1} < α < β_{2} .

(Alternatively, using actions as constant symbols, we could write P_{A}(α) = (b_{0} < α) ∧ (α < c).) As the reader can check, the instance of the conditional equation (2) associated with this predicate is sound. (Again, the soundness of this equation will follow from the more general result in Lemma 5.) Moreover, following the lines of the proof sketch for Theorem 4(2), one can argue that, together with (PR1), (CPR2), (CPR3) and (CPR4)_{2} (to handle the finite anti-chain {b_{0}, b_{1}}), this equation can be used to remove all occurrences of Θ from closed terms. It follows that:

5 If one only considers predicates that can be written as boolean combinations of atomic formulae of the form α < β or α = β, then all predicates of the form P (α) are either tautologies or contradictions, and thus no non-trivial subsets of the set of actions can be expressed.

Proposition 3. Consider the priority poset A. Then the axiom system consisting of the conditional equation (2) for predicate P_{A}, (CPR2), (CPR3) and (CPR4)_{2}, together with equations (A1)–(A4) and (PR1) in Table 1, is groundcomplete for bisimilarity over the language BCCSP_{Θ}.

In both of the examples we have just presented, the conditional equation (2) plays a key role in that it allows us to reduce the size of terms in “head normal form” having summands of the form a.p and b.q with a, b contained in an infinite antichain within the scope of a Θ operator. The following lemma states a necessary and sufficient condition on the infinite anti-chain that guarantees that axiom (2) be sound modulo bisimilarity.

Lemma 5. Let A be an anti-chain in the poset (Act, <) whose membership is described by predicate P_{A}. Then the conditional equation (2) for predicate P_{A} is sound modulo bisimilarity iff each element of A is above the same set of actions—that is, for each a, b ∈ A and c ∈ Act, we have that c < a iff c < b.

Proof. We first prove the “if implication”. To this end, assume that a, b ∈ A and p, q, r are closed terms in the language BCCSP_{Θ}. We claim that

Θ(a.p + b.q + r) \underline{↔} Θ(a.p + r) + Θ(b.q + r) .

To see that this claim does hold, it suffices only to observe that the following statements hold for each closed term p′:

1. Θ(a.p + b.q + r) →^{a} p′ iff Θ(a.p + r) + Θ(b.q + r) →^{a} p′,

2. Θ(a.p + b.q + r) →^{b} p′ iff Θ(a.p + r) + Θ(b.q + r) →^{b} p′, and

3. Θ(a.p + b.q + r) →^{c} p′ iff Θ(a.p + r) + Θ(b.q + r) →^{c} p′, for each action c different from a, b.

We only offer a proof for the last of these statements. To this end, assume, first of all, that Θ(a.p + b.q + r) →^{c} p′ for some action c different from a, b and closed term p′. Since c is different from a, b, there is a closed term r′ such that

– p′ = Θ(r′),

– r →^{c} r′,

– r ↛^{d} for each action d such that c < d and

– neither c < a nor c < b holds.

It is now a simple matter to see that, for instance, Θ(a.p + r) →^{c} p′. This yields that Θ(a.p + r) + Θ(b.q + r) →^{c} p′, which was to be shown.

Conversely, suppose that Θ(a.p + r) + Θ(b.q + r) →^{c} p′ for some action c different from a, b and closed term p′. Without loss of generality, we may assume that this is because Θ(a.p + r) →^{c} p′. Since c is different from a, b, there is a closed term r′ such that

– p′ = Θ(r′),

– r →^{c} r′,

– r ↛^{d} for each action d such that c < d and

– c < a does not hold.

Observe now that c < b does not hold either, because a and b are above the same actions by the proviso of the lemma. It follows that Θ(a.p + b.q + r) →^{c} p′, which was to be shown.

To establish the “only if implication”, assume that A contains two distinct incomparable actions a and b that are not above the same set of actions. Suppose, without loss of generality, that c < a, but c < b does not hold, for some action c. Then

Θ(a.0 + b.0 + c.0) \underline{↔} a.0 + b.0 \underline{↔} / a.0 + b.0 + c.0 \underline{↔} Θ(a.0 + c.0) + Θ(b.0 + c.0) .

(The last equivalence holds true because b and c must be incomparable, as c < a and a and b are incomparable.) Therefore equation (2) for predicate P_{A} is not sound modulo bisimilarity. ⊓ ⊔

Remark 4. Let A, B be different, maximal anti-chains in the poset (Act, <). Assume that each element of A is above the same set of actions—that is, for each a, b ∈ A and c ∈ Act, we have that c < a iff c < b—, and so is each element of B. Then A and B are disjoint.

To see this, assume, towards a contradiction, that a ∈ A ∩ B. Since A and B are maximal anti-chains, neither one is a subset of the other. Therefore, since A ≠ B, there are actions b, c such that b ∈ A − B and c ∈ B − A. It follows that a, b, c are above the same set of actions in Act. However, b ∉ B. Therefore, since B is maximal, there must be some action d ∈ B with b < d or d < b. If b < d, we have that b < a because a, d ∈ B and each element of B is above the same actions. This contradicts the assumption that A is an anti-chain. If d < b then reasoning as above we can reach a contradiction to the assumption that B is an anti-chain. Therefore, A and B must be disjoint.

Suppose that p is a closed term in head normal form whose set of initial actions is included in an infinite anti-chain satisfying the constraint in the statement of Lemma 5. Then the sound conditional equation (2) offers a way of “simplifying” the term Θ(p). The use of this axiom is the key to the proof of the following generalization of Theorem 4(2), and of Propositions 2 and 3.

Theorem 5. Let (Act, <) be an infinite poset of actions. Assume that

1. the collection of the sizes of the finite, maximal anti-chains in (Act, <) is finite,

2. (Act, <) has finitely many infinite, maximal anti-chains, and

3. for each infinite, maximal anti-chain A in (Act, <)

(a) membership of A can be characterized by a predicate P_{A} in first-order logic and

(b) each element of A is above the same set of actions—that is, for each a, b ∈ A and c ∈ Act, we have that c < a iff c < b.

Let k be the size of the largest finite, maximal anti-chain in (Act, <), or 1 if all maximal anti-chains are infinite. Then the axiom system consisting of one instance of the conditional equation (2) for predicate P_{A} for each infinite antichain A in (Act, <), (CPR2), (CPR3) and (CPR4)_{k}, together with equations (A1)–(A4) and (PR1) in Table 1, is ground-complete for bisimilarity over the language BCCSP_{Θ}.

Proof. The soundness of the axiom system is easily established, using Lemma 5 for the instances of axiom (2). The completeness of the axiom system can be shown along the lines of the proof of Theorem 4. The key of the argument is again to prove that each term Θ(∑_{i=1}^{n} a_{i}.p_{i}), where the p_{i} do not contain occurrences of Θ, can be proven equal to a term q that does not contain occurrences of Θ by induction on the size of ∑_{i=1}^{n} a_{i}.p_{i}. This we do by considering several sub-cases depending on the number n of summands in ∑_{i=1}^{n} a_{i}.p_{i}.

If n = 0, then the claim follows using (PR1). If n = 1, then it suffices only to use (1) and the inductive hypothesis. (Recall that (1) is derivable from (CPR4)_{k}.) If n ≥ 2, then we distinguish the following sub-cases:

– there are i, j such that 1 ≤ i < j ≤ n and a_{i} = a_{j},

– there are i, j such that 1 ≤ i, j ≤ n and a_{i} < a_{j},

– the collection of actions {a_{1}, …, a_{n}} is an anti-chain in the poset (Act, <).

The first two sub-cases are handled using the inductive hypothesis, and the conditional equations (CPR2) and (CPR3), respectively.

The last sub-case is handled using (CPR4)_{k} as in the proof of Theorem 4 if {a_{1}, …, a_{n}} is included in a finite maximal anti-chain. Assume now that {a_{1}, …, a_{n}} is only included in an infinite maximal anti-chain, say A. (In fact, Remark 4 ensures that such an anti-chain A is unique.) Using the instance of the conditional equation (2) for predicate P_{A} and induction, the claim follows.

The rest of the proof follows the lines of that of Theorem 4, and is therefore omitted. ⊓ ⊔

Remark 5. The priority structure we employed in our proof of Theorem 3 satisfies neither condition 2 nor condition 3 in the proviso of the above theorem.

In light of the above result, bisimilarity has a finite, ground-complete axiomatization using conditional equations over the language BCCSP_{Θ} if the poset of actions satisfies the proviso of the above theorem.

We have not yet attempted a complete classification of the priority structures for which bisimulation equivalence affords a finite axiomatization in terms of conditional equations over the language BCCSP_{Θ}. This is most likely a hard problem which we leave for future research.

References

1. L. Aceto, W. Fokkink, A. Ingolfsdottir, and B. Luttik. CCS with Hennessy’s merge has no finite equational axiomatization. Theoretical Computer Science, 330(3):377– 405, 2005.

2. L. Aceto, W. Fokkink, A. Ingolfsdottir, and S. Nain. Bisimilarity is not finitely based over BPA with interrupt. In J. Fiadeiro, N. Harman, M. Roggenbach, and J. Rutten, eds., Proc. 1st Conference on Algebra and Coalgebra in Computer Science (CALCO’05), LNCS 3629, pp. 52–66. Springer, 2005.

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

4. J. Baeten and J. Bergstra. Mode Transfer in Process Algebra. Report CSR00–01, Eindhoven University of Technology, 2000.

5. J. Bergstra. Put and Get, Primitives for Synchronous Unreliable Message Passing. Logic Group Preprint Series 3, Utrecht University, Department of Philosophy, 1985.

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

7. B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can’t be traced. Journal of the ACM, 42(1):232–268, 1995.

8. E. Brinksma. A tutorial on LOTOS. In M. Diaz, ed., Proc. 5th IFIP Workshop on Protocol Specification, Testing and Verification (PSTV’85), pp. 171–194. North-Holland, 1985.

9. J. Camilleri and G. Winskel. CCS with priority choice. Information and Computation, 116(1):26–37, 1995.

10. R. Cleaveland and M. Hennessy. Priorities in process algebras. Information and Computation, 87(1-2):58–77, 1990.

11. R. Cleaveland, G. Lüttgen, and V. Natarajan. Priorities in process algebra. In J. Bergstra, A. Ponse, and S. Smolka, eds., Handbook of Process Algebra, pp. 711– 765. Elsevier, 2001.

12. R. Cleaveland, G. Lüttgen, V. Natarajan, and S. Sims. Priorities for modeling and verifying distributed systems. In T. Margaria and B. Steffen, eds., Proc. 2nd Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS’96), LNCS 1055, pp. 278–297. Springer, 1996.

13. A. Dsouza and B. Bloom. On the expressive power of CCS. In P.S. Thiagarajan, ed., Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’95), LNCS 1026, pp. 309–323. Springer, 1995.

14. R. van Glabbeek. The linear time-branching time spectrum. In J. Baeten and J.W. Klop, eds., Proc. 1st Conference on Concurrency Theory: Unification and Extension (CONCUR’90), LNCS 458, pp. 278–297. Springer, 1990.

15. R. van Glabbeek. The linear time-branching time spectrum I. The semantics of concrete, sequential processes. In J. Bergstra, A. Ponse and S. Smolka, eds., Handbook of Process Algebra, pp. 3–99. Elsevier, 2001.

16. J.F. Groote. A new strategy for proving ω-completeness with applications in process algebra. In J. Baeten and J.W. Klop, eds., Proc. 1st Conference on Concurrency Theory (CONCUR’90), LNCS 458, pp. 314–331. Springer, 1990.

17. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985.

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

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

20. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

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

22. F. Moller. The importance of the left merge operator in process algebras. In M. Paterson, ed., Proc. 17th Colloquium on Automata and Languages (ICALP’90), LNCS 443, pp. 752–764. Springer, 1990.

23. F. Moller. The nonexistence of finite axiomatisations for CCS congruences. In Proc. 5th Symposium on Logic in Computer Science (LICS’90), pp. 142–153. IEEE Computer Society Press, 1990.

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

Recent BRICS Report Series Publications

RS-06-1 Luca Aceto, Taolue Chen, Willem Jan Fokkink, and Anna Ingólfsdóttir. On the Axiomatizability of Priority. January 2006. 25 pp.

RS-05-38 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. December 2005. iii+39 pp. Revised version of BRICS RS-05-22.

RS-05-37 Gerth Stølting Brodal, Kanela Kaligosi, Irit Katriel, and Martin Kutz. Faster Algorithms for Computing Longest Common Increasing Subsequences. December 2005. 16 pp.

RS-05-36 Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the Static and Dynamic Extents of Delimited Continuations. December 2005. ii+33 pp. To appear in the journal Science of Computer Programming. Supersedes BRICS RS-05-13.

RS-05-35 Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. November 2005. 19 pp.

RS-05-34 Henning Korsholm Rohde. Formal Aspects of Polyvariant Specialization. November 2005. 27 pp.

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

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

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

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