NOTE! This is the text only version of the PDF version or the PS version of this paper. Since there are many formulas in this work, the HTML version is not optimal.


Conservative Extension in Structural Operational Semantics

Luca Aceto\Lambda  Wan Fokkinky Chris Verhoefz

1 Introduction Structural operational semantics (SOS) [44] provides
a framework to give an operational semantics to programming and
specification languages. In particular, because of its intuitive appeal
and flexibility, SOS has found considerable application in the study of
the semantics of concurrent processes. SOS generates a labelled transition
system, whose states are the closed terms over an algebraic signature,
and whose transitions are supplied with labels. The transitions between
states are obtained inductively from a transition system specification
(TSS), which consists of so-called transition rules of the form
premisesconclusion . A typical example of a transition rule is

x a! x0 xky a! x0ky

stipulating that if t a! t0 holds for closed terms t and t0, then so does
tku a! t0ku for each closed term u. In general, validity (or invalidity)
of the positive (or negative) premises of a transition rule, under a
certain substitution, implies validity of the conclusion of this rule
under the same substitution.

This column is an excerpt from [2], which gives an overview of recent
results in the field of SOS, with an emphasis on existing formats
for TSSs.

\Lambda BRICS (Basic Research in Computer Science), Centre of the Danish
National Research Foundation, Department of Computer Science, Aalborg
University, Fredrik Bajers Vej 7-E, DK-9220 Aalborg O/, Denmark. Email:
luca@cs.auc.dk. Partially supported by a grant from the Italian CNR,
Gruppo Nazionale per l'Informatica Matematica (GNIM).

yCWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands. Email:
wan@cwi.nl.

Partially supported by a grant from the Nuffield Foundation.

zUniversity of Amsterdam, Department of Computer Science, Programming
Research

Group, Kruislaan 403, 1098 SJ Amsterdam, The Netherlands. Email:
x@wins.uva.nl.

1

Each of these formats comes equipped with a rich body of results that
are guaranteed to hold for any process calculus whose TSS is within
that format.

Over and over again, process calculi such as CCS [40], CSP [47], and ACP
[11] have been extended with new features, and the TSSs that provide
the operational semantics for these process algebras were extended
with transition rules to describe these features; see, e.g., [10] for a
systematic approach. A question that arises naturally is whether or not
the the original and the extended TSS induce the same transitions t a! t0
for closed terms t in the original domain. Usually it is desirable that
an extension is operationally conservative, meaning that the provable
transitions for an original term are the same both in the original and
in the extended TSS.

Groote and Vaandrager [34, Thm. 7.6] proposed syntactic restrictions
on a TSS, which automatically yield that an extension of this TSS
with transition rules that contain fresh function symbols in their
sources is operationally conservative. Bol and Groote [18, 33]
supplied this conservative extension format with negative premises.
Verhoef [49] showed that, under certain conditions, a transition rule
in the extension can be allowed to have an original term as its source.
D'Argenio and Verhoef [22, 23] formulated a generalization in the context
of inequational specifications. Fokkink and Verhoef [25] relaxed the
syntactic restrictions on the original TSS, and lifted the operational
conservative extension result to higher-order languages. This column
contains an exposition on existing conservative extension formats for
SOS, and their applications with respect to term rewriting systems and
completeness of axiomatizations.

Predicates in SOS semantics can be coded as binary relations [34].
Moreover, negative premises can often be expressed positively using
predicates [9]. However, in the literature SOS definitions are often
decorated with predicates and/or negative premises. For example,
predicates are used to express matters like (un)successful termination,
convergence, divergence [3], enabledness [14], maximal delay, and side
conditions [42]. Negative premises are used to describe, e.g., deadlock
detection [38], sequencing [17], priorities [7, 21], probabilistic
behaviour [39], urgency [19], and various real [37] and discrete time [6,
35] settings. Since predicates and negative premises are so pervasive,
and often lead to cleaner semantic descriptions for many features and
constructs of interest, we deal explicitly with these notions.

The organization of this column is as follows. Sect. 2 gives an overview
of the basics of SOS. Sect. 3 presents syntactic constraints to ensure
that an extension of a TSS is operationally conservative. Sect. 4 and 5
contain applications of conservative extension in equational specification
and term rewriting. Sect. 6 finishes with some conclusions.

2

2 Structural Operational Semantics In this section we present the
basic notions from process theory that are needed in the remainder of
this column.

2.1 Labelled Transition Systems We begin by reviewing the model of
labelled transition systems [36, 44], which are used to express the
operational semantics of many process calculi.

Definition 2.1 A labelled transition system (LTS) is a quadruple

(Proc; Act; n a!j a 2 Acto; Pred); where:

ffl Proc is a set of states, ranged over by s; ffl Act is a set of
actions, ranged over by a; b; ffl a!` Proc\Theta Proc for each a 2 Act.
We use the more suggestive notation

s a! s0 in lieu of (s; s0) 2 a!, and write s a9 if s a! s0 for no
state s0;

ffl P ` Proc for every P 2 Pred. We write sP (resp. s:P ) if state s

satisfies (resp. does not satisfy) predicate P .

Relations s a! s0 and predicates sP in an LTS are called transitions.

In what follows, an LTS is often identified with its collection of
transitions. We trust that the meaning will always be clear from the
context.

LTSs describe the operational behaviour of processes in great detail.
In order to abstract away from irrelevant information on the way that
processes compute, a wealth of notions of behavioural equivalence over the
states of an LTS have been studied in the literature on process theory.
A systematic investigation of these notions is presented in [28],
where van Glabbeek presents the linear time/branching time spectrum.
This lattice contains all the known behavioural equivalences over LTSs,
ordered by inclusion.

2.2 Term Algebras We start from a countably infinite set Var of variables,
ranged over by x; y; z.

3

Definition 2.2 A signature \Sigma  is a set of function symbols, disjoint
from Var, together with an arity mapping that assigns a natural number ar
(f ) to each function symbol f . A function symbol of arity zero is called
a constant, while function symbols of arity one and two are called unary
and binary, respectively.

The arity of a function symbol represents its number of arguments.
Definition 2.3 The set (\Sigma ) of (open) terms over a signature \Sigma ,
ranged over by t; u, is the least set such that:

ffl each x 2 Var is a term; ffl f (t1; : : : ; tar(f)) is a term, if f
is a function symbol and t1; : : : ; tar(f)

are terms.

T(\Sigma ) denotes the set of closed terms over \Sigma , i.e., terms
that do not contain variables.

For a constant a, the term a() is abbreviated to a. By convention,
whenever we write a term-like phrase (e.g., f (t; u)), we intend it to
be a term (i.e., f is binary).

Definition 2.4 A substitution is a mapping oe : Var ! (\Sigma ).
A substitution is closed if it maps each variable to a closed term in
T(\Sigma ). A substitution extends to a mapping from terms to terms as
usual; the term oe(t) is obtained by replacing occurrences of variables
x in t by oe(x).

2.3 Transition System Specifications We proceed to introduce the
main objects of study in the field of SOS, viz. transition system
specifications.

Definition 2.5 Let \Sigma  be a signature, and let t and t0 range over
(\Sigma ). A transition rule ae is of the form H=ff, with H a collection
of positive premises t a! t0 and tP , and of negative premises t a9
and t:P . Moreover, the conclusion ff is of the form t a! t0 or tP .
The left-hand side of the conclusion is the source of ae. A transition
rule is closed if it does not contain variables.

A transition system specification (TSS) is a collection of transition
rules. A TSS is positive if its transition rules do not contain negative
premises.

4

For the sake of clarity, we will often display transition rules in
the form

H

ff . The first systematic study of TSSs may be found in [48], while the
firststudy of TSSs with negative premises appeared in [16].

We proceed to define when a transition is provable from a TSS.
The following notion of a proof from [31] generalizes the standard
definition (see, e.g., [34]) by allowing for the derivation of closed
transition rules. The derivation of a transition ff corresponds to the
derivation of the closed transition rule H=ff with H = ?. The case H 6=
? corresponds to the derivation of ff under the assumptions in H.

Definition 2.6 Positive literals are transitions t a! t0 and tP ,
while negative literals are expressions t a9 and t:P , where t and t0
range over the collection of closed terms. A literal is a positive or
negative literal.

Definition 2.7 Let T be a TSS. A proof of a closed transition rule
H=ff from T is a well-founded, upwardly branching tree whose nodes are
labelled by literals, where the root is labelled by ff, and if K is the
set of labels of the nodes directly above a node with label fi, then

1. either K = ? and fi 2 H, 2. or K=fi is a closed substitution instance
of a transition rule in T . If a proof of H=ff from T exists, then H=ff
is provable from T .

2.4 Three-Valued Stable Models In the presence of negative premises,
the meaning of a TSS is sometimes ambiguous. For example, one can express
that a transition holds if it does not hold. In order to associate an LTS
to each TSS, we use the notion of a (least) three-valued stable model,
introduced by Przymusinski [46] in logic programming. A three-valued
stable model partitions the collection of transitions into three disjoint
sets: the set C of transitions that are certainly true, the set U of
transitions for which it is unknown whether or not they are true, and
the set F of remaining transitions that are false.

Definition 2.8 A disjoint pair of sets of transitions hC; U i constitutes
a three-valued stable model for a TSS T if:

- a transition ff is in C iff T proves a closed transition rule N=ff where

N contains only negative literals and C [ U j= N ;

- a transition ff is in C [ U iff T proves a closed transition rule N=ff

where N contains only negative literals and C j= N .

5

Each TSS has one or more three-valued stable models. For example, the
TSS a:P

2

aP1

a:P1

aP2 has hfaP1g; ?i, hfaP2g; ?i, and h?; faP1; aP2gi as its three-valued
stable models. Each TSS T affords a unique (information-)least
three-valued stable model hC; U i, in the sense that the set U is maximal.
Przymusinski [46] showed that this least three-valued stable model
coincides with the so-called well-founded model that was introduced
by van Gelder, Ross, and Schlipf [27] in logic programming. It is
advocated in, e.g., [18, 32] that a TSS is meaningful if and only if its
least three-valued stable model does not contain unknown transitions.
In particular, each TSS that does not contain negative premises in its
transition rules satisfies this requirement. The reader is referred to
[31, 32] for more information on three-valued stable models and related
notions.

3 Operational Conservative Extension Often one wants to add new operators
and rules to a given TSS. Therefore, a natural operation on TSSs is to
take their componentwise union. The following definition stems from [34].

Definition 3.1 Let T0 and T1 be TSSs whose signatures \Sigma 0 and \Sigma
1 agree on the arity of the function symbols in their intersection.
We write \Sigma 0 \Phi  \Sigma 1 for the union of \Sigma 0 and \Sigma 1.
The sum of T0 and T1, notation T0 \Phi  T1, is the TSS over signature
\Sigma 0 \Phi  \Sigma 1 containing the rules in T0 and T1.

An operational conservative extension requires that an original TSS and
its extension prove exactly the same closed transition rules that have
only negative premises and an original closed term as their source.
(This notion of an operational conservative extension is related to
an equivalence notion for TSSs in [24, 32]: two TSSs are equivalent
if they prove exactly the same closed transition rules that have only
negative premises.)

Definition 3.2 A TSS T0 \Phi  T1 is an operational conservative extension
of TSS T0 if for each closed transition rule N=ff such that:

- N contains only negative literals;

- the left-hand side of ff is in T(\Sigma 0); - N=ff is provable from
T0 \Phi  T1; we have that N=ff is provable from T0.

6

3.1 Guaranteeing Operational Conservative Extension We start by defining
the notion of a source-dependent variable [25, 30], which will be an
important ingredient of a rule format to ensure that an extension of a
TSS is operationally conservative. In order to conclude that an extended
TSS is operationally conservative over the original TSS, we need to know
that the variables in the original transition rules are source-dependent.
In the literature this criterion is sometimes neglected. For example, in
[43] an extended TSS is considered in which each transition rule in the
extension contains a fresh operator in its source, and from this fact
alone it is concluded that the extension is operationally conservative.
In general, however, this characteristic is not sufficient, as is shown
in the next example.

Example: Let a and b be constants. Consider the TSS over signaturef

ag that consists of the transition rule xP=aP . Extend this TSS with
the TSS over signature fbg that consists of the transition rule ?=bP ,
which contains the fresh constant b in its source. The transition aP
can be proved in the extended TSS, but not in the original one, so this
extension is not operationally conservative. \Lambda

Definition 3.3 The source-dependent variables in a transition rule ae
are defined inductively as follows:

- all variables in the source of ae are source-dependent; - if t a!
t0 is a premise of ae and all variables in t are source-dependent,

then all variables in t0 are source-dependent.

A transition rule is source-dependent if all its variables are.

Note that the transition rule xP=aP from the example above is not
sourcedependent, because its variable x is not.

Thm. 3.4 below, which stems from [25], formulates sufficient criteria for
a TSS T0 \Phi  T1 to be an operational conservative extension of TSS T0.
We say that a term in (\Sigma 0 \Phi  \Sigma 1) is fresh if it contains a
function symbol from \Sigma 1n\Sigma 0. Similarly, an action or predicate
symbol in T1 is fresh if it does not occur in T0.

Theorem 3.4 Let T0 and T1 be TSSs over signatures \Sigma 0 and \Sigma 1,
respectively. Under the following conditions, T0 \Phi T1 is an operational
conservative extension of T0.

1. Each ae 2 T0 is source-dependent.

7

2. For each ae 2 T1,

ffl either the source of ae is fresh,ffl

or ae has a premise of the form t a! t0 or tP , where:

- t 2 (\Sigma 0); - all variables in t occur in the source of ae; - t0,
a, or P is fresh.

3.2 Applications to TSSs We apply Thm. 3.4 to some TSSs from the
literature.

Basic Process Algebra with Empty Process The signature of basic process
algebra with empty process [50], denoted by BPAffl(Act), consists of
the following operators:

- a set Act of constants, representing indivisible behaviour; - a
constant ffl, called empty process, representing successful termination;
- a binary operator +, called alternative composition, where a term

t1 + t2 represents the process that executes either t1 or t2;

- a binary operator \Delta , called sequential composition, where a term
t1 \Delta  t2

represents the process that executes first t1 and then t2.

So the BNF grammar [5] for BPAffl(Act) is (with a 2 Act):

t ::= a j ffl j t1 + t2 j t1 \Delta  t2 : The intuition for the operators
in BPAffl(Act) is formalized by the transition rules in Table 1 from [11],
which constitute the TSS for BPAffl(Act). This TSS defines transitions t
a! t0 to express that term t can evolve into term t0 by the execution of
action a 2 Act, and transitions tp to express that term t can terminate
successfully. The variables x, x0, y, and y0 in the transition rules
range over the collection of closed terms, while the a ranges over Act.

The transition rules for BPAffl(Act) are source-dependent. For example,
consider the third transition rule for sequential composition in Table 1:

x a! x0 x \Delta  y a! x0 \Delta  y

8

a a! ffl fflp xp x + yp

x a! x0 x + y a! x0

yp x + yp

y a! y0 x + y a! y0

xp yp

x \Delta  yp

xp y a! y0

x \Delta  y a! y0

x a! x0 x \Delta  y a! x0 \Delta  y

Table 1: Transition Rules for BPAffl(Act). The variables x and y are
source-dependent, because they occur in the source. Moreover, since x is
source-dependent, the premise x a! x0 ensures that x0 is source-dependent.
Since the three variables x, x0, and y in this transition rule are
source-dependent, the transition rule is source-dependent.

Extending the Set of Actions Suppose that Act is extended to a set Actext
. The TSS for BPAffl(Actext ) is the TSS for BPAffl(Act) in Table 1, with
the proviso that a ranges over Actext . We make the following observations
concerning the extra transition rules in the TSS for BPAffl(Actext ):

ffl the source of the transition rule a a! ffl for a 2 Actext nAct
contains the

fresh constant a;

ffl each transition rule concerning an a-transition of an alternative or

sequential composition with a 2 Actext nAct, such as

x a! x0 x + y a! x0

contains a premise with the fresh relation symbol a! and with as lefthand
side a variable from the source.

So, since the transition rules for BPAffl(Act) are source-dependent,
it can be concluded from Thm. 3.4 that BPAffl(Actext ) is an operational
conservative extension of BPAffl(Act).

9

Priorities The language BPAffl`(Act) is obtained by adding the priority
operator ` from [7] to BPAffl(Act). This function symbol assumes a
partial order ! on Act. Intuitively, the process `(t) is obtained by
eliminating all

transitions s a! s0 from the process t for which there is a transition
s b! s00 with a ! b. For example, if a ! b then `(a + b) can execute the
action b but not the action a. The TSS for BPAffl`(Act) consists of the
transition rules in Tables 1 and 2, where the transition rules in the
latter table capture the operational semantics of the priority operator.
This TSS has a unique least three-valued stable model, which does not
contain unknown transitions. (This follows from the fact that the TSS
is stratifiable [33, 45].)

xp `(x)p

x a! x0 x b9 for a ! b

`(x) a! `(x0)

Table 2: Transition Rules for the Priority Operator. The two transition
rules for the priority operator in Table 2 contain the fresh function
symbol ` in their sources. So, since the transition rules for BPAffl(Act)
are source-dependent, Thm. 3.4 implies that BPAffl`(Act) is an operational
conservative extension of BPAffl(Act).

3.3 Implications for Three-Valued Stable Models In [25] it was noted
that the operational conservative extension notion as formulated in Def.
3.2 implies a conservativity property for three-valued stable models.
If an extended TSS is operationally conservative over the original TSS,
in the sense of Def. 3.2, and if a three-valued stable model of the
extended TSS is restricted to those transitions that have an original
term as left-hand side, then the result is a three-valued stable model
of the original TSS.

Proposition 3.5 Let T0 \Phi  T1 be an operational conservative extension
of T0. If hC; U i is a three-valued stable model of T0 \Phi  T1, then

C0

\Delta = fff 2 C j the left-hand side of ff is in T(\Sigma 0)g

U 0

\Delta = fff 2 U j the left-hand side of ff is in T(\Sigma 0)g

is a three-valued stable model of T0.

10

The converse of Prop. 3.5 also holds, in the following sense. If an
extended TSS is operationally conservative over the original TSS, then
each threevalued stable model of the original TSS can be obtained by
restricting some three-valued stable model of the extended TSS to those
transitions that have an original term as left-hand side.

Proposition 3.6 Let T0\Phi T1 be an operational conservative extension
of T0. If hC; U i is a three-valued stable model of T0, then there exists
a three-valued stable model hC0; U 0i of T0 \Phi  T1 such that

C

\Delta = fff 2 C0 j the left-hand side of ff is in T(\Sigma 0)g

U

\Delta = fff 2 U 0 j the left-hand side of ff is in T(\Sigma 0)g :

Corollary 3.7 Let T0 \Phi  T1 be an operational conservative extension of
T0. If hC; U i is the least three-valued stable model of T0 \Phi  T1, then

C0

\Delta = fff 2 C j the left-hand side of ff is in T(\Sigma 0)g

U 0

\Delta = fff 2 U j the left-hand side of ff is in T(\Sigma 0)g

is the least three-valued stable model of T0.

4 Applications to Axiomatizations This section discusses how operational
conservative extension can be used to derive that an extension of
an axiomatization is so-called axiomatically conservative, or that an
axiomatization is complete or !-complete with respect to some behavioural
equivalence.

4.1 Axiomatic Conservative Extension Definition 4.1 A (conditional)
axiomatization over a signature \Sigma  consists of a set of (conditional)
equations, called axioms, of the form t0 = u0 ( t1 = u1; : : : ; tn =
un with ti; ui 2 (\Sigma ) for i = 0; : : : ; n.

An axiomatization gives rise to a binary equality relation = on (\Sigma
) thus:

ffl if t0 = u0 ( t1 = u1; : : : ; tn = un is an axiom, and oe a
substitution

such that oe(ti) = oe(ui) for i = 1; : : : ; n, then oe(t0) = oe(u0);

ffl the relation = is closed under reflexivity, symmetry, and
transitivity;

11

ffl if f is a function symbol and u = u0, then

f (t1; : : : ; ti\Gamma 1; u; ti+1; : : : ; tar(f)) = f (t1; : : : ;
ti\Gamma 1; u0; ti+1; : : : ; tar(f)):

Definition 4.2 Assume an axiomatization E, together with an equivalence
relation , on T(\Sigma ).

1. E is sound modulo , iff t = u implies t , u for all t; u 2 T(\Sigma
). 2. E is complete modulo , iff t , u implies t = u for all t; u 2
T(\Sigma ).

Note that the above definitions of soundness and completeness, albeit
standard in the literature on process algebras, are weaker than the
classic ones in logic and universal algebra, where they are required to
apply to arbitrary open expressions.

Definition 4.3 Let E0 and E1 be axiomatizations over signatures \Sigma 0
and \Sigma 0\Phi \Sigma 1, respectively. The axiomatization E0[E1 is an
axiomatic conservative extension of E0 if every equality t = u with t; u 2
T(\Sigma 0) that can be derived from E0 [ E1 can also be derived from E0.

The next theorem from [49] can be used to derive that an extension of
an axiomatization is axiomatically conservative.

Theorem 4.4 Let , be an equivalence relation on T(\Sigma 0 \Phi  \Sigma
1). Assume axiomatizations E0 and E1 over \Sigma 0 and \Sigma 0 \Phi
\Sigma 1, respectively, such that:

1. E0 [ E1 is sound over T(\Sigma 0 \Phi  \Sigma 1) modulo ,; 2.
E0 is complete over T(\Sigma 0) modulo ,. Then E0 [ E1 is an axiomatic
conservative extension of E0.

The idea behind Thm. 4.4 is as follows. Suppose that t = u can be derived
from E0 [ E1 for t; u 2 T(\Sigma 0). Soundness of E0 [ E1 (requirement 1)
yields t , u. Hence, completeness of E0 (requirement 2) yields that t =
u can be derived from E0.

Thm. 4.4 is particularly helpful in the case of an operational
conservative extension of a TSS. Assume TSSs T0 and T1 over signatures
\Sigma 0 and \Sigma 0 \Phi  \Sigma 1, respectively, where T0 \Phi  T1
is an operational conservative extension of T0. Moreover, let , be an
equivalence relation on states in LTSs. Since the states in the LTSs
associated with T0 and T0 \Phi  T1 are closed terms, the equivalence
relation , carries over to T(\Sigma 0) and T(\Sigma 0 \Phi  \Sigma 1),
respectively.

12

Owing to operational conservativity, the equivalence relation , on
T(\Sigma 0) as induced by T0 agrees with this equivalence relation on
T(\Sigma 0) as induced by T0 \Phi  T1. Applications of Thm. 4.4 in process
algebra, in the presence of an operational conservative extension of a
TSS, are abundant in the literature; we give a typical example.

Example: Using Thm. 3.4 it is not hard to see that the process algebra
ACP` [7] is an operational conservative extension of ACP. Baeten,
Bergstra, and Klop introduced in op. cit. an axiomatization E0 that is
complete over ACP modulo bisimulation equivalence, and an axiomatization
E0 [ E1 that is sound over ACP` modulo bisimulation equivalence. Hence,
Thm. 4.4 says that E0 [E1 is an axiomatic conservative extension of E0.
(In [7], fifteen pages were needed to prove this fact for the more general
case of open terms, by means of a term rewriting analysis.) \Lambda

4.2 Completeness of Axiomatizations The next theorem from [49] can be
used to derive that an axiomatization is complete.

Theorem 4.5 Let , be an equivalence relation on T(\Sigma 0 \Phi  \Sigma
1). Assume axiomatizations E0 and E1 over \Sigma 0 and \Sigma 0 \Phi
\Sigma 1, respectively, such that:

1. E0 [ E1 is sound over T(\Sigma 0 \Phi  \Sigma 1) modulo ,; 2. E0 is
complete over T(\Sigma 0) modulo ,; 3. for each t 2 T(\Sigma 0 \Phi
\Sigma 1) there is a t0 2 T(\Sigma 0) such that t = t0 can be

derived from E0 [ E1.

Then E0 [ E1 is complete over T(\Sigma 0 \Phi  \Sigma 1) modulo ,.

The idea behind Thm. 4.5 is as follows. Let t; u 2 T(\Sigma 0 \Phi
\Sigma 1) with t , u. There exist terms t0; u0 2 T(\Sigma 0) such that
E0 [ E1 proves t = t0 and u = u0 (requirement 3). Soundness of E0 [
E1 (requirement 1) yields t , t0 and u , u0, which together with t ,
u implies t0 , u0. Finally, owing to completeness of E0 over T(\Sigma 0)
(requirement 2), we may derive t0 = u0, and thus t = t0 = u0 = u.

Thm. 4.5 is particularly helpful in the case of an operational
conservative extension of a TSS. Assume TSSs T0 and T1 over signatures
\Sigma 0 and \Sigma 0 \Phi  \Sigma 1, respectively, where T0 \Phi  T1
is an operational conservative extension of T0. Moreover, let , be an
equivalence relation on states in LTSs. Since the

13

states in the LTSs associated with T0 and T0 \Phi  T1 are closed terms,
the equivalence relation , carries over to T(\Sigma 0) and T(\Sigma
0 \Phi  \Sigma 1), respectively. Owing to operational conservativity,
the equivalence relation , on T(\Sigma 0) as induced by T0 agrees with
this equivalence relation on T(\Sigma 0) as induced by T0 \Phi  T1.
Applications of Thm. 4.5 in process algebra, in the presence of an
operational conservative extension of a TSS, are abundant in the
literature; we give a typical example.

Example: Using Thm. 3.4 it is not hard to see that the process algebra ACP
[12] is an operational conservative extension of BPAffi. Bergstra and
Klop presented in op. cit. an axiomatization E0 that is complete over
BPAffi modulo bisimulation equivalence, and an axiomatization E0 [
E1 that is sound over ACP modulo bisimulation equivalence, and that
satisfies requirement 3 above. Hence, Thm. 4.5 says that E0 [ E1 is
complete over ACP modulo bisimulation equivalence. \Lambda

For the precise proofs of Thm. 4.4 and Thm. 4.5, and for more detailed
information such as generalizations of these results to axiomatizations
based on inequalities, the reader is referred to [22, 23, 49].

4.3 !-Completeness of Axiomatizations Definition 4.6 An axiomatization E
over a signature \Sigma  is !-complete if an equation t = u with t; u 2
(\Sigma ) can be derived from E whenever oe(t) = oe(u) can be derived
from E for all closed substitutions oe.

Milner [41] introduced a technique to derive !-completeness of an
axiomatization using SOS. The idea is to give a semantics to open (as
opposed to closed) terms; in particular, variables need to be incorporated
in the transition rules. See, e.g., [1, 29] for further applications of
this technique in the realm of process algebra.

The next theorem can be used to derive that an axiomatization is !-
complete.

Theorem 4.7 Let , be an equivalence relation on (\Sigma ). Suppose that
for all t; u 2 (\Sigma ), t , u whenever oe(t) , oe(u) for all closed
substitutions oe. IfE

is an axiomatization over \Sigma  such that

1. E is sound over T(\Sigma ) modulo ,, and 2. E is complete over
(\Sigma ) modulo ,, then E is !-complete.

14

The idea behind Thm. 4.7 is as follows. Let t; u 2 (\Sigma ) and suppose
that oe(t) = oe(u) can be derived from E for all closed substitutions oe.
Soundness of E over T(\Sigma ) modulo , (requirement 1) yields oe(t) ,
oe(u) for all closed substitutions oe, so t , u. Then completeness of E
over (\Sigma ) modulo , (requirement 2) yields that t = u can be derived
from E.

Assume a TSS T0 over a signature \Sigma , and let T0 be extended
with a TSS T1 that provides semantics to variables; thus, T0 \Phi  T1
gives semantics to open terms in (\Sigma ). Suppose that T0 \Phi  T1
is an operational conservative extension of T0. Moreover, let , be
an equivalence relation on states in LTSs. Since the states in the
LTSs associated with T0 and T0 \Phi  T1 are closed and open terms,
respectively, the equivalence relation , carries over to T(\Sigma 0) and
(\Sigma 0). Owing to operational conservativity, the equivalence relation
, on T(\Sigma 0) as induced by T0 agrees with this equivalence relation
on T(\Sigma 0) as induced by T0 \Phi  T1. Applications of Thm. 4.7 in
process algebra are abundant in the literature; we give a typical example.

Example: Extend the TSS for BPAffl(Act) in Table 1 by letting the symbol
a range not only over Act, but also over Var. In a sense this means that
variables are considered to be constants. This extension is operationally
conservative, which follows from Thm. 3.4 by the following facts:ffl

the transition rules for BPAffl(Act) are source-dependent;

ffl the sources of transition rules z z! ffl for variables z are fresh;
ffl each transition rule for alternative or sequential composition with
ztransitions, such as

x z! x0

x + y z! x0 contains a premise with the fresh relation symbol z! and as
left-hand side a variable from the source.

Furthermore, the following properties can be derived for the
axiomatizationE

of BPAffl(Act) in [50]:

1. E is sound over BPAffl(Act) modulo bisimulation equivalence;

2. open terms t and u in BPAffl(Act) are bisimilar whenever oe(t)
and oe(u)

are bisimilar for all closed substitutions oe;

3. E is complete over the open terms in BPAffl(Act) modulo bisimulation.
So Thm. 4.7 implies that E is !-complete over BPAffl(Act) modulo
bisimulation equivalence. \Lambda

15

5 Applications to Rewriting This section discusses how operational
conservative extension can be used to derive that an extension of a
conditional term rewriting system is so-called rewrite conservative,
or that a conditional term rewriting system is ground confluent.

5.1 Rewrite Conservative Extension Definition 5.1 Assume a signature
\Sigma . A conditional term rewriting system (CTRS) [4, 13] over \Sigma
consists of a collection of rewrite rules

t0 ! u0 ( t1 !\Lambda  u1; : : : ; tn !\Lambda  un with ti; ui 2 (\Sigma )
for i = 0; : : : ; n. Intuitively, a rewrite rule is a directed axiom that
can only be applied from left to right. A CTRS induces a binary rewrite
relation !\Lambda  on terms, similar to the way that an axiomatization
induces an equality relation on terms (the only difference is that the
rewrite relation is not closed under symmetry), thus:

ffl if t0 ! u0 ( t1 !\Lambda  u1; : : : ; tn !\Lambda  un is a rewrite
rule, and oe a

substitution such that oe(ti) !\Lambda  oe(ui) for i = 1; : : : ; n,
then oe(t0) !\Lambda  oe(u0);

ffl the relation !\Lambda  is closed under reflexivity and transitivity;
ffl if f is a function symbol and u !\Lambda  u0, then

f (t1; : : : ; ti\Gamma 1; u; ti+1; : : : ; tar(f)) !\Lambda  f (t1; :
: : ; ti\Gamma 1; u0; ti+1; : : : ; tar(f)):

The definition of sum of TSSs (cf. Def. 3.1) applies equally well
to CTRSs. Definition 5.2 Let R0 and R1 be CTRSs over signatures \Sigma
0 and \Sigma 0 \Phi  \Sigma 1, respectively. R0 \Phi  R1 is a rewrite
conservative extension of R0 if every rewrite relation t !\Lambda  u
with t 2 T(\Sigma 0) that can be derived from R0 \Phi  R1 can also be
derived from R0.

The conservative extension theorem for TSSs, Thm. 3.4, applies to CTRSs
just as well; see [26] for more details. Note that the definition of
sourcedependent variables in transition rules, Def. 3.3, also applies
to rewrite rules (where, in a rewrite rule t0 ! u0 ( t1 !\Lambda  u1;
: : : ; tn !\Lambda  un, the expression t0 ! u0 is the conclusion and
the ti !\Lambda  ui for i = 1; : : : ; n are the premises).

16

Theorem 5.3 Let R0 and R1 be CTRSs over signatures \Sigma 0 and \Sigma
0 \Phi \Sigma 1, respectively. Under the following conditions, R0 \Phi
R1 is a rewrite conservative extension of R0.

1. Each ae 2 R0 is source-dependent. 2. For each ae 2 T1,

ffl either the source of ae is fresh,ffl

or ae has a premise of the form t ! t0 where:

- t 2 (\Sigma 0); - all variables in t occur in the source of ae; -
t0 is fresh.

5.2 Ground Confluence of CTRSs Definition 5.4 A CTRS is ground confluent
if for all t; t0; t1 2 T(\Sigma ) with t !\Lambda  t0 and t !\Lambda
t1 there is a u 2 T(\Sigma ) with t0 !\Lambda  u and t1 !\Lambda  u.

Ground confluence is an important property, for instance, to prove that an
axiomatization is complete modulo some behavioural equivalence relation.

The next theorem from [49] can be used to derive that a CTRS is ground
confluent. We say that a CTRS R is sound modulo an equivalence relation,

on T(\Sigma ) if t !\Lambda  u implies t , u for all t; u 2 T(\Sigma ).

Theorem 5.5 Let , be an equivalence relation on T(\Sigma 0 \Phi  \Sigma
1). Assume CTRSs R0 and R1 over \Sigma 0 and \Sigma 0 \Phi  \Sigma 1,
respectively, such that:

1. R0 \Phi  R1 is sound over T(\Sigma 0 \Phi  \Sigma 1) modulo ,; 2.
if t; t0 2 T(\Sigma 0) with t , t0, then there is a u 2 T(\Sigma 0)
such that t !\Lambda  u

and t0 !\Lambda  u can be derived from R0;

3. for each t 2 T(\Sigma 0 \Phi  \Sigma 1) there is a t0 2 T(\Sigma 0)
such that t !\Lambda  t0 can be

derived from R0 \Phi  R1.

Then R0 \Phi  R1 is ground confluent over T(\Sigma 0 \Phi  \Sigma 1).

The idea behind Thm. 5.5 is as follows. Let t 2 T(\Sigma 0 \Phi \Sigma
1) such that t !\Lambda  t0 and t !\Lambda  t1 can be derived from R0
\Phi  R1. There exist t00; t01 2 T(\Sigma 0) such that t0 !\Lambda  t00
and t1 !\Lambda  t01 can be derived from R0 \Phi  R1 (requirement 3).
Soundness of R0 \Phi  R1 (requirement 1) yields t , t0 , t00 and t ,
t1 , t01,

17

so t00 , t01. Then there exists a u 2 T(\Sigma 0) such that t00 !\Lambda
u and t01 !\Lambda  u (requirement 2). Hence, t0 !\Lambda  u and t1
!\Lambda  u.

Thm. 5.5 is particularly helpful in the case of an operational
conservative extension of a TSS. Assume TSSs T0 and T1 over signatures
\Sigma 0 and \Sigma 0 \Phi  \Sigma 1, respectively, where T0 \Phi  T1
is an operational conservative extension of T0. Moreover, let , be an
equivalence relation on states in LTSs. Since the states in the LTSs
associated with T0 and T0 \Phi  T1 are closed terms, the equivalence
relation , carries over to T(\Sigma 0) and T(\Sigma 0 \Phi  \Sigma
1), respectively. Owing to operational conservativity, the equivalence
relation , on T(\Sigma 0) as induced by T0 agrees with this equivalence
relation on T(\Sigma 0) as induced by T0 \Phi  T1. Applications of Thm.
5.5, in the presence of an operational conservative extension of a TSS,
are abundant in the literature; we give a typical example.

Example: Using Thm. 3.4 it is not hard to see that the process algebra
ACP [12] is an operational conservative extension of BPAffi. Bergstra
and Klop presented in op. cit. an (unconditional) CTRS R0\Phi R1 for
the process algebra ACP, which reduces each closed term in ACP to a
closed term in BPAffi. Moreover, R0 \Phi  R1 is sound over ACP modulo
bisimulation equivalence, and it is easily shown that R0 can reduce
bisimilar closed terms in BPAffi to the same closed term in BPAffi.
Hence, Thm. 4.4 says that R0 \Phi  R1 is ground confluent. (In [12, p.
122], an analysis of about 400 cases was needed to prove this fact for
the more general case of open terms.) \Lambda

6 Conclusion Operational conservativity of an extension of a TSS can in
general be concluded in a straightforward fashion from the syntactic form
of the transition rules. Operational conservative extension seems such
a natural notion that in the literature this property is often a hidden
assumption: its formulation and proof are omitted without justification.
For example, this happens in the design of process algebras, and in
applications of the strategy to prove !-completeness mentioned in Sect.
4.3.

Paying attention to operational conservative extension not only leads to
more accurate contemplations on concurrency theory, but is also beneficial
in other respects. Namely, operational conservative extension can be
applied to derive useful results in the realm of equational reasoning,
which are much harder to obtain using more classical term rewriting
approaches or customized techniques.

18

References

[1] L. Aceto, W. Fokkink, R. van Glabbeek, and

A. Ing'olfsd'ottir, Axiomatizing prefix iteration with silent steps,
Information and Computation, 127 (1996), pp. 26-40.

[2] L. Aceto, W. Fokkink, and C. Verhoef, Structural operational

semantics, in Handbook of Process Algebra, J. Bergstra, A. Ponse, and S.
Smolka, eds., Elsevier, 1999. To appear.

[3] L. Aceto and M. Hennessy, Termination, deadlock and divergence,

J. Assoc. Comput. Mach., 39 (1992), pp. 147-187.

[4] F. Baader and T. Nipkow, Term Rewriting and All That, Cambridge
University Press, 1998.

[5] J. Backus, The syntax and semantics of the proposed international
algebraic language of the Zurich ACM-GAMM conference, in Proceedings ICIP,
Unesco, 1960, pp. 125-131.

[6] J. Baeten and J. Bergstra, Discrete time process algebra, in
Cleaveland [20], pp. 401-420.

[7] J. Baeten, J. Bergstra, and J. W. Klop, Syntax and defining

equations for an interrupt mechanism in process algebra, Fundamenta
Informaticae, IX (1986), pp. 127-168.

[8] J. Baeten and J. W. Klop, eds., Proceedings 1st Conference on

Concurrency Theory, Amsterdam, The Netherlands, vol. 458 of Lecture
Notes in Computer Science, Springer-Verlag, 1990.

[9] J. Baeten and C. Verhoef, A congruence theorem for structured

operational semantics with predicates, in Best [15], pp. 477-492.

[10] , Concrete process algebra, in Handbook of Logic in Computer
Science, S. Abramsky, D. Gabbay, and T. Maibaum, eds., vol. IV, Oxford
University Press, 1995, pp. 149-268.

[11] J. Baeten and P. Weijland, Process Algebra, Cambridge Tracts in

Theoretical Computer Science 18, Cambridge University Press, 1990.

[12] J. Bergstra and J. W. Klop, Process algebra for synchronous
communication, Information and Control, 60 (1984), pp. 109-137.

19

[13] , Conditional rewrite rules: Confluence and termination, J. Comput.
System Sci., 32 (1986), pp. 323-362.

[14] J. Bergstra, A. Ponse, and J. van Wamel, Process algebra with

backtracking, in Proceedings REX School/Symposium on A Decade of
Concurrency: Reflections and Perspectives, Noordwijkerhout, The
Netherlands, J. de Bakker, W. d. Roever, and G. Rozenberg, eds., vol.
803 of Lecture Notes in Computer Science, Springer-Verlag, 1994, pp.
46-91.

[15] E. Best, ed., Proceedings 4th Conference on Concurrency Theory,

Hildesheim, Germany, vol. 715 of Lecture Notes in Computer Science,
Springer-Verlag, 1993.

[16] B. Bloom, S. Istrail, and A. Meyer, Bisimulation can't be traced:

preliminary report, in Conference Record 15th ACM Symposium on Principles
of Programming Languages, San Diego, California, 1988, pp. 229-239.
Preliminary version of [17].

[17] , Bisimulation can't be traced, J. Assoc. Comput. Mach., 42 (1995),

pp. 232-268.

[18] R. Bol and J. F. Groote, The meaning of negative premises in

transition system specifications, J. Assoc. Comput. Mach., 43 (1996), pp.
863-914.

[19] T. Bolognesi and F. Lucidi, Timed process algebras with urgent

interactions and a unique powerful binary operator, in Proceedings
REX Workshop on Real-Time: Theory in Practice, Mook, The Netherlands,
June 1991, J. de Bakker, C. Huizing, W. d. Roever, and G. Rozenberg,
eds., vol. 600 of Lecture Notes in Computer Science, Springer-Verlag,
1992, pp. 124-148.

[20] R. Cleaveland, ed., Proceedings 3rd Conference on Concurrency
Theory, Stony Brook, NY, vol. 630 of Lecture Notes in Computer Science,
Springer-Verlag, 1992.

[21] R. Cleaveland and M. Hennessy, Priorities in process algebras,

Information and Computation, 87 (1990), pp. 58-77.

[22] P. D'Argenio, A general conservative extension theorem in process

algebras with inequalities, in Proceedings 2nd Workshop on the Algebra
of Communicating Processes, Eindhoven, The Netherlands, A. Ponse,

20

C. Verhoef, and B. van Vlijmen, eds., Report CS-95-14, Eindhoven
University of Technology, 1995, pp. 67-79.

[23] P. D'Argenio and C. Verhoef, A general conservative extension

theorem in process algebras with inequalities, Theoretical Comput. Sci.,
177 (1997), pp. 351-380.

[24] W. Fokkink and R. van Glabbeek, Ntyft/ntyxt rules reduce to ntree

rules, Information and Computation, 126 (1996), pp. 1-10.

[25] W. Fokkink and C. Verhoef, A conservative look at operational

semantics with variable binding, Information and Computation, 146
(1998), pp. 24-54.

[26] , Conservative extension in positive/negative conditional term

rewriting with applications to software renovation factories,
in Proceedings 2nd Conference on Fundamental Approaches to Software
Engineering, Amsterdam, The Netherlands, J.-P. Finance, ed., vol. 1577 of
Lecture Notes in Computer Science, Springer-Verlag, 1999, pp. 98-113.

[27] A. van Gelder, K. Ross, and J. Schlipf, The well-founded semantics
for general logic programs, J. Assoc. Comput. Mach., 38 (1991), pp.
620-650.

[28] R. van Glabbeek, The linear time - branching time spectrum, in

Baeten and Klop [8], pp. 278-297.

[29] , A complete axiomatization for branching bisimulation congruence of
finite-state behaviours, in Proceedings 18th Symposium on Mathematical
Foundations of Computer Science 1993, Gdansk, Poland, A. Borzyszkowski
and S. Sokolowski, eds., vol. 711 of Lecture Notes in Computer Science,
Springer-Verlag, 1993, pp. 473-484.

[30] , Full abstraction in structural operational semantics (extended
abstract), in Proceedings 3rd Conference on Algebraic Methodology and
Software Technology, Enschede, The Netherlands, M. Nivat, C. Rattray, T.
Rus, and G. Scollo, eds., Workshops in Computing, Springer-Verlag,
1993, pp. 77-84.

[31] , The meaning of negative premises in transition system
specifications II, in Automata, Languages and Programming,
23rd Colloquium, F. Meyer auf der Heide and B. Monien, eds., vol.
1099 of Lecture Notes in Computer Science, Paderborn, Germany, 1996,
SpringerVerlag, pp. 502-513.

21

[32] , The meaning of negative premises in transition system
specifications II, Report STAN-CS-TN-95-16, Department of Computer
Science, Stanford University, 1996.

[33] J. F. Groote, Transition system specifications with negative
premises,

Theoretical Comput. Sci., 118 (1993), pp. 263-299.

[34] J. F. Groote and F. Vaandrager, Structured operational semantics

and bisimulation as a congruence, Information and Computation, 100
(1992), pp. 202-260.

[35] M. Hennessy and T. Regan, A process algebra for timed systems,

Information and Computation, 117 (1995), pp. 221-239.

[36] R. Keller, Formal verification of parallel programs, Comm. ACM, 19

(1976), pp. 371-384.

[37] S. Klusener, Completeness in real time process algebra, in
Proceedings 2nd Conference on Concurrency Theory, Amsterdam, The
Netherlands, J. Baeten and J. F. Groote, eds., vol. 527 of Lecture Notes
in Computer Science, Springer-Verlag, 1991, pp. 376-392.

[38] K. G. Larsen, Modal specifications, Tech. Rep. R 89-09, Institute for

Electronic Systems, University of Aalborg, 1989.

[39] K. G. Larsen and A. Skou, Compositional verification of probabilistic
processes, in Cleaveland [20], pp. 456-471.

[40] R. Milner, Communication and Concurrency, Prentice-Hall
International, Englewood Cliffs, 1989.

[41] , A complete axiomatisation for observational congruence of
finitestate behaviors, Information and Computation, 81 (1989), pp.
227-247.

[42] F. Moller and C. Tofts, A temporal calculus of communicating

systems, in Baeten and Klop [8], pp. 401-415.

[43] X. Nicollin and J. Sifakis, The algebra of timed processes, ATP:

theory and application, Information and Computation, 114 (1994), pp.
131-178.

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

22

[45] T. Przymusinski, On the declarative semantics of deductive databases

and logic programs, in Foundations of Deductive Databases and Logic
Programming, J. Minker, ed., Morgan Kaufmann Publishers, Inc., Los Altos,
California, 1988, pp. 193-216.

[46] , The well-founded semantics coincides with the three-valued stable

semantics, Fundamenta Informaticae, 13 (1990), pp. 445-463.

[47] A. Roscoe, The Theory and Practice of Concurrency, Prentice-Hall

International, 1998.

[48] R. de Simone, Calculabilit'e et Expressivit'e dans l'Algebra de
Processus

Parall`eles Meije, th`ese de 3e cycle, Univ. Paris 7, 1984.

[49] C. Verhoef, A general conservative extension theorem in process
algebra, in Proceedings IFIP Working Conference on Programming Concepts,
Methods and Calculi, San Miniato, Italy, E.-R. Olderog, ed., IFIP
Transactions A-56, Elsevier, 1994, pp. 149-168.

[50] J. Vrancken, The algebra of communicating processes with empty
process, Theoretical Comput. Sci., 177 (1997), pp. 287-328.

23