A general conservative extension theorem


              in process algebras with inequalities



                Pedro R. D'Argenio1   and  Chris Verhoef 2


                   1Dept. of Computer Science. University of Twente.

                   P.O.Box 217. 7500 AE Enschede.The Netherlands.

                              dargenio@cs.utwente.nl


             2Dept. of Mathematics, Computer Science, Physics and Astronomy.

        Universityof Amsterdam. Kruislaan 403. 1098 SJ Amsterdam. The Netherlan*
 *ds.

                                 chris@fwi.uva.nl



                                   Abstract

        We prove a general conservative extension theorem for transition system*
 * based
     process theories with easy-to-check and reasonable conditions.  The core o*
 *f this
     result is another general theorem which gives sufficient conditions for a *
 *system of
     operational rules and an extension of it in order to ensure conservativity*
 *, that is,
     provable transitions from an original term inthe extension are the same as*
 * in the
     original system. As a simple corollary of the conservative extension theor*
 *em we
     prove a completeness theorem. We also prove a general theorem giving suffi*
 *cient
     conditions to reduce the question of ground confluence modulo some equatio*
 *ns
     for a large term rewriting system associated with an equationalprocess the*
 *ory to
     a small term rewriting system under the condition that thelarge system is *
 *a con-
     servative extension of the small one.We provide many applications to show *
 *that
     our results are useful. The applications include (but are not limited to) *
 *various
     real and discrete time settings in ACP, ATP, and CCS and the notions proje*
 *ction,
     renaming, state operator, priority, recursion,the silent step, autonomous *
 *actions,
     the empty process, divergence, etc.


     1991 Mathematics Subject Classification: 68Q05, 68Q10, 68Q42, 68Q55, 03C05.

     1991 CR Categories: D.3.1, F.1.1, F.3.2, F.4.3.

     Keywords:  structured operational semantics, term deduction system, transi*
 *tion
     system specification, semantic equivalence, semantic preorder, algebraic s*
 *ystem,
     process algebra, conservative extension.



________________________________
   Supported by the NWO/SION project 612-33-006.



                                       1





1    Introduction


In the past few years people workingin the area of process algebra have started*
 * to

extend process theories such as CCS, CSP, and ACP with, for instance, real-time*
 * or

probabilistics. A natural question is whether ornot such an extension is someho*
 *w re-

lated with its subtheory, for instance, whether or not the extension is conserv*
 *ative in

some sense. If we add new operatorsor rules to a particular transition system i*
 *t would

be nice to know whether or not provable transitions of a term in the original s*
 *ystem

are the same as those in the extended system for that term; we will call this p*
 *roperty

operationalconservativity (cf. [GV92 ]). Or, if we extend an axiomatical framew*
 *ork with

new operators, equations, or inequalities itwould be interesting to know whethe*
 *r or

not a theorem (for instance,an equality or an inequality) in the extended frame*
 *work

over original closed terms canalso be derived in the original framework.  When *
 *no

new theorems over closed termsin the original framework are provable from the e*
 *xten-

sion, we call the extensionan algebraic conservative extension. This is a well-*
 *known

property under the name of conservativity; we just added the adjective `algebra*
 *ic' to

prevent possible confusion with theop erational variant.  In particular we say *
 *equa-

tional or inequational conservative extension when the involved algebraic frame*
 *works

are, respectively, equational or inequational specifications.

   A frequently used method to prove that analgebraic theory is a conservative *
 *ex-

tension of a subtheory is term rewritinganalysis.  In pro cess algebra such an *
 *analysis

is often very complex because the rewriting system associated with a process al*
 *gebra

seems to need term rewriting techniques modulo the equations without a clear di*
 *rec-

tion (such as commutativityof the choice).  Moreover,these term rewriting syste*
 *ms

generally have undesirable properties making a term rewriting analysis a comple*
 *x tool

for conservativity.  Such term rewriting systems are not regular, which implies*
 * that

confluence (modulo some equations) is not straightforward and we note that the *
 *term

rewriting relation induced by the rewrite rules does not necessarily commute wi*
 *th the

equality induced by the algebraic system, which means that termination modulo t*
 *hese

equations is not at all easy to prove. Let us briefly mention two examples to m*
 *ake the

problems a bit more concrete. Bergstra and Klop [BK84  ]claim that for the conf*
 *luence

modulo some equations of their term rewritingsystem, they need to check 400 cas*
 *es

(which they left to the reader as anexercise).  Jouannaud communicated to us th*
 *at,

in general, it is very hard (and unreliable) to make such exercises by hand but*
 * they

can possibly be checked by computer. Our second example originates from Akkerman

and Baeten [AB90 ]. They show that a fragment of ACP with the branching | is bo*
 *th

terminating and confluent modulo associativity and commutativity of the alterna*
 *tive

composition. Akkerman told us that it is not clear to him how this result could*
 * also

be established for the whole system and thus yielding a conservativity result. *
 *However,

according to Baeten it is not a problemto establish these results; needless to *
 *say that

their term rewriting analysis is rathercomplicated.


   To bypass the abovementioned problems involving term rewriting, we propose an

alternative method to prove conservativity. We provide ageneral theorem with re*
 *ason-



                                       2





able and easy-to-check conditions giving us immediately the operational and alg*
 *ebraic

conservativity in manycases.  For instance, with our results, the conservativit*
 *y of the

abovementioned systems with problematic term rewriting properties is peanuts. T*
 *he

idea is that we transfer the question of algebraic conservativity to that of op*
 *erational

conservativity rather thanto perform a term rewriting analysis. The only thing *
 *that

remains to be done in order to provethe operational conservativity is to check *
 *our

simple conditions for the operational rules. For the algebraic conservativity w*
 *e more-

over demand completeness of thesubtheory and soundness of its extension.  These

conditions are in our opinion reasonable, because relations between algebraic t*
 *heories

only become important if the theories themselves satisfy such well-established *
 *basic

requirements. Moreover, our result works for a large class of theories, which i*
 *s certainly

not the case with a term rewriting analysis.  All this implies that we give a s*
 *emanti-

cal proof of conservativity, which might be seen as a drawback since a term rew*
 *riting

analysis often is model independent (but seeBergstra and Klop [BK85 ], Fokkink *
 *and

Zantema [FZ94 ],Zantema [Zan95 ] for semantical termrewriting analyses).  Howev*
 *er,

since the paper of Plotkin [Plo81], the use of labelled transition systems as a*
 * model

for operational semantics of process theoriesis widespread; so virtually every *
 *process

theory has an operational semantics of this kind. Moreover, our algebraic conse*
 *rvativ-

ity result holds for all semantical preorders -thus, also equivalences- that ar*
 *e definable

exclusively in terms of transition relations.  We recall some examples of seman*
 *tical

preorders and equivalences which are definable in terms of relation and predica*
 *te sym-

bols only to show that our conditions are quite general.  Examples of equivalen*
 *ces

are trace equivalence,failure equivalence, simulation equivalence,strong bisimu*
 *lation

equivalence, weak bisimulationequivalence, branching bisimulation equivalence, *
 *the

rooted variants of the last two equivalences, etc.  We refer to van Glabbeek's *
 *linear

time - branching time spectra [Gla90 ] and [Gla93 ] for more information on the*
 *se equiv-

alences. In [Gla90 ] and [Gla93 ], references to the origins (and use) of these*
 * semantics

can be found.  Equivalences for true concurrency were also defined in that way,*
 * for

instance, step bisimulation [NT84  , BB93] and pomset bisimulation [BC88 ]. Exa*
 *mples

of preorders are simulation, n-nested simulations [GV92  ],ready simulation [BI*
 *M95 ],

the preorder for the degree of parallelism based on pomset bisimulation of [Ace*
 *91 ],the

"more distributed than" preorders of [Cas93] and [Yan93 ], the preorder for uns*
 *table

nondeterminism of [VB96 ] and the preorders of bisimulation with divergence of *
 *[Abr87 ]

and [Wal90].


   As a result we now can prove conservativity without using the confluence pro*
 *p-

erty. However,it is widely recognised that confluence itself is an important pr*
 *operty,

for instance, for computational or implementational purposes.  So, at this poin*
 *t the

question arises: "Why bother about such a general conservative extension theore*
 *m if

we still have to prove confluence for each particular system and get the conser*
 *vativity

as a by-product?" The answer is that once we have the conservativity we can con*
 *sid-

erably reduce the complexity of theground confluence as a by-product. We prove a

general reduction theorem stating that in many cases a conservative extension i*
 *s ground

Church-Rosser modulo some equationsif the basic system already has this propert*
 *y.



                                       3





For instance, the 400cases of Bergstra and Klop [BK84 ] reduce to a term rewrit*
 *ing

analysis with only five rewrite rules and two equations. We should note, howeve*
 *r, that

they prove (modulo 400 cases!) the confluence for open terms (although they only

need the closed case), whereas our reduction theorem gives the closed case only*
 *. In

fact, we show that conservativity and ground Church-Rosser are, in some sense, *
 *equally

expressive prop erties.

   Another advantage of our approachis that it also works for process algebras *
 *with

really bad term rewriting properties,such as process algebras containing the th*
 *ree| laws

of Milner, where the term rewriting approach breaks down; see,e.g., [BK85  ]. W*
 *e will

treat these examples in this paper.


   Now that we have given somemotivation for this paper we discuss its organisa*
 *tion.

In section 2 we recall some generalSOS definitions of Verhoef [Ver95] and in se*
 *ction 3

we recall some concepts of algebraicsystems. We provide a running example to el*
 *uci-

date the abstract notions. In section 4 we formally define the notions of opera*
 *tional

and algebraic conservativity. Then we prove a general operational conservativit*
 *y the-

orem, a general inequational conservativity theorem and a simple corollary conc*
 *erning

completeness. Also here we provide our running example. In the next section we *
 *recall

some basic term rewriting terminology toprove the abovementioned reduction theo*
 *rem

on the ground Church-Rosser prop erty modulo some equations.  Insection 6 we gi*
 *ve

the reader an idea of the applicability of our general theorems. Surprisingly, *
 *wecould

not find any conservativity result in the literature for which our conservativi*
 *tytheorem

could not be applied, as well. The last section contains concluding remarks.



1.1    Related work


In this subsection we briefly mention related work. Nicollin and Sifakis [NS91 *
 *] prove

conservativity_in some particular cases_using the same general approach as we p*
 *ro-

pose in this paper, namelya semantical approach. We will discuss their conserva*
 *tivity

results (and new results) in section 6.The notion that we call in this paper op*
 *erational

conservativity originates from Groote and Vaandrager [GV92 ] under the name con*
 *ser-

vativity. In Groote[Gro93 ], Bol and Groote [BG91 ], and Fokkink and Verhoef [F*
 *V95 ]

this notion also appears. In all these papers this notion is used for a differe*
 *nt pur-

pose than ours. Aceto, Bloom and Vaandrager [ABV92  ] introduce a so-called dis*
 *joint

extension, which is a more restricted form of an operational conservative exten*
 *sion;

they need this restriction for technical reasons. They present an algorithm gen*
 *erating

a sound and complete axiomatisation if the operational rules satisfy certain cr*
 *iteria.

Bosscher [Bos94] studied term rewriting properties of such axiomatisations by l*
 *ooking

at the form of the operational rules.



                                       4





2    Some general SOS definitions


In this section we briefly recall some notions concerning general SOS theory th*
 *at we will

need later on in Section 4. We followVerhoef [Ver95] since this paper gives the*
 * most

general setting. To elucidate the formal notions we intersperse them with a run*
 *ning

example.


   We assume that we have an infinite set V of variables with typical elements *
 *x;y ; z; : :.:

A (single sorted) signature  is a set of function symbols together with their a*
 *rity. If

the arity of a function symbol f2  is zero we say that f is a constantsymbol.  *
 *The

notion of a term (over ) is defined as usual: x 2 V is a term; if t1; : :;:tn a*
 *re terms

and if f 2 is n-ary then f(t1; : :;:tn) is a term. Aterm is also called an open*
 * term;

if it contains no variableswe call it closed. We denote the set of closed terms*
 * by C()

and the set of (open) terms by O(). We also want to speak about variables occur*
 *ring

in terms: let t 2 O() then var(t)  V is the set of variables occurring in t.

   A substitution oeis a map from the set of variables into the setof terms ove*
 *r a given

signature. This map can easily be extended to the set of all terms by substitut*
 *ing for

each variable occurring in an op enterm its oe-image.


Definition 2.1 A term deductionsystem is a structure (;D) with  a signature and*
 * D

a set of deductionrules. The set D = D(Tp;Tr) is parameterised with two sets, w*
 *hich

are called (following usual process algebra terminology) respectively the set o*
 *f predicate

symbols and the set of relation symbols. Let s; t; u 2 O(), P 2 Tp, and R2 Tr. *
 *We

call expressions P s;:P s, tRu, and t:R formulas. We call the formulas P s and *
 *tRu

positive and :Ps and t:R negative1. If S is a set of formulas we write PF(S) fo*
 *r the

subset of positive formulas of Sand NF (S) for the subset of negative formulas *
 *of S.

   A deduction rule d 2 D has the form

     H_

      C

with H a set of formulasand C a positive formula; we willalso use the notation *
 *H=C.

We call the elements of H the hypotheses of d and we call the formula C the con*
 *clusion

of d. If the set of hypotheses of adeduction rule is empty we call such a rule *
 *an axiom.

We denote an axiom simply by its conclusion provided that no confusion can aris*
 *e. The

notions "substitution", "var", and "closed"extend to formulas and deduction rul*
 *es as

expected. Note that the overload of the symbol C in C() and H=C is harmless.

   LetSd = H=C a deduction rule with C= P s or C= sRs0. Let X = var(s) and let

Y =  fvar(t0)j tRt02 Hg. Ifvar(d) = X [Y we call d pure. A term deduction system

is called pure if allits rules are pure.                                       *
 *     2


   Note that arbitrary many premises are allowed in the set of hypotheses of a *
 *deduction

rule. This generality is useful, for instance, in real-time process algebras wh*
 *ere it is very

natural to have continuously many premises (see [MT90  , Yi90, Klu93].)
________________________________
  1The idea behind t:R is that there is no term s such that tRs. We chose this *
 *notation among

others like :tR, :Rt, or :(tR) since itseems to be the most accurate one.



                                       5





Example 2.2   As a running example,we present the operational semantics of the *
 *pro-

cess algebra with parallel composition PA [BK84  , BW90 ] and the basic process*
 * algebra

with relative discrete time: BPAdt [BB92 ]. We will consider separately BPA (ba*
 *sic pro-

cess algebra), MRG, a mo dule that defines parallel processes without communica*
 *tion

and DT, which is an extension to discrete timed processes.

   The signature of BPA contains constants a of a set A of atomic actions,alter*
 *native

composition, denoted +, and sequential composition (). The signature of MRG (for

merge) contains paral lelcomposition ormerge (jj) and the leftmerge (jj_). The *
 *signature

of DT contains +,  and the discrete time unit delay (oed).

   It is easy to see that the signatures of BPA, MRG, and DT with their operati*
 *onal

rules in Table 1 form termdeduction systems.  These term deduction systems havep

relations _ a! _for all a 2 A,a relation _ oe!_with oe =2A and predicates _ a! *
 *  for

all a 2 A. The intended interpretation of x  a! x0ispthat a process x mayexecut*
 *e an

action a and evolve into x0. The meaning of x  a!   is that x terminates succes*
 *sfully

after the execution of a. With x  oe!x0 we mean that apro cess x evolves into x*
 *0by

letting a time unit pass. We write x 6 oe!instead of x:  oe!.

   Our running examples are the combination of BPA with either MRG or DT. The s*
 *ig-

nature of the term deduction system PA is the union of signature of BPA and MRG*
 *. The

operational rules are those of BPA and MRG combined. Similarly,the term deducti*
 *on

system BPAdt is obtained by combining BPA and DT. It is easy to check that PA a*
 *nd

BPAdt  are indeed term deduction systems. We will later on use them to demonstr*
 *ate

our results.                                                                   2

   _________________________________________________________________________

   _  (i)                                                      p            _
                  p             ___x_a!_x0___            _x_a!____
             a  a!                    a                       a
   _                            x  y  ! x0 y             x  y !  y          _

   _                                                 p                      _
                     ___x_a!_x0___            __x__a!_____
                                                       p
                      x + y a! x0              x+ y  a!
                           a! x0               y+ x a!p
   _                  y+ x                                                  _

   __________________________________________________________________________

   _  (ii)                            _ (iii)                               _
      ___x__a!x0____   ___x_a!_x0___                     x__oe!x0__y_oe!y0_
                                          oed(x) oe!x
       xjjy  a!x0jjy   xjj_y  a!x0jjy                     x + y oe!x0+ y0
             a!yjjx0
   _   yjjx                           _                                     _

   _          p                p      _                                     _
        _x__a!____       _x_a!_____      ___x_oe!x0___    x__oe!x0__y_6oe!_

        xjjy  a!y        xjj_y a! y      x  y  oe!x0 y      x + y oe!x0
              a!y                                           y+ x oe!x0
   _    yjjx                          _                                     _

   __________________________________________________________________________

                Table 1: Operational rules for BPA, MRG and DT



                                       6





Definition 2.3 Let T be a term deduction system. Let F (T ) be the set of all c*
 *losed

formulas over T. We denote the set of all positive formulas over T by PF (T) an*
 *d the

negative formulas by NF(T ).  Let X PF (T ). We define when a formula ' 2 F (T )

holds in X; notation X` '.


     X ` sRt   if sRt 2 X;

     X ` Ps    if P s 2 X;

     X ` s:R   if 8t 2 C (): sRt =2X;

     X ` :Ps   if P s2=X:


                                                                             2


   The purpose of a term deduction system is to define a set of positive formul*
 *as that

can be deduced using the deduction rules. For instance, if the term deduction s*
 *ystem

is a transition system specification then a transition relation is such a set. *
 *For term

deduction systems without negative formulas this set comprises all the formulas*
 * that

can be proved by a well-founded proof tree. If we allow negative formulas in th*
 *epremises

of a deduction rule it is no longer obvious which set of positive formulas can *
 *be deduced

using the deduction rules. Bloom, Istrail, and Meyer [BIM88 , BIM95 ] formulate*
 * that a

transition relation must agree witha transition system specification. We will u*
 *se their

notion; it is only adapted to incorporate predicates.


Definition 2.4 Let T = (;D) be a term deduction system and let X PF (T) be a

set of positive closed formulas.We say that X agreeswith T if for every formula*
 * ' 2 X

we have that there is a deduction rule instantiated with a closed substitution *
 *such that

the instantiated conclusion equals 'and all the instantiated hypotheses hold in*
 * X, and

vice versa. More formally: Xagrees with T if


     ' 2 X  () 9 H=C 2 D; oe : V ! C() : oe(C) = ';8h 2 H : X ` oe(h):


                                                                             2


   There are several ways to give meaning to a set of formulas that agree with a

given term deduction system.In [Gla95 ] an elaborate study on the meaning of ne*
 *gative

premises is given reviewing known interpretations and discussing new ones. We m*
 *ention

the uniqueness approach of [BIM95 ],the stratification techniques described in *
 *[Gro93 ],

the reduction techniques of [BG91 ],and the complete models of [Gla95 ].In this*
 * paper

we focus on applications instead of theory so we choose to work with a techniqu*
 *e that

is easily applicable: the stratification technique described in [Gro93 ]. We no*
 *te that our

results are also valid for moregeneral models such as stable ones [Gla95]. We r*
 *efer the

interested reader to [FV95 ] for details.


Definition 2.5 Let T = (;D) be a term deduction system. Amapping S :PF (T )!

ff for an ordinal ff is called a stratification for T if for all deduction rule*
 *sH =C 2 Dand

closed substitutions oethe following conditions hold:



                                       7





   1.for all h 2 PF (H),S (oe(h))  S(oe(C));


   2.for all s:R 2NF (H )and for all t 2 C(), S(oe(sRt)) < S(oe(C));


   3.for all :P s 2 NF (H), S(oe(P s)) < S(oe(C)).


We call a term deduction system stratifiable if there exists a stratification f*
 *or it.    2


Example 2.6   When dealing with GSOSlanguages [BIM95 ], a stratification is obt*
 *ained

just by measuring the complexity of a positive formula in terms of counting a p*
 *articular

symbol occurring in the conclusion of a rulewith negative antecedents. This doe*
 *s not

hold in general for any term deduction system but can be adopted as a rule of t*
 *humb. In

our case,for BPA and PAthe stratifications are trivial since they have no negat*
 *ive rule.

We can see in Table 1 that BPAdt  has only one rule with a negative antecedent.*
 * In its

conclusion we find the function symbol +. Let t be a closed term with n occurre*
 *nces of

this symbol. Then the map S(t oe!t0) = n is a stratification (t0is a closed ter*
 *m). This

means that the term deduction system BPAdt makes sense. Informally speaking this

means that the transition relations andthe predicates are defined by the operat*
 *ional

rules.                                                                        2


   Next, we assign to a term deduction system a(regular) ordinal that expresses*
 * a

uniform upper bound of the number of premisesin the deduction rules.  We use th*
 *is

upper bound for proof-technical reasons.


Definition 2.7 Let V  be a set. If 0  jV j < @0we define the degree ofV , denot*
 *ed

d(V ), to be !0. If jV j = @fffor an ordinal ff 0, we define d(V ) = !ff+1.

   Let T = (;D) be a term deduction system. The degree d(H=C) of a deduction

rule H=C 2 D is the degree of its set of positive premises: d(H=C) = d(PF (H)).

Let !ff= supfd(H=C)j H=C 2 Dg. The degree d(T) of a term deduction system T

is !0if ff = 0 and !ff+1otherwise.                                             *
 * 2


Example 2.8   The reader can see that for every ruleH =Cin Table 1, jPF (H)j  2.

Thus, d(H=C) = !0, which implies that the degree of every term deduction system*
 * in

our example is !0. In particular, d(BPA ) = d(PA ) =d(BPAdt ) = !0.            *
 *   2


   Next, we will define a set of positive formulas from which we will show that*
 *it agrees

with a given term deduction system.


Definition 2.9 Let T = (;D) be a term deduction system and let S : PF (T) ! ff

be a stratification for an ordinal number ff. We define a set TS PF (T) as foll*
 *ows.
          [            [
     TS =   Ti;   Ti=      Ti;j:
         i<ff        j<d(T )


We will need unions over Ti and Ti;jin proofs; so,we introduce the following no*
 *tations
         [                      [
     Ui=    Ti0(i  ff);  Ui;j=    Ti;j0(j  d(T)):
         i0<i                  j0<j



                                       8





Now we define for all i < ffand for all j < d(T) the set Ti;j:

             n
     Ti;j =    'jS(') = i; 9H=C 2 D and oe : V ! C()with oe(C) = ';
                                                                            o
                  8 h2 PF (H) : Ui;j[ Ui` oe(h) and 8 h 2 NF(H) : Ui ` oe(h) :


                                                                             2



Example 2.10   We will elucidate the above definition by calculating a specific*
 * set TS.

The example is taken from [Ver95] and is based on an example of [Gro93 ]. Consi*
 *der the

term deduction system T with only a constant c in the signature, and rules:Pnc=*
 *Pn+2c

and :P2nc=P0c with n  0.  Then S : PF (T) ! 2!0 defined as S(P2nc) = !+ n

and S(P2n+1c) = n is a stratification for T . Moreover d(T) = !0. Now, we calcu*
 *late

TS. Since there are no positive premises we havethat Ti;0= Ti;jfor all j < d(T)*
 *. So

Ti= Ti;0. It is not hard to verify that for all n  0 we have T2n= T!0+2n+1= ;, *
 *T2n+1=

fP4n+3cg,and T!0+2n= fP4ncg. So we find that TS= fP0c; P3c; P4c; P7c; P8c; P11c*
 *; :g:.:

                                                                             2



   The next theorem is taken from Verho ef [Ver95 ] but its proof isessentially*
 * the same

as a similar theorem due to Groote [Gro93].



Theorem 2.11    Let T = (; D) be a term deduction system and let S : PF (T) ! ff

be a stratification for an ordinal number ff. Then TS agrees with T.  If S0is a*
 *lso a

stratification for T then TS = TS0. That is, every stratifiable term deduction *
 *system has

a unique set of formulas obtained as in Definition 2.9 that agrees with it.



Example 2.12   Since the term deduction systems of our running example arestrat*
 *ifi-

able it follows from the abovetheorem that the rules of BPA, PA, and BPAdt dete*
 *rmine

a transition relation (with predicates)on closed terms.                        *
 *    2



Definition 2.13  LetT  = (;D) be a term deduction system and let F be a set

of formulas. The variable dependency graph of F is a directed graph with variab*
 *les

occurring in F as its nodes. The edge x ! y is an edge of the variable dependen*
 *cy

graph if and only if there is a positiverelation tRs 2 F with x 2 var(t) and y2*
 * var(s).

   The set F is called well-founded if every backward chain of edges in its var*
 *iable

dependency graph is finite. Adeduction rule is called well-founded if its set o*
 *fhypothe-

ses is so. A term deduction system is called well-founded if all its deduction *
 *rules are

well-founded.                                                                 2



Example 2.14   It is easy to see that the rules of our running examples are wel*
 *l-founded.

                                                                             2



                                       9





3    Some concepts of algebraic systems


We want to formulate a general theorem in which both equational specifications *
 *and

inequational specifications play a crucial role. For completeness sake we will,*
 *therefore,

recall the necessary notions in this section.  We mainly follow [Gil76]; an alt*
 *ernative

approach can be found in [Wec92 , Hen88].

   Next, we define the notion of an algebraic system, or abstract algebra. It w*
 *ill turn

out that both equational and inequational systems are special cases of an algeb*
 *raic

system.



Definition 3.1 An algebraic system(or abstract algebra ) is a structure (; A; P*
 *) where

 is a signature, P  O()  O() is a set of predicates, and A is a set of axioms

having the form fpi(si; ti)ji 2 Ig ) p(s; t) where I  isa finite set, s; t; si;*
 * ti2 O()

and p; pi2 P. We call the set fpi(si; ti)ji 2I g the conditions. If the set of *
 *conditions

is empty we write p(s; t) instead of ; ) p(s; t).  Note that the overload of th*
 *e word

predicate with that of definition 2.1 isharmless.                              *
 *    2



   The predicate symbols in algebraic systems are mostoften relations such as e*
 *quality

or, in our case, inequality.  Next, we axiomatise the most common properties of*
 * such

predicates.



Definition 3.2 Let (; A; P) where  be an algebraic system. Let p 2 P, f 2  be

n-ary, and x; y; z; xi; yi2 V then,


   fflif p(x;x) 2 A we say that p is reflexive;


   fflif fp(x;y)g ) p(y; x) 2 Awe say that p is symmetric;


   fflif fp(x; y); p(y; z)g ) p(x;z) 2 A we say that p is transitive;


   fflif p is both reflexive, symmetric, andtransitive, we say that p is an equ*
 *ivalence;

     and


   fflif fp(x1; y1); : :;:p(xn; yn)g ) p(f(x1; : :;:xn); f(y1; : :;:yn)) 2 A we*
 * say that p

     preserves f.


We refer to the first axiomas the axiom of reflexivity and to the others likewi*
 *se. We

refer to some or all of the above axioms loosely as the special axioms.        *
 *     2



   Now we are able to give precise definitions of equational and inequational s*
 *pecifica-

tions.



Definition 3.3 An inequational specification is an algebraic system with a sing*
 *le pred-

icate that is reflexive,transitive and preserves all functions in the signature*
 *. Anequa-

tional specification is an inequational specification such that its predicate i*
 *s also sym-

metric.                                                                       2



                                      10





   From now on we will tacitlyassume the presence of the axioms of reflexivity,*
 *transi-

tivity, and preservation of functions in the inequational specifications, and i*
 *n addition

symmetry in the equational specifications that we will discuss in the examples *
 *and

applications.


Example 3.4   Now we give a few examples ofequational specifications and inequa*
 *tional

ones. We present some axioms and inequalities that fit our running example in a*
 * natural

way. Web egin with the equational specification called BPA. Its signature is th*
 *esame

as the signature of the term deduction system also called BPA. Its axioms are l*
 *isted in

Table 2.(i). This is a known system; see [BW90  ] for its use.

   The equational specification BPAdt is constructed in the same way: take the *
 *sig-

nature of its term deduction system andits axioms are the ones of the equational

specification BPA and the oneslisted in Table 2.(iv). Also this equational spec*
 *ification

is known,see [BB92 ]. To demonstrate our general theorems we will alsoneed the *
 *equa-

tional specification DT formed by the same signature as its term deduction syst*
 *em, and

axioms in Table 2.(iv). In fact, BPAdt is the sum of the modules BPA and DT .

   Now we give an example of an inequational specification.  Theinequational sp*
 *eci-

fication PA  consists of the signature of the term deduction system PA together*
 * with

the axioms in Table 2.(i-iii ). In this case, expressions having the form s = t*
 * stand for

the two axioms s  t and t  s. From now on, we will assume s = t as an abbrevia-

tion for those two inequalitiesin an inequational specification. Thus, for inst*
 *ance, the

expression A3 stands for the two axioms x + x  x and x  x + x.

   Similar to BPAdt we will define two modules that,when combined, form PA  . We

will use those two inequationalsp ecifications to show our main results for ine*
 *quational

systems. The first one called BPA   has the signature of the equational specifi*
 *cation

BPA, and as axioms those inTable 2.(i-ii) (note that there are eleven axioms). *
 *The

inequational specification expressing the parallel side of PA   is called MRG  *
 *  and has

the same signature than PA  and the nine axioms in Table 2.(iii).

   Now that we have given examples of definition 3.3 we will briefly discuss th*
 *eir

axioms. Axioms A1-5 and M1-4 are the well known axioms for the PA process alge-

bra [BK84 , BW90  ]; PA is a simple language with sequential, alternative and p*
 *arallel

composition. Axioms DT1 and DT4 originate from [BB92 ]; BPAdt  is a sequential *
 *basic

language that incorporates discrete time features.  See also [BV95 ] for a syst*
 *ematic

treatment of the above equational specifications. We discuss the inequational a*
 *xioms.

SM stands for simulation; to the best of our knowledge this axiom is intro duce*
 *d here.

MP stands for "more parallel"and embodies the idea that xjjy has a "more parall*
 *el

behaviour" than x  y. Note that for closed terms,MP can be derived with inducti*
 *on

on the size of x from the other axioms in PA  .                                *
 *   2


   Noteworthy perhaps is that in some treatments of equational theories, the no*
 *tion

of equational specification does not incorporate any defined behaviour of the e*
 *quality

predicate, but its suggestive name (see, for instance, [Wec92 , Hen88 , BW90  ]*
 *) or a

tacitly assumed presence of equational logic. The meaning of the equality predi*
 *cate is

often expressed in the notion of derivability. Normally this would not give ris*
 *e to any



                                      11





   _________________________________________________________________________

   _  (i)                                                                   _
   _                                                                        _

   _  A1     x + y = y+ x                 A4      (x + y)  z =x  z + y z    _

   _  A2     x + (y + z) = (x + y) + z    A5      (x  y)  z =x  (y  z)      _

   _  A3     x + x = x                                                      _

   __________________________________________________________________________

   _  (ii)                                                                  _
   _                                                                        _

   _  SM     x  x + y                                                       _

   __________________________________________________________________________

   _  (iii)                                                                 _
   _                                                                        _

   _  M1     xjjy = xjj_y+ yjj_x          M3      a  xjj_y =a  (xjjy)       _

   _  M2     a jj_x = a  x                M4      (x + y)jj_z =xjj_z +yjj_z _

   _                                                                        _
   _  MP     x  y  xjjy                                                     _

   __________________________________________________________________________

   _  (iv)                                                                  _
   _                                                                        _

   _  DT1    oed(x) + oed(y) = oed(x + y) DT2     oed(x)  y =oed(x  y)      _

   __________________________________________________________________________

                    Table 2: Axioms for the runningexamples



problems since mostly the application isonly equational specifications. In this*
 * paper,

such an approach would be very confusing since there would be no distinction be*
 *tween

the definition of equational specification and that of inequational specificati*
 *on. To make

this distinction apparent we put the special axioms in the definition of (in)eq*
 *uational

specification instead of in the definition ofderivability. As a result the next*
 * definition of

derivability only contains the substitutivity property since that one is not al*
 *gebraically

expressible.



Definition 3.5 Let S = (; A; P) be an algebraic system. Let s; t 2 O(). A state-

ment p(s;t) can be derived from A, notation A ` p(s; t), ifthere is an axiom in*
 * A such

that, together with a given substitution, the premises of the axioms can be der*
 *ived from

A, and the conclusion is p(s;t), that is, let oe: V ! O(), then

                                   )
      fpi(si; ti)ji 2 Ig ) p(s; t) 2 A
                                      =)  A ` p(oe(s);oe (t))
      and 8i 2 I:A ` pi(oe(si); oe(ti))


We call this property the substitutivity axiom.                                *
 *   2



   In the next definition, we borrow the notion ofA-assignments from [Hen88 ].



Definition 3.6 An algebra is a set A of elements, the carrier ,together with ce*
 *rtain

functions over A of arity n 0.



                                      12





   Let  be a signature. A-algebra A is an algebrawith a function fA for each fu*
 *nction

symbol f 2 with the same arity. Such a correspondence is called an interpretati*
 *on. An

A-assignment for V is a function ae : V ! A.Let hae: O() ! A be the homomorphism

defined inductively as follows:


   fflhae(f(t1; : :;:tn)) = fA(hae(t1); : :;:hae(tn)); and


   fflhae(x) = ae(x).


It can be shown that haeis the unique homomorphism from O() to A such thathae(x*
 *) =

ae(x) [Hen88].

   Let S = (; A; P) be an algebraic system. Let A be a -algebra with carrier set

A. Let R be a set of binary relations on A with one relation pA for each p 2 P.*
 * For

s;t 2 O() we say that p(s; t) holds in A under R, notation A=R  j= p(s;t) if fo*
 *r all

A-assignment ae for V, we have pA(hae(s);hae(t)).

   A is a sound axiomatisation with respect to R for A if for all s;t 2 O(), p *
 *2 P


     A ` p(s;t) =) A=R  j=p(s; t):


Moreover, if for all closed terms s; t 2 C() and p 2 P


     A ` p(s;t) () A=R  j=p(s; t)


then A is called a complete axiomatisation with respect to R for A.            *
 *    2



A model for our examples


Now, we will briefly discuss the semantics of our running examples and give the*
 * nec-

essary definitions. We state this in a separate paragraph since some new result*
 *s are

introduced. We will use them later on to demonstrate our main theorems. First w*
 *e give

the definition of simulation and that of bisimulation [Par81], adapted to the r*
 *unning

examples.



Definition 3.7 A binary relation Son the set of closed PA terms is a simulation*
 * if for

all (s;t) 2 S and for all a 2 A, the two following transfer propertieshold:


     - 8s0: s a! s0=) 9t0: t  a!t0and (s0; t0) 2 S,
            p          p
     - s a!    =)  t a!  .


If there is a simulation Ssuch that (s; t) 2 S, then s is simulated by t, notat*
 *ion sae+t.

   Now we give the well-known definition of bisimulation modified to our case. *
 *First,

extend the notion of simulation by considering also the relation  oe!. A binary*
 * relation S

on the set of closed BPAdt terms is a (strong) bisimulation if Sand S1  are sim*
 *ulations.

If there is a bisimulation S such that (s; t) 2 S, then s and t are bisimilar ,*
 * notation

s $__t.                                                                        2



                                      13





   The facts that BPA is sound and complete modulo strong bisimulation and that

BPAdt  is sound with resp ect to strong bisimulation equivalence are well-known*
 *. We

refer to [BW90  , BV95, BB92 ] for details.

   Since the inequational specifications are new here we will focus more on tho*
 *se.



Lemma 3.8    The inequational specifications BPA   and PA  are sound axiomatisa*
 *tions

with respect tothe ae+model induced bytheir term deduction systems.

   The inequational specification BPA   is complete with respect to the ae+mode*
 *l induced

by the BPA term deduction system.



Proof. (Sketch) In order to prove that PA   is a sound axiomatisation with resp*
 *ect to

the ae+model induced by the PA term deduction system,it is enough to prove that*
 * ae+

is reflexive,transitive, and preserves all functions in PA (i.e.+aeis a precong*
 *ruence for

PA) and moreover,that for every axiom s  t of PA  in Table 2 with free variable*
 *s in

V, the relation


     S = f(oe(s);oe(t))j oe substitutes closed terms for variablesVing [ Id


is a simulation. As a consequence, BPA   is also a sound axiomatisation with re*
 *spect

to ae+.

   Moreover, BPA   is a complete axiomatisation with respect to the ae+model in*
 *duced

by the BPA term deduction system. The proof follows by induction on the size of*
 * the

basicpterms [BW90  ] by considering that if t is a basic term then t  a!t0(resp*
 *ectively

t  a!  ) if and only if t has the form t00+ (a  t0) (respectively t00+a) modulo*
 * axioms

A1, A2.                                                                      2



   The equational specification PA  is also complete as we will show using our *
 *results

later on.



4    Operational and algebraic conservativity


In this section we prove ageneral operational conservative extension theorem wi*
 *th easy

to check conditions.We also study conservativity on algebraic systems and we st*
 *ate that

algebraic conservative extension can be derived from conservativity on models w*
 *hich

are complete for the original algebraicsystem.  If we moreover have the elimina*
 *tion

property for the new operators we also have completeness of the extension. By c*
 *ombin-

ing both results, weprove as a corollary a general inequational conservativeext*
 *ension

theorem. We will use our running examples to elucidate the definitions and to d*
 *emon-

strate our results. We recall that since an equational specification is a speci*
 *al case of an

inequational specification,all our results also hold for equational specificati*
 *ons, which

is indeed a very important subcase.



Definition 4.1 Let 0 and 1 be signatures. If for all f 20" 1 the arityof f in 0

is the same as the arity of f in 1 then 0 1, called the sum of 0 and 1, is the



                                      14





signature 0[1. Note that  is not simply the union of twosignatures since the sum

could be undefined if the signatures share afunction symbol having different ar*
 *ity for

each one of them.                                                             2


Example 4.2   We denote by BPA the signature of BPA and similarly for MRG, DT,

etc. It is easy for the reader to check that BPA MRG  is defined and is equal t*
 *o the

signature of PA, and that BPADT is also defined and equals the signature of BPA*
 *dt .

                                                                             2


Definition 4.3 Let T i=(i; Di) be term deduction systems with predicate and rel*
 *a-

tion symbols Tipand Tirrespectively (i =0; 1). Let 01be defined. The sum T0T1,

called the sum of T0 and T1, is the term deduction system (0  1;D0 [ D1) with

predicate and relation symbols T0p[T1pand T0r[Tr1.                             2


Example 4.4   Consider the term deduction systems definedin Example 2.2. It is *
 *easy

to see that BPA  MRG   =PA  and BPA  DT  = BPAdt.                          2



4.1    Operationalconservativity


Next, we formally definethe notion of an operational conservative extension and*
 * the

notion of an operational conservative extension up to some semantical preorder *
 *which

is defined exclusively in terms of predicate and relation symbols. This is not *
 *a serious

restriction since many preorders aredefined in this way.

   The notions operational conservative extension and operational conservative *
 *exten-

sion up to strong bisimulation equivalence were already defined by Groote and V*
 *aan-

drager [GV92 ] (without the adjective `operational') where they usedthe first n*
 *otion

to characterise the completed tracecongruence induced by their pure well-founded

tyft/tyxt format. Groote [Gro93 ] gives the two definitions in the case that ne*
 *gative

premises come into play. He used operational conservativity for a similar chara*
 *cterisa-

tion result as in [GV92 ]. In Bol and Groote [BG91 ] the approach of Groote [Gr*
 *o93] is

placed in a wider perspective. Aceto,Bloom and Vaandrager [ABV92  ] use a restr*
 *icted

form of operational conservative extension for technical reasons; they call it *
 *disjoint

extension. Fokkink and Verhoef [FV95 ] studied conservative extensions in stabl*
 *e term

deduction systems with bindings and substitutions.  Some corollaries of these r*
 *esults

are given in [D'A95 ] for term deduction systems with unique stable model and t*
 *erms

without bindings and substitutions.We will use the notion of operational conser*
 *vativity

to prove inequational conservativity.


Definition 4.5 Let T i= (i; Di) be term deduction systems.  Let T = (; D) =

T0 T1 be defined and let D =D(Tp;Tr). The term deduction system T is called an

operational conservative extension of T0 if it is stratifiable and for all s; u*
 * 2 C(0),for

all relation symbols R 2Tr and predicate symbols P 2 Tp, and for all t 2 C () we

have


     TS ` sRt () TS00` sRt  and   TS ` P u () TS00`P u



                                      15





where S is a stratification forT  and S 0is a stratification for T0 (take for i*
 *nstance S 0

to be the restriction of S to positive formulas of T0).                        *
 *     2



Definition 4.6 Let T i= (i; Di) be term deduction systems with T  = (;D) =

T0 T1defined and let D =D (Tr; Tp). Let  be some semantic preorder or equivalen*
 *ce

defined in terms of relation and predicate symbols only, i.e., defined in terms*
 * of symbols

into the set Tr[ Tp.  T isan operational conservative extension of T0up to  if *
 *for all

s;t 2 C(0), s2  t ()  s20t, where 20 and2   are thepreorder or equivalence

interpreted in terms of predicate and relation symbols of T0 and T, respectivel*
 *y.

   We will often use  to denote a preorder and j for an equivalence.           *
 *  2



   Many preorders and equivalences are definable in terms of relation and predi*
 *cate

symbols only. First we will mention a number of equivalences and then alist of *
 *preorders

that are defined as such.

   Examples of equivalences that satisfy ourrestrictions are trace equivalence,*
 * failure

equivalence, simulationequivalence, strong bisimulation equivalence (we recall *
 *that we

defined this equivalence in 3.7), weak bisimulation equivalence,branching bisim*
 *ulation

equivalence, the rooted variants of the last two equivalences, etc.  We refer t*
 *o van

Glabbeek's linear time - branching timesp ectra [Gla90 ] and [Gla93 ] for more *
 *informa-

tion on these equivalences.Equivalences for true concurrency were also defined *
 *in that

way, for instance, step bisimulation [NT84 , BB93 ] and pomset bisimulation [BC*
 *88 ].

   Also many important preorders are defined in terms of relation and predicate*
 * sym-

bols. An example of a preorder is simulation that we defined in Definition 3.7.*
 * Other

examples are n-nested simulations [GV92 ], ready simulation [BIM95 ], the preor*
 *der for

the degree of parallelism based on pomset bisimulation of [Ace91 ],the "more di*
 *stributed

than" preorders of [Cas93] and [Yan93 ], the preorder for unstable nondetermini*
 *sm

of [VB96 ], and the preorders of bisimulation with divergence of [Abr87 ] and [*
 *Wal90].

   For all the above equivalences and preorders, the following theorem holds. I*
 *t states

that if an extension is operationally conservative, it is also operationally co*
 *nservative

up to some preorder definable in terms of relations and predicates only.



Theorem 4.7   Let Ti = (i;Di) be term deduction systems and let T = (;D) =

T0 T1 be defined. If T is an operational conservative extension of T0, then it *
 *isalso

an operational conservative extension up to , for any preorder (thus equivalenc*
 *e)

defined in terms of predicate and relation symbols only.



Proof. (Sketch) Let s;t 2 C(0). Since T is an operational conservative extensio*
 *n of

T0, the state-transition diagrams (orb etter:  the term-relation-predicate diag*
 *rams) of

s in both T and T0 are the same, and so are the term-relation-predicate diagram*
 *s of

t.  Let  be a preorder defined in terms of relation and predicate symbols. Beca*
 *use

  is defined in the same way for relation and predicate symbols in T 0as 0, and

the term-relation-predicate diagrams ofs and t are the same in both term deduct*
 *ion

systems, s 0t implies s   t. The counterpositive is proved analogously.        *
 * 2



                                      16





   After publishing [Ver95], Verhoef found out thatin his conservativity theore*
 *m the

ntyft/ntyxt format condition was not necessary.  Groote was pleasantly surprise*
 *d by

this fact.  Shortly thereafter,  Verhoef was even more surprised since in [BG91*
 * ] the

conservativity theorem already lacked the ntyft/ntyxt format proviso. Groote cl*
 *arified

this mystery by stating that his co-author, Roland Bol, apparently must have se*
 *en that

the condition was not necessary andhad dropped it tacitly.  What theydid  discu*
 *ss

in depth [BG91 ] is their way of giving meaning to negative premises, which is *
 *more

general than stratifiability.  We recall that this paper is focussed towards pr*
 *actical

applications. Since the stratification condition is, inour opinion, more practi*
 *cal than

their criterion we chose for stratifiability. However,we claim that our theorem*
 * can also

be proved for that more general notion.  Infact, in [D'A95 ] and [FV95 ] conser*
 *vativity

theorems have been proved with even more general conditions than the one presen*
 *ted

in [BG91 ]. Anyway, theimplications of the fact that the ntyft/ntyxt format con*
 *dition

can be dropped are immense.  The cross-over between term deduction systems and

conditional term rewriting is not longertheoretical [GV92  ],as can be seen in *
 *this paper

and in, for instance, [FV95 ].

   After we put the next theorem in context,we discuss the theorem itself. It g*
 *ives

sufficient conditions such thatT 0 T1is an operational conservative extension o*
 *f T0.

The theorem is on the one hand a generalisation of a similar result in [BG91 ],*
 * since we

allow new rules to contain original function symbols in the left-hand side of a*
 * conclusion

such as, for instance, rules in Table 1.(iii) of our running example. Moreover,*
 * Boland

Groote require for the new rules that the left-hand side of a conclusion may no*
 *t be a

single variable,whereas we do not have such a restriction. On the other hand,we*
 * use

stratifications which is less general than the criterion stated in [BG91 ].


Theorem 4.8   Let T0 = (0;D0) be a pure well-founded term deduction system.  Let

T1 = (1;D1) be a term deduction system. If there is a conclusion sRt or Ps of a

rule d12 D1 with s 2 O(0), we additional ly require that

  1. d1 is pure and well-founded,


  2. t 2 O(0) for premises tRt0of d1, and


  3. there is a positive premise containing only 0 terms anda new relation or p*
 *redicate

     symbol.

If T =T 0T1 is defined and stratifiable then T is an operational conservative e*
 *xtension

of T0.


Proof.  Let T = (; D) and D= D (Tp; Tr).  Let S : PF(T ) ! ffbe a stratification

for T and let S0 : PF(T 0) ! ff be the restriction of S to PF (T0) (note that S*
 * 0is a

stratification).

   Let u;w 2 C (0), R 2 Tr, P 2 Tp, and v 2 C().  We have to show that the

following two bi-implications hold

     TS `uRv    ()     T0S0` uRv;

     TS `P w    ()     T0S0` Pw:



                                      17





By definition 2.9 it suffices to prove the two bi-implications below for all i *
 *< ff.

     Ti` uRv    ()    T0i`uRv;                                              (1)

     Ti` Pw     ()    T0i`P w:                                              (2)

We will do this by transfinite induction on i. So let both statements be true f*
 *or all i0<i,

then we prove them for i.

   We begin to prove both implications from left to right. By definition 2.9 it*
 * suffices

to show for all j< d(T) that

     Ti;j`uRv   =)    T0i` uRv;                                             (3)

     Ti;j`Pw    =)    T0i` Pw:                                              (4)

We will do this by transfinite induction on j. So let 3 and 4 be true for all j*
 *0< j. We

prove them for j. By definition 2.9there is a rule d 2 D

     fPksk_:_k2_K_g_[_ftlRlt0l:_l2_Lg_[_f:Pmum_:_m_2_M_g_[_fvn:Rn:_n_2_Ng_

                                      C

with C = sRt and a closed substitution oe with oe(s) = u and oe(t) = v. We first

show that d 2 D0. Suppose that this is not the case. Since u 2 C(0) we must have

that s 2 O(0);Sso the additional requirements clearly hold for d.  Let var(s) =*
 * X

and Y  =  l2Lvar(t0l).  Sinced is pure we have that var(d) = X [ Y.  We know

that oe(x) 2 C(0) for all x 2 X. We show that for ally 2 Y we have oe(y) 2 C(0).

Suppose that there is a y02 Y with oe(y0) 2 C() n C(0) then oe(t0l0) 2 C() n C(*
 *0).

This contradicts the well-foundedness of the rule d, for Ui[ Ui;j`oe(tl0)Rl0oe(*
 *t0l0) so

by the induction hypotheses on i orj we find that oe(tl0) 2C () n C(0). Since t*
 *l0

is a 0 term, this must b ethe result of a substitution.  This can only be due t*
 *o a

variable y12 Y. By induction on the subsubscript we find an infinite backward c*
 *hain

of edges y0   y1   : :i:n the variable dependency graph of d.  So oe(y) 2 C(0)f*
 *or

all y 2Y . Let h be a positive premise containing only 0 terms and anew relatio*
 *n or

predicate symbol. By definition2.9 we have Ui[Ui;j` oe(h) so by induction on i *
 *or jwe

find that U0i[ U0i;j`oe (h),which is a contradiction since the oe(h) is not eve*
 *n a formula

in T0. So the assumption that d 2 D1cannot hold and we must have that d 2 D0. T*
 *his

means that d is pure and well-founded. Just as above we can show that oe(x) 2 C*
 *(0)for

all x 2 X[ Y so we have that allthe instantiated premises of d only contain 0te*
 *rms.

So we find by induction on i and/or j that for all positive premises h of rule *
 *d we

have U0i[ U0i;j` oe(h). Suppose that U0i6` oe(vn:Rn).Then there is a v0n2 C(0) *
 *such

that U0i` oe(vnRnv0n) so by induction oni we find that also Ui` oe(vnRnv0n), wh*
 *ich is a

contradiction. In this way we find that U0i`oe(h) for all negative premises h o*
 *f rule d.

By definition 2.9 we have T0i;j` uRv so Ti0` uRv.

   The case C = Ps is treated in the same way.  This ends our induction step on*
 * j,

which proves 3 and 4.So we find that equations 1 and 2 hold from left to right *
 *for i.

   Now we show that they hold from right to left for i. By definition 2.9 it su*
 *ffices to

show for all j< d(T0) that

     Ti0;j`uRv  =)    Ti`uRv;

     Ti0;j`Pw   =)    Ti`P w:



                                      18





This can be proved by inductionon j in the same way as we proved both implicati*
 *ons

from left to right,but simpler since we can apply induction immediately. This c*
 *oncludes

the proof.                                                                    2


Example 4.9   We are in a position to apply themain results discussed in this s*
 *ection

to our running examples.

   It is not hard to see that the term deduction systems of BPA and MRG satisfy*
 * the

conditions of Theorem 4.8. Thus, PA is an operational conservative extension of*
 * BPA.

Moreover, because of theorem 4.7, PA is an operational conservative extension u*
 *p to

simulation.

   Also the term deduction systems of BPAand DT satisfy the conditions of Theo-

rem 4.8; so, BPAdt is an operational conservative extension of BPA, andagain wi*
 *th

theorem 4.7 we find that BPAdt is an operational conservativeextension up to st*
 *rong

bisimulation of BPA.                                                          2



4.2    Algebraic conservativity


In this subsection we state and prove the main conservativity result for algebr*
 *aic sys-

tems. In particular, we prove that conservativity in inequational and equationa*
 *l spec-

ifications with transition system basedmo dels is a consequence of operational *
 *conser-

vativity. We will use ourrunning examples to show how our results work. For more

elaborate application of these results we refer to Section 6.


Definition 4.10  LetSi= (i; Ai; Pi) be algebraic systems (i = 0; 1).Let 0 1 be

defined. Then the sum S0 S1 of S0 and S1 is the algebraic system (0 1;A0 [

A1;P0 [P1).                                                                  2


Example 4.11   Consider the equational and inequational specifications of Examp*
 *le 3.4.

Notice that BPA   MRG    equals PA  and BPA  DT  equals BPAdt .            2


   Next, we define the notion of an algebraic conservative extension.  An algeb*
 *raic

system is a conservative extension of another one if exactly the same theorems *
 *regarding

only original terms can be derived fromb othof them.


Definition 4.12  LetSi = (i; Ai; Pi) be algebraic systems (i = 0; 1) and letS  =

(; A; P) = S0 S1b edefined. S is an (algebraic) conservative extension of S0if *
 *for

all s;t 2 C(0) and p 2 P0


     A ` p(s; t) () A0` p(s; t):


                                                                             2


   In this way,an inequational conservative extension is a conservative extensi*
 *on where

the involved algebraic systems are inequational specifications, and in particul*
 *ar, an

equational conservativeextension is a conservative extension where the algebrai*
 *c sys-

tems are equational specifications. Notice that in these cases P0 =P1.



                                      19





Definition 4.13  Let0 and 1 be two signatures such that 0 1 is defined. Let

A0b ea 0-algebra with carrier set A0. Let A be a (01)-algebra with carrier set A

such that A0 A. A is a model conservative extension of A0 if for every f 2 0 wi*
 *th

arity n, for all d1; : :;:dn 2 A0, fA(d1; : :;:dn) = fA0(d1; : :;:dn) where fA0*
 * and fA are

the interpretations of f in A0and A respectively.

   Moreover, let R0 and R be sets of binary relations on A0 and A respectively *
 *and

let g : R0! R. A=R is a model conservative extension of A0=R0 according to gif *
 *A is

a model conservative extensionof A0 and for all r02 R0, r0= g(r0) " (A0 A0).   2


   Now, we are in ap osition to state and prove the main result of this paper. *
 *It is the

algebraic conservative extension theorem.


Theorem 4.14    Let Si= (i; Ai; Pi) be algebraic systems, i = 0;1. Let S = (; A*
 *; P)

= S0S1be defined. Let A0be a complete axiomatisation of A0with respect to R0.Let

A be a sound axiomatisation of Awith respect to R. If A=R  is a model conservat*
 *ive

extension of A0=R0 according to g such that for al l p 2 P0, g (pA0) = pA , the*
 *n Sis an

algebraic conservativeextension of S0.


Proof.  The proof that for all s; t 2 C(0), A0 ` p(s; t)  =)  A ` p(s; t) is tr*
 *ivial.

Now, let s;t 2 C(0) and suppose A ` p(s;t). Since A is sound for A respect to R

A=R j= p(s;t). Because A=R is a model conservative extension of A0=R0 according*
 * to

g with g(pA0)= pA , A0=R0  j= p(s; t). Finally, A0` p(s;t) since A0 is complete*
 * for A0

with respect to R0. So A is an algebraicconservative extension of A0.          *
 *   2


   Notice that the requirements on gbecome trivial in inequational specificatio*
 *ns since

there is only one predicate to consider(namely, ). Thus, as a corollary we have*
 * the

following theorem with many useful applications (see Section 6).


Theorem 4.15    Let Si = (i; Ai; fg) be inequational specifications, i = 0;1.  *
 *Let

S = (; A; fg) = S0S1 be defined. Let Ti= (i;Di) be term deduction systems and

let T = (;D) = T0 T1 be defined. Let  be a preorder definable exclusively in te*
 *rms

of predicate and relation symbols. Let A0 be a complete axiomatisation with res*
 *pectto

the model induced by  in T0 and let A be a sound axiomatisation with respect to*
 * the

model induced by  in T . If T is an operational conservative extension up to  o*
 *f T0,

then S is an inequationalconservative extension of S0.


   We can deduce a general completeness theorem from Theorem 4.14.  Therefore,

we need the notion of elimination which roughly states that operators in an ext*
 *ended

algebraic system can be expressed in the original system.


Definition 4.16  LetS  = (; A; P) be an algebraic conservative extension of S0 =

(0; A0; P0). p 2 P is an elimination predicate if for all s 2 C ()nC (0) there *
 *is a

t 2 C(0) such that A ` p(s; t) and A` p(t; s), i.e., for every new term there i*
 *s a

"p-symmetric" old term.

   S has the eliminationproperty if all predicates in P0are elimination predica*
 *tes.  2



                                      20





   Notice that this definition of elimination subsumesthe definition of elimina*
 *tion on

equational specifications (see for instance [BV95 ]) and thedefinition of elimi*
 *nation on

inequational specifications [D'A95 ].


Theorem 4.17    Under the same hypotheses of Theorem 4.14, if in addition P = P*
 *0, all

predicates in Pare transitive, and Shas the elimination property,then A is a co*
 *mplete

axiomatisation of A with respect to R.


Proof.  Let s;t 2 C(0) such that A=R j= p(s;t). Since A=R  is a model conservat*
 *ive

extension of A0=R0 according to g with g(pA0) = pA, then A0=R0 j= p(s;t). So A0*
 * `

p(s; t) because A0is complete, which trivially implies A ` p(s; t).

   Suppose s;t 2 C ()nC (0) such that A=R  j= p(s;t). Because S has the elimina*
 *tion

property, there are s0;t02 C(0) such that A ` p(s;s0), A ` p(s0; s), A` p(t; t0*
 *), and

A ` p(t0; t).  Since A is sound, A=R  j= p(s; s0), A=R  j=  p(s0; s), A=R   j= *
 *p(t; t0),

and A=R  j= p(t0;t).  Because p is transitive and A is sound, pA  is transitive*
 *, then

A=R j= p(s0;t0). Now,since A=R  is a model conservative extension of A0=R0 acco*
 *rding

to g with g(pA0) = pA, then A0=R0  j= p(s0; t0). Because A0is complete, A0` p(s*
 *0;t0).

Since S is an algebraic conservative extension of S0, A ` p(s0;t0). Finally, be*
 *cause p is

transitive A` p(s; t).

   The proof of the cases of s and t belonging separately to C(0)and C ()nC(0)

follows the same lines of the previous case omitting the considerations of elim*
 *ination

when s or t belongs to C(0).                                                  2


   Assume that S is an inequational specification,we have that P = P0 = fgand

moreover  is transitive. Thus, as an immediate corollary of the previous theore*
 *mwe

have the following important subcase. See Section 6 for many applications.


Theorem 4.18    Under the same hypotheses of Theorem 4.15,if in addition S has *
 *the

elimination property,A is a complete axiomatisation with respect to the model i*
 *nduced

by the preorder in T .


   Recall that an equational specification is an inequational specification wit*
 *h an ad-

ditional conditional axiom (see Definition 3.3). We obtain as a trivial corolla*
 *ry that if

S, S0 and S1 are equational specifications and  is an equivalence,under the sam*
 *e con-

ditions of Theorem 4.15,S is an equational conservative extension of S0. If mor*
 *eover S

has the elimination property, A is a complete axiomatisation with respect to th*
 *e mo del

induced by  in T.


Example 4.19   We demonstrate our results with the running example (see Section*
 * 6

for more information).

   Lemma 3.8 states that BPA   is complete withrespect to ae+and PA  is sound w*
 *ith

respect to ae+. Since, in addition, PA is an operational conservative extension*
 * up toae+

of BPA, PA   isan inequational conservative extension of BPA  .  Moreover, beca*
 *use

PA   has the elimination property (see [BW90  ]), it is a complete axiomatisati*
 *on with

respect to ae+of PA.



                                      21





   Analogously,since BPA is a complete axiomatisation with respect to $__and BP*
 *Adt

is sound with respect to $__, and moreover, the term deduction system of BPAdt *
 *is an

operational conservative extension of the term deduction system of BPA up to $_*
 *_we

may conclude that BPAdt is an equational conservative extension of BPA.        *
 *  2



5    Ground and confluence modulo equations


In this section we will use our mainresults to prove a theorem in term rewritin*
 *g analysis.

Therefore,we restrict ourselves to equational specifications in this section.We*
 * will prove

a general reduction theorem stating thatin many cases checking the Church-Rosser

property for closed terms modulo some equations for a large system reduces to v*
 *erifying

this property for a small basic system.Of course, provided that the large syste*
 *m is an

equational conservative extension of the small system. From a term rewriting po*
 *int of

view this condition is not realistic since usually the Church-Rosser property f*
 *or closed

terms is necessary to obtain conservativity.

   In the previous section, we showed that, under certain conditions, it is pos*
 *sible

to prove conservativity without a term rewriting analysis. Thus, we could argue*
 * that

conservativity and ground confluence are equally powerful properties, so to spe*
 *ak.


Definition 5.1 A term rewriting system is a pair (; R) with  a signature and Ra

set of rewrite rules. Rewrite rules are pairs of terms (over ) that we denote s*
 * ! t.

We suppose that s is not a variable and that var(t)  var(s). The one step rewri*
 *te

relation !1Ris the smallestrelation on terms containing R that is closed under *
 *substi-

tutions and contexts. The rewrite relation !R is the transitive-reflexive closu*
 *re of the

one step rewrite relation !1R. Often,we refer to a term rewriting system (;R) b*
 *y its

set of (rewrite) rules R.                                                      *
 *  2


Definition 5.2 Let R be a set of rewrite rules and E be a set of equations.  Le*
 *t =E

be the smallest congruence generated bythe equations in E.  The one step rewrit*
 *ing

relation !1R=E is defined as =E ffi !1Rffi =E . The rewriting relation !R=E  is*
 * the

transitive-reflexive closure ofthe one step rewrite relation !1R=E. (Recall tha*
 *t for two

relations R and Swe have R ffiS = f(r;s) j 9t : (r; t) 2 R; (t; s) 2S g.)      *
 *       2


Definition 5.3 Let R be a set of rules and let E be a setof equations. Let ! be*
 * the

rewriting relation !R=E. Let s be a term. If for all s0; s1 such that s ! s0and*
 * s ! s1

there is a term s0such that s0! s0and s1! s0we say that the rewriting relation *
 *!R=E

is Church-Rosser or confluent.  We call !R=E ground Church-Rosser if it is Chur*
 *ch-

Rosser for closed terms. Sometimes, we will write CR  instead of Church-Rosser.*
 * We

also say that !R is Church-Rosser (or confluent) modulo E; we write CR =E. In t*
 *he

literature we also see E-Church-Rosser and E -confluence if !R=E is confluent i*
 *n the

above sense; see, for instance, Jouannaud and Mu"noz [JM84 ].                  *
 *   2


Definition 5.4 Let R be a set of rules and let E be a set of equations. Let = b*
 *e the

least congruence generated by the equations in E and the rules in R in both way*
 *s. We



                                      22





say that the rewriting relation !R=Eis ground CR = if for all groundterms s and*
 * t such

that s = t there are terms s0and t0such that s !R=E s0, t !R=Et0, and s0=E t0. *
 *   2



Remark 5.5   It is not hard to see that !R is ground CR =E if and only if it is

ground CR ==E.                                                               2



Definition 5.6 A term rewriting system Ris (strongly) terminating if there exis*
 *ts no

infinite sequence s0 !1Rs1 !1Rs2: :.:We call a term s a normal form if we do not

have s!1Rs0for any s0.                                                       2



Theorem 5.7   Let Si= (i; Ai; f=g) be equational specifications.Let S = (; A; f*
 *=g)

= S0 S1 bedefined.  Suppose that S  is an equational conservative extension of *
 *S0.

Turn a set R=0 A0 into a setof rewrite rules R0 and let E = A0n R=0be a set of

equations (or axioms). Turn the set R= = (A n E) [ R=0into a set of rewrite rul*
 *es R.

Suppose that !R is terminating and that normal forms are 0 terms (so S has the

elimination property). If !R0=E is ground Church-Rosser then !R=E is also ground

Church-Rosser.



Proof.  Let s and t be ground  terms and suppose that A` s = t.  By assumption,

there are ground 0 terms s0 and t0 with s !R  s0 and t !R t0.  So A ` s0 = t0.

Since S is a conservative extension of S0 we now have that A0 ` s0= t0. Since !*
 *R0=E

is ground CR there are s0 and t0 such that s0!R0=E s0,t0!R0=E t0, and E` s0 = t*
 *0.

Since R0 R we also have s0 !R=Es0. Since s !R s0we also haves !R=E s0(simply

put s =E s; ::;:s0=E s0between the one step rewritings). So we find that s!R=E *
 *s0.

In the same way we find that t !R=E t0,and we have E ` s0= t0. This implies usi*
 *ng

remark 5.5 that !R=E is ground CR.                                            2



   In section 6 we will apply the just derived results.



6    Applications


In this section we will give the reader an idea of the applicability of our con*
 *servativity

results, the completeness corollary and the ground Church-Rosser reduction theo*
 *rem.

Noteworthy perhaps,is that we could not find any conservativity result in the l*
 *iterature

for which our method does not work, as well.

   Within the ACP community there is a long tradition with conservativity resul*
 *ts,

completeness results and confluence results. Also in ATP there are many conserv*
 *ativity

and completeness results. We will simultaneously treat numerous examples from A*
 *CP,

ATP, and CCS. We will treat some typical cases more elaborately. We note that t*
 *he

examples in Figures 1, 2, 3, and 4 contain both known results and new results.



                                      23





6.1    Applications in equational specifications


In the introduction we mentioned the problems concerning the confluence of ACP *
 *that

Bergstra and Klop [BK84 ] used to prove conservativity.  We claimed that with o*
 *ur

theorems it is very easy to see thatthe conservativity result holds.  Therefore*
 *, we

elaborately treat the ffl-labelled arrow fromACP to BPA ffiin Figure 1. We show*
 * that

all our general results apply to this arrow.

   Van Glabbeek [Gla87] gives an operational semantics for Bergstra and Klop's *
 *ACP

[BK84  ] and for their sequential subsystem BPA ffi[BK84  ]. With our operation*
 *al result 4.8

it is easily seen that the large semantics is an operational conservative exten*
 *sion of the

small one. Baeten and Weijland [BW90 ], for instance, show that BPA ffiis sound*
 * and

complete with respect to the small semantics and that ACP is sound with respect*
 * to

the large one. They use a variant of strong bisimulation with successful termin*
 *ation

predicates, which is definable in terms of transition relations and predicates *
 *only. So,

our equational result 4.15 immediately implies that ACP is an equational conser*
 *vative

extension of BPA ffi.Since ACP has the elimination property we also find the co*
 *mplete-

ness of ACP with Theorem 4.18. Moreover,with our reduction Theorem 5.7 we have

that the question whether or not ACPis ground Church-Rosser modulo associativity

and commutativity of the choice (CR/AC) reduces to this question for BPA ffi. T*
 *he as-

sociated term rewriting system of BPA fficonsists of five rewrite rules and two*
 * equations,

which is a considerable reduction since the term rewriting system for ACP has m*
 *any

more rules.



                                     BPA ffi     PAffi
                                 ffl


                          ACP        BPA         PA



                          ACP x      BPA y       PAy



                                     BPA ffix   PA ffix


                         Figure 1: Applications in ACP



   Now, we discuss Figure 1. An arrow A ____-B indicates that system A is both *
 *an

operational and an equational conservative extension of system B and that this *
 *can be

shown using our conservativity results. The x and y stand for variables; we use*
 * them

to treat many examples at the same time.

   Let x = y. And let x be one of PR, RN, , , , or a combination of them. The

abbreviations stand for projections, renamings, simple state operators, extende*
 *d state

operators, and the priority operator respectively. A concise reference to these*
 * notions,

their operational rules, their axiomatisations, and their associated term rewri*
 *ting sys-

tems is the text book of Baeten and Weijland [BW90  ] or the survey [BV95 ].  T*
 *he



                                      24





variant of bisimulation that is used in these applications is definable in term*
 *s of transi-

tion relations and predicates exclusively. So, for all these cases we have that*
 * all arrows

of Figure 1: operational and equational conservativity. Moreover, all these ext*
 *ensions

have the elimination property for either the complete BPA or the complete BPA f*
 *fi(if

the extension contains already a ffi);for full proofs see, for instance, [BW90 *
 *] or [BV95 ].

So we find for all these extensionsthe completeness with Theorem 4.18.  Moreove*
 *r,

the ground confluence modulo AC for these systems reduces to the ground conflue*
 *nce

modulo AC for either BPA orBPA ffi.

   Now, let x = yand let x be one of rec, dt, or a combination of those (note t*
 *hat we

can also combine rec with the already treated notions).  The abbreviations stan*
 *d for

recursion and discrete time [BB92 ],respectively. Also for these systems we hav*
 *e that all

arrows hold. Note that BPAdt ____-BPA was one of the running examples. We do not

have the elimination property for subscripted systems to systems without a subs*
 *cript

(for instance oed(a) cannot be written as a BPA term). For the other arrows we *
 *have

the elimination property [BB92 ], so fromthe completeness of BPA y we conclude *
 *the

completeness for all the extensions.The ground confluence of these systems has *
 *not yet

been studied but with our reduction theorem it is only necessary to study the g*
 *round

confluence for the BPA ysystems.

   Now, let x = yand let x be Milner's silent action |. We already mentioned in*
 * the

introduction that systems containingthe three | laws of Milner have in general *
 *bad

rewriting properties. The conservativity of ACP | over ACP was proved semantica*
 *lly

by Bergstra and Klop [BK85 ] since the second and third | law have no clear term

rewriting direction. Next, we will show that our approach also works in cases w*
 *here

the established method breaks down. In fact, we immediately find this result. T*
 *he

operational semantics of ACP | is just the one of ACP but now a ranges also ove*
 *r |

itself. It is easy to see that the conditions of Theorem 4.8 are satisfied,so A*
 *CP  | is

an operational conservative extension of ACP. Now with Theorem 4.7 we find that

ACP | is an operational conservative extension up to rooted | bisimulation equi*
 *valence

of ACP. Since ACP is sound andcomplete and since ACP  |is sound with respect to

this equivalence,we find with Theorem 4.15 that ACP | is an equational conserva*
 *tive

extension of ACP. All the other arrows in Figure 1 go likewise. Since all the e*
 *xtensions

have the elimination property for BPA ffi;|, we find their completenesswith the*
 * aid of the

completeness of BPA ffi;|. Thesystems have bad term rewriting properties so the*
 * ground

confluence results does not apply.

   We mentioned in the introductionthe rather complicated term rewriting analys*
 *is

of Akkerman and Baeten [AB90 ] of a fragment ofACP with the branching |.  We

will show in a moment that ourresults can be easily applied to this case. With *
 *the

aid of Theorem 4.7 we find that ACP |is an operational conservative extension u*
 *p to

branching bisimulation equivalence [GW89  ] of ACP. Also in this case we find i*
 *n the

same way as above that ACP with the branching | axioms [GW89  ], denoted ACP  |*
 *, is

an equational conservativeextension of ACP. The same holds for all the other ar*
 *rows

in Figure 1. Since all the extensions have the elimination property for BPA |we*
 * find the

completeness for them with the completeness of BPA |. The branching | axioms ha*
 *ve



                                      25





better term rewriting properties [AB90 ] than the | laws of Milner (that we dis*
 *cussed

above). So our ground confluence result may be useful, as well.

   Let x = y be the empty process " of Koymans and Vrancken [KV85 ];  see also

Vrancken [Vra91]. We can show operational and equational conservativity for all*
 * arrows

from a system with an " to a subsystem also featuring this " by using the opera*
 *tional

semantics that can be found in Baeten and Weijland's text book [BW90  ]. In [BW*
 *90  ]

we also find that these systems have the elimination property, soalso our compl*
 *eteness

and the ground confluence results apply.  For the remaining arrows we have to f*
 *ollow

a different approach. The operational semantics in [BW90 ] features the rule a *
 * a! "

so we can never have that this semantics is an operational conservative extensi*
 *on of

a semantics without " (but containing a).  For, there is no " in the subsystem.*
 *  The

solution to this problem is to takeanother operational semantics that is easily*
 * obtained

by "upgrading" the complete graph modelof Koymans and Vrancken [KV85 ]. In fact,

this operational semantics is that of the subsystempwhere we include " as a nor*
 *mal

atomic action. So we have,for instance, "  "!  . The special behaviour of the e*
 *mpty

process is expressed with the aid of so-called " bisimulation equivalence of Ko*
 *ymans

and Vrancken [KV85 ]. Also this definition needs a straightforward upgrade from*
 * graphs

to transitions (and is definable in terms of transition relations and predicate*
 *s only).

In this way we find the operational and equational conservativity. Since we can*
 *not

eliminate the empty process,we cannot apply our completeness theorem and the gr*
 *ound

confluence result for these particular systems.

   Let x be ae standing for absolute real time [BB91 ]. Then the x-arrow inthe *
 *figure

holds.  To obtain this result we take the operational semantics of Klusener [Kl*
 *u91 ].

Also here we have the elimination property, so our completenessand ground confl*
 *uence

results apply, too.



                               ATP         ATP u       ATP  v



                   ASP         ASTP       ASTP  u      ASTP v


                         Figure 2: Applications in ATP



   Now we treat results on ATPwhich are depicted in Figure 2. The acronym ASP

stands for the algebra of sequentialprocesses. This system stems from Milner [M*
 *il84].

Nicollin and Sifakis [NS91 ] studied a timed process algebra called ATP with va*
 *rious

extensions and restrictions of whichthe most restricted timed one is ASTP, the *
 *algebra

of sequential timed processes.Milner's [Mil84 ] algebra of sequential processes*
 * ASP_the

untimed version of ASTP_is themost restricted system. The interesting thing her*
 *e is

that they prove some conservativity results with the same strategy as ours: the*
 *y show

that the extensions are operationally conservative up to bisimulation by lookin*
 *g at the

transition rules and then conclude the equational conservativity. Our figure in*
 *tends

to show that every possible extension that can be obtained with the so-called d*
 *elay



                                      26





operators of Nicollin and Sifakis [NS91] is conservative. There are four delay *
 *operators

present in [NS91 ]:start delay, unbounded start delay, execution delay, and ter*
 *mination

delay. The termination delay (td) is an enhancement of the execution delay (ed)*
 * so if

we have the termination delay we also have execution delay. For u we can take a*
 *ny

combination of delay operators.If u does not contain all delay operators yet we*
 * can take

for v the operators ofu and a new one, or if the execution delay operator is in*
 * u we can

take the termination delay operatorin v and we do not necessarily need an extra*
 * delay

operator for a non-trivial extension. Cases like ASP  ____-ASTP   and ASTP  td *
 *____-

ASTP  edare, in our opinion, the most interesting since in these cases not only*
 * a new

operator (unit delay and a special constant respectively) is introduced but als*
 *o an

original operator gets a new rule.  Since the elimination property holds [NS91 *
 *] for

ASTP our completeness corollary appliesfor all the arrows but the two to ASP. T*
 *he

ground confluence of ATP isnot yet studied but its study reduces to that of ASTP

with our reduction theorem.



6.2    Applications in inequational specifications



                                       ?
                            BPA ffiaa      ACP  aa



                            BPA ffiaa      ACP aa


                        Figure 3:Applications in ACP aa



Voorhoeve and Basten introducedin [VB96  ] a preorder for unstable nondetermini*
 *sm.

They deal with a set of autonomousactions which can be regarded as observable a*
 *c-

tions that somehow behave as the silent step.  Several algebras were defined th*
 *ere.

BPA ffiaa  is the basic process algebra with deadlock and autonomous actions.  *
 *They

use our results to extend BPA ffiaa  with the parallel operator, obtaining thus*
 * ACP aa  .

Moreover, sinceACP  aa  has the elimination property, completeness is proved us*
 *ing our

results. In addition,they added the binary Kleene star [BBP94 ] to both theorie*
 *s. Since

BPA ffiaa  and ACP  aa  are sound, and the respective term deductionsystems sat*
 *isfy

the conditions of Theorem 4.8,operational and inequational conservative extensi*
 *oncan

be also shown using our results. Figure 3 shows this overview. Perhaps, the rea*
 *der

expected the arrow ACP  aa  ____-BPAffiaa . In this case only operational conse*
 *rvative

extension can be proved using results in this articles (and so operational cons*
 *ervative

extension up to the preorder). Since BPA ffiaa  is not complete (see [Sew94, VB*
 *96 ]),

Theorem 4.15 cannot be used.

   The next application is based on Walker [Wal90 ]. He introduced in [Wal90] a*
 * com-

plete (but non finite) axiomatisation for a preorder that extends | bisimulatio*
 *n with

divergence. Also here,we can use our results to prove conservativity and comple*
 *teness.



                                      27





                                ST ?      CCS ?


                                new   new  new


                                 ST        CCS


                          Figure 4: Applications in CCS



   Below we will explain Figure 4. LetST be the algebra of synchronisation tree*
 *s with

Milner's | laws [Mil89]. The signature of ST has prefixing operators, the alter*
 *native

composition and the nilpro cess. Let CCS be the well-known calculus of Milner [*
 *Mil89]

that extends ST with renaming, restriction and parallel composition, and the ex*
 *pansion

laws. LetST ? and CCS ? the respective extensions of ST and CCS with the diverg*
 *ence

operator as given in [Wal90]. We note that for all CCS terms Walker's preorder *
 *agrees

with rooted | bisimulation [Wal90]. In addition, since ST is complete for the p*
 *reorder,

and the new operators can be eliminated, we can use our results to show that CCS

is complete.  Analogously, CCS  ? is complete since ST? is complete and CCS ?  *
 *has

the elimination property. Nevertheless, nor ST? neither CCS ?  have the elimina*
 *tion

property with respect to ST or CCS. Moreover, it deserves to notice that the ne*
 *w-

labelled arrows in Figure 4 are new results here.



7    Concluding remarks


In this paper we presented general conservativity results for transition system*
 * based

process theories with reasonable and easy-to-check conditions.  As a simple cor*
 *ollary

of the conservativity results we proved a completeness theorem. We proved a gen*
 *eral

theorem giving sufficient conditionsto reduce the question of ground confluence*
 * modulo

some equations for a large term rewriting system associated with a process theo*
 *ry to a

small term rewriting system under the condition that the large system is a cons*
 *ervative

extension of the small one. With numerous examples that we took from the litera*
 *ture

about CCS, ACP, and ATP we showed that our theorems are useful. The applications

include various real and discrete time settings in ACP, ATP, and CCS and the no*
 *tions

projection, renaming, state operator, priority, recursion, the silent step (bot*
 *h the weak

and branching variants), autonomous actions, the empty process, divergence, etc.

   Remarkably,we could not find any conservativity results inthe literature for*
 * which

our method cannot be applied. We want to stress that the established method for

proving conservativityin these theories usually makes use of a rather complicat*
 *ed term

rewriting analysis,whereas our method is very easily applicable. This is a grea*
 *t advan-

tage of our approach in our opinion.



Acknowledgements. This paper came into being by merging two earlier papers. One

by Verhoef [Ver94] and one by D'Argenio [D'A95]. Wan Fokkink suggested us to me*
 *rge



                                      28





those papers. We thank him for this idea and for his comments onthe penultimate

version of the ensuing amalgamation.We also thank Alban Ponse for being so help*
 *ful

on the last version of this article. Moreover, we like to thank Gertjan Akkerma*
 *n,Jos

Baeten, Twan Basten, Jean-Pierre Jouannaud, Pim Kars, Jan Willem Klop, Xavier

Nicollin, and the referees for their valuable comments on earlier versions of t*
 *his paper

and/or the other two.



References


[AB90]  G.J. Akkerman and J.C.M. Baeten.Term rewriting analysis in process alge*
 *bra.

        Report P9006, Programming Research Group, University of Amsterdam, 1990.


[Abr87] S. Abramsky. Observation equivalence as a testing equivalence.  Theoret*
 *ical

        Computer Science, 53:225-241, 1987.


[ABV92]  L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOSrules into equatio*
 *ns.

        In Proceedings 7th Annual Symposium on Logic in Computer Science,Santa

        Cruz, California, pages 113-124. IEEE Computer Society Press, 1992.


[Ace91] L. Aceto.   On relating concurrency and nondeterminism.   In S. Brookes,

        M. Main, A. Melton, M. Mislove, andD. Schmidt, editors, Proceedings Mat*
 *h-

        ematical Foundations ofProgramming Semantics (MFPS 7), volume 598 of

        Lecture Notes in Computer Science, pages 376-402, Pittsburgh, 1991. Spr*
 *inger-

        Verlag.


[BB91]  J.C.M. Baeten and J.A. Bergstra. Real time pro cess algebra. Journal of*
 * Formal

        Aspects of Computing Science, 3(2):142-188, 1991.


[BB92]  J.C.M. Baeten and J.A. Bergstra.  Discrete time process algebra.  In W.*
 *R.

        Cleaveland, editor, Proceedings CONCUR92, Stony Brook,NY, USA, volume

        630 of Lecture Notes in Computer Science, pages 401-420. Springer-Verla*
 *g,

        1992.


[BB93]  J.C.M. Baeten and J.A. Bergstra. Non interleaving process algebra. In B*
 *est

        [Bes93], pages 308-323.


[BBP94]  J.A. Bergstra,I. Bethke, and A. Ponse. Process algebra with iteration *
 *and

        nesting. The Computer Journal, 37(4):243-258, 1994.


[BC88]  G. Boudol and I. Castellani. Concurrency andatomicity. TheoreticalCompu*
 *ter

        Science, 59(1/2):25-84, 1988.


[Bes93] E. Best, editor. Proceedings CONCUR93, Hildesheim, Germany, volume715

        of Lecture Notes in Computer Science. Springer-Verlag, 1993.



                                      29





[BG91]  R.N. Bol and J.F. Groote. The meaning of negative premises in transition

        system specifications (extended abstract).In J. Leach Albert, B. Monien*
 *, and

        M. Rodriguez, editors, Proceedings 18thICALP, Madrid, volume 510 of Lec*
 *ture

        Notes in Computer Science, pages 481-494. Springer-Verlag, 1991. Full v*
 *ersion

        appeared as Report CS-R9054, CWI, Amsterdam, 1990. To appear in Journal

        of the ACM.


[BIM88] B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced: Pre*
 *limi-

        nary report. In Conference Record of the 15thACM Symposium on Principles

        of Programming Languages, San Diego, California, pages 229-239, 1988.


[BIM95] B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced. Jou*
 *rnal

        of the ACM, 42(1):232-268, January1995.


[BK84]  J.A. Bergstra and J.W. Klop.Process algebra for synchronous communicati*
 *on.

        Information and Computation, 60(1/3):109-137, 1984.


[BK85]  J.A. Bergstra and J.W. Klop. Algebra of communicating processes with ab-

        straction. Theoretical Computer Science, 37(1):77-121, 1985.


[BK90]  J.C.M. Baeten and J.W. Klop,editors. Proceedings CONCUR90, Amsterdam,

        volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.


[Bos94] D.J.B. Bosscher.  Term rewriting properties of SOS axiomatisations.  Re*
 *port

        CS-R9405, CWI, Amsterdam, January 1994.


[BV95]  J.C.M. Baeten and C. Verhoef. Concrete process algebra. In S. Abramsky,

        D. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer

        Science, Vol 4. OxfordUniversity Press, 1995.


[BW90]  J.C.M. Baeten and W.P. Weijland.  Process Algebra.  Cambridge Tracts in

        Theoretical Computer Science 18. Cambridge University Press, 1990.


[Cas93] I. Castellani.  Observing distribution in pro cesses.  In Proceedings M*
 *FCS'93,

        volume 711 of Lecture Notes in Computer Science. Springer-Verlag, 1993.


[D'A95] P.R. D'Argenio. Ageneral conservative extension theorem in pro cess alg*
 *ebras

        with inequalities. In Ponse et al.[PVV95  ], pages 67-79.


[FV95]  W.J. Fokkink and C. Verhoef. A conservative look at termdeduction syste*
 *ms

        with variable binding. Report 95/28,Department of Mathematics and Com-

        puting Science, Eindhoven University of Technology, October 1995.  Also*
 * as

        Logic Group Preprint Series 140,Department of Philosophy, Utrecht Unive*
 *r-

        sity, September 1995.


[FZ94]  W.J. Fokkink and H. Zantema.  Basic process algebra with iteration: Com-

        pleteness of its equational axioms.  The Computer Journal, 37(4):259-26*
 *7,

        1994.



                                      30





[Gil76] A. Gill. Applied Algebra for the Computer Sciences.  Prentice-Hall Inte*
 *rna-

        tional, New Jersey - USA, 1976.


[Gla87] R.J. van Glabbeek. Bounded nondeterminism and the approximation induc-

        tion principle in process algebra. In F.J. Brandenburg, G. Vidal-Naquet*
 *, and

        M. Wirsing, editors, Proceedings STACS 87,volume 247 of Lecture Notes in

        Computer Science, pages 336-347. Springer-Verlag, 1987.


[Gla90] R.J. van Glabbeek. The linear time - branching time spectrum. In Baeten

        and Klop [BK90 ], pages 278-297.


[Gla93] R.J. van Glabbeek. The linear time - branching time spectrum II (the se*
 *man-

        tics of sequential systems with silent moves). In Best [Bes93], pages 6*
 *6-81.


[Gla95] R.J. van Glabbeek. The meaning of negative premises in transition system

        specifications II.  Report STAN-CS-TN-95-17,  Dept. ofComputer Science,

        Stanford University,1995. To appear in Information and Computation.


[Gro93] J.F. Groote. Transition system specifications with negativepremises.  T*
 *heo-

        retical Computer Science, 118(2):263-299, 1993.


[GV92]  J.F. Groote and F.W. Vaandrager.  Structuredop erational semantics and

        bisimulation as a congruence. Information and Computation, 100(2):202-2*
 *60,

        October 1992.


[GW89]  R.J. van Glabbeek and W.P. Weijland.  Branching time and abstraction in

        bisimulation semantics (extended abstract).  In G.X. Ritter, editor, In*
 *forma-

        tion Processing 89, pages 613-618. North-Holland, 1989. Full version av*
 *ailable

        as Report CS-R9120, CWI, Amsterdam, 1991.


[Hen88] M. Hennessy. Algebraic Theory of Processes.  MIT Press, Cambridge, Mas-

        sachusetts,1988.


[JM84]  J.-P. Jouannaud and M. Mu"noz. Termination of a set of rules modulo a s*
 *et of

        equations. In R.E. Shostak, editor, 7th International Conference on Aut*
 *omated

        Deduction, volume 170 of Lecture Notes in Computer Science, pages 175-1*
 *93.

        Springer-Verlag,1984.


[Klu91] A.S. Klusener. Completeness in real time processalgebra. In J.C.M. Baet*
 *en

        and J.F. Groote, editors, Proceedings CONCUR 91,Amsterdam, volume 527

        of Lecture Notes in Computer Science, pages 376-392. Springer-Verlag, 1*
 *991.


[Klu93] A.S. Klusener.Models and axioms for a fragment of realtime process alge*
 *bra.

        PhD thesis, Departmentof Mathematics and Computing Science, Eindhoven

        University of Technology, December 1993.



                                      31





[KV85]  C.P.J. Koymans and J.L.M.Vrancken.  Extending processalgebra with the

        empty process ffl. Logic Group Preprint Series Nr. 1, CIF, State Univer*
 *sity of

        Utrecht, 1985.


[Mil84] R. Milner.  A complete inference system for a class of regular behaviou*
 *rs.

        Journal of Computer and System Sciences, 28:439-466, 1984.


[Mil89] R. Milner.  Communication and Concurrency.  Prentice-Hall International,

        Englewood Cliffs, 1989.


[MT90]  F. Moller and C. Tofts.  Atemporal calculus of communicating systems.  *
 *In

        Baeten and Klop [BK90 ], pages 401-415.


[NS91]  X. Nicollin and J. Sifakis. The algebra of timed processes ATP: Theory *
 *and

        application (revised version).Technical Report RT-C26,LGI-IMAG, Grenobl*
 *e,

        France, November 1991.


[NT84]  M. Nielsen and P.S. Thiagarajan. Degrees of non-determinism and concur-

        rency: a Petri net view.In M. Joseph and R. Shyamasundar, editors, Proc*
 *eed-

        ings 5thConference on Foundations of SoftwareTechnology and Theoretical

        Computer Science,India, volume 181 of LectureNotes in Computer Science,

        pages 89-118. Springer-Verlag,1984.


[Par81] D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deus*
 *sen,

        editor, 5thGI Conference, volume 104 of Lecture Notes in Computer Scien*
 *ce,

        pages 167-183. Springer-Verlag, 1981.


[Plo81] G.D. Plotkin. Astructural approach to operational semantics. Rep ort DA*
 *IMI

        FN-19, Computer Science Department, Aarhus University, 1981.


[PVV95]  A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors.Proceedings of t*
 *he 2nd.

        WorkshopACP'95, Report 95/14. Department of Mathematics and Computing

        Science, Eindhoven University of Technology, 1995.


[Sew94] P. Sewell. Bisimulation is not (first order) equationally axiomatisable*
 *. InPro-

        ceedings 9thAnnual Symposium on Logic in Computer Science, Paris, Franc*
 *e,

        pages 62-70. IEEE Computer Society Press, 1994.


[VB96]  M. Voorhoeve and T. Basten. Process algebrawith autonomous actions. Re-

        port 96/01, Department of Mathematics and Computing Science, Eindhoven

        University of Technology, 1996.A preliminary version appeared in Ponse *
 *etal.

        [PVV95  ].


[Ver94] C. Verhoef. A general conservative extension theorem in process algebra*
 *. In

        E.-R. Olderog, editor, Proceedings IFIPConference of Programming Concep*
 *ts,

        Methods and Calculi, SanMiniato, Italy, volume A-56 of IFIP Transaction*
 *s,

        pages 149-168. Elsevier Science Publishers,1994.



                                      32





[Ver95] C. Verhoef. A congruencetheorem for structured operational semantics wi*
 *th

        predicates and negative premises. Nordic Journal of Computing,2:274-302,

        1995.


[Vra91] J.L.M. Vrancken. Studies in process algebra, algebraic specifications a*
 *nd par-

        allelism. PhD thesis, University of Amsterdam, 1991.


[Wal90] D.J. Walker. Bisimulation and divergence.  Information and Computation,

        85(2):202-241, 1990.


[Wec92] W. Wechler.  Universal Algebra for Computer Scientists.  Springer-Verla*
 *g,

        Berlin, Germany, 1992.


[Yan93] D. Yankelevich. Parametric views of process description languages.PhD t*
 *hesis,

        University of Pisa, 1993.


[Yi90]  W. Yi.  Real-time behaviourof asynchronous agents.  In Baeten and Klop

        [BK90 ], pages 502-520.


[Zan95] H. Zantema. Termination of term rewriting by semantic labelling.Fundame*
 *nta

        Informaticae, 24:89-105, 1995.



                                      33