A congruence theorem for structured operational semantics with predicates J.C.M. Baeten and C. Verhoef Department of Mathematicsand Computing Science Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands e-mail:chrisv@win.tue.nl, josb@win.tue.nl Abstract. We proposed a syntactical format, the path format,for structu* *red operationalsemantics in which predicates may occur. We proved that stro* *ng bisim- ulationis a congruence for all the operators that can be defined within* * the path for- mat.To show that this format is useful we provided many examples that w* *e took from theliterature about CCS, CSP, and ACP;they do satisfy the path for* *mat but no formats proposed by others. The examples include concepts like termi* *nation, convergence, divergence, weak bisimulation, azero ob ject, side conditi* *ons, func- tions, real time, discrete time, sequencing, negative premises, negativ* *e conclusions, and priorities (or a combination of these notions). Key Words & Phrases: structured operational semantics, term deduction s* *ystem, transition system sp ecification, structured state system, labelled transition sys* *tem, strong bisimulation, congruence theorem, predicate. 1980 Mathematics Subject Classification (1985 Revision): 68Q05, 68Q55. CR Categories: D.3.1, F.1.1, F.3.2, F.4.3. Note:Partial support received from the European Communities under CONCU* *R 2,BRA 7166. 1. Introduction Since the paper of Plotkin [23] about structuralop erational semantics it has b* *ecome quite popular to provide a semantics for pro cess calculi, programming, and specifica* *tion languages by using a labelled transition system. Since then a number of papers about the * *sub ject of structured operational semantics appeared andit gradually became a subject of r* *esearch of its own. Various so-called formats were proposed for labelled transition systems in* * Plotkin's style. Such a format is a syntactical constraint on the form of the rules such that so* *me nice property holds, for instance, that bisimulation equivalence is a congruence for all the * *operators that can be defined within the format. ntyft/ntyxt path GSOS tyft/tyxt positiveGSOS De Simone format Figure 1.The lattice of formats In figure 1 we depict the various formats together with a new one;the dashe* *d arrow points to it. An arrow from one format to another indicatesthat all operators that can* * be defined in the first format can also be defined in the second one. The most basic forma* *t is a modest reformulation of a format proposed by De Simone [25]. Yet it is already powerfu* *l enough to define all the usual operators of,for instance, CCS or ACP. The GSOS format ofB* *lo om, Istrail and Meyer [11]allows negative premises but no lookahead and the tyft/tyxt forma* *t of Groote and Vaandrager [16] allows lookahead but no negative premises. They both genera* *lize the format of De Simone. The positive GSOS format in the figure is the greatest com* *mon divisor (so to speak) of the GSOSand the tyft/tyxt format. The ntyft/ntyxt format of Gr* *oote [15]is the least common multiple (using thesame informal phrasing) of the tyft/tyxt fo* *rmat and the GSOS format. In this paper we will extend the tyft/tyxt format with predicates.* * We propose the path format,which stands for predicates and tyft/tyxt hybrid format. We will no* *t give the exact definitions of all these formats exceptthe definitions of the path format and t* *he tyft/tyxt format. The main result of this paper is a congruence theorem stating that if a so-* *called term deduction system satisfies the path format (and is well-founded) then strong bi* *simulation is a congruence. We prove this using the congruence theorem of Groote and Vaandrag* *er [16] (which is the case without predicates) by coding each predicate as a binary rel* *ation. So all the operators that can be defined in the pathformat can also be defined in the tyft* */tyxt format. Now the question arises why we need the path format anyway. Next, we will motiv* *ate the need for this new format. Aformat is, in general, a purely syntactical constraint on the form of the * *deduction rules, so the path format syntactically generalizes the tyft/tyxt format since we may * *mix predicates and ordinary transitions (in fact, our format uses relations instead of transit* *ions), whereas we cannot use predicates in the tyft/tyxt format. Another argumentthat advocates the path format is that usually an operation* *al semantics in Plotkin's style that containspredicates can be easily understood, but if we * *have to code each predicate as a binary relationto obtain an operational semantics in tyft/t* *yxt format we immediately lose the simplicity of the operational semantics. Even if we donot care about syntactical freedom or simplicity at all we sti* *ll have to be careful with coding of predicates by relations since this can lead to non-intui* *tive situations. Next, we will give some examples of operational semantics that are better under* *stood with than without predicates. Two examples canb e found in a paper of Baeten and Vaandrager [7] in which * *several operational semantics are given forthe simple language Basic Process Algebra (B* *PA ); this consists of the first five lawsof the theory PA of Bergstra and Klop [10]. The * *language BPA has only atomic actions and alternative and sequential composition. First, Baeten and Vaandrager extend the signature with a constant ffi. Then* * they give an operational semantics with negative premises. Forcompleteness they need tha* *t ffix = x, which is different from the usual law in the ACP framework,namely ffix = ffi; * *the constant ffi stands for inaction or deadlock. In section 2 we will return to this operationa* *l semantics. An operational semantics using predicates that to us is more intuitively appealing* * is given by Van Glabbeek [14].Further on in this section we will use his semanticsto explain ou* *r format. When discussing another operational semantics of BPA ,Baeten and Vaandrager* * moreover add the constant " (see Koymansand Vrancken [19])to the algebraic description l* *anguage featuring the rule p "! ffi; p here is just an extra label. Our intuitionof the empty process is that it is * *only capable of immediatelypsuccessfully terminating, but this rule suggests that it can, in fa* *ct, perform an action and then terminate unsuccessfully. Baeten and Van Glabbeek [6]give an * *operational semantics with a termination predicate that is more in accordance with our intu* *ition about the empty process. We will returnto this issue in another context where we treat an* * operational semantics of Aceto and Hennessy [1]in which a termination predicate occurs; see* * section 2. As a last example ofsemantics that are better understood with than without * *predicates we will mention the clear operational semantics using predicates that Klusener * *[18] givesfor various real time process algebras.He also gives non-intuitive semantics with n* *egative premises for the same languages. Klusener introduces these negative premises to eliminat* *e the predicates (in order to obtain a congruence result). We claim that this is not necessary;s* *ee section 2 for more details. Next we will informally introduce the path format by giving the operational* * semantics of Van Glabbeek [14]of the languageBPA to demonstrate thecongruence theorem. In f* *act, we take a fragment of the structured operational semantics of Van Glabbeek [14]. I* *n BPA we have alternative and sequential composition (denoted by + and resp.) and a set* * A of atomic actions. Often we will write xyinstead of x y. In table 1 we have that x; x0* *; y, and y0are distinct variables and a rangesover the set A. We have ordinaryptransitions int* *hisptable and predicates. For each a 2A there is a postfix predicate !a . The intuitionof x* *! a is thatx can perform an a action and then terminate successfully. The intended meaning o* *f x!a x0is as expected: x evolves into x0by performing an a action. We have to check two p* *roperties of the transition system in order to be able touse our congruence theorem. We will* * informally introduce them and show that they hold for the system in table 1. The first demand is that every rule must be well-founded. Well-foundedness * *roughly says that there are no transitions in the premises with cyclic occurrences of variab* *les; for instance, the rules x!a_x_ y!a_z;z!_b_y ; (1) C C are not well-founded. Itis easy to check that the rules in table 1 are well-fou* *nded. __________________________________________________p p _x!a_x0_ x!_a___ a!a xy!a x0y xy!a y p p __x!a_x0__ _y!_ay_0__ _x!_a_____p __y!a_____p x_+_y!_a_x0___x_+_y!a_y0___x_+_y!a______x_+_y!a___ Table 1. A Transition system for BPA. The last demand is alittle bit more involved: the rules have to be in path * *format. We list the conditions. Check for each rule the following. All the transitions in the premises must* * end in distinct variables;denote this set by Y .If the conclusion is a transition then it must * *begin with either a variable x=2Y or a term f(x1; : :;:xn) with x1; : :;:xn distinct variables th* *at are not in Y .If the conclusion contains a predicatewe treat the term that occurs in it as if it* * were the beginning of an ordinary transition. Now it is easy toverify that the rules of table 1 are in path format but it* * will be even more easy if we also list the things thatwe do not have to worry about. There is no restriction on the number of premises. There is also no restric* *tion whatso ever on terms occurring in predicates in the premises. There is no restriction on a * *term that occurs in the left-hand side of a transition ina premise or in the right-hand side of * *a transition in a conclusion. As an example wetreat the last rule of table 1. For the premise of this rul* *e there is nothing to check. The beginning of the transition in the conclusion is of the form f(x;* *y ).So this rule is in path format and bisimulation is a congruence. In the remainder of this section we will discuss the organization of this p* *aper. We did not choose for a chronological orderingof our paper. In section 2 we start with the* * end: namely the applications. At first sight this may seem a bit unlogical but there are se* *veral reasons that advocate this ordering, in fact, wealready discussed an application in the intr* *oduction. The first reason for this choice is thatthe area of application is operational sema* *ntics and they are often easy to read. The second reason is that the informal definitions that we * *just gave for the well-foundedness and the path format will be enough to understand what is g* *oing on. The third and maybe most important reason for this choice is that the reader immedi* *ately can see if her or his operational semantics hasa go od chance to fit in our format. If * *this is the case then the time has come to read on and enter section 3. In this section we intro* *duce the basics and the notion of a term deduction system, which is a generalization of a trans* *ition system specification. In the next section we define a structured statesystem, which ge* *neralizes the concept of a labelled transition system and we define a notion of bisimulation * *equivalence in the presence of predicates.The connection between these two sections is that a * *term deduction system induces in a natural waya structured state system. Now we have all the p* *rerequisites to continue with section 5.In this section we will give the exact definitions o* *f well-foundedness and the path and tyft/tyxt formats. Thereafter, we willstate and prove the cong* *ruence theorem. The last section contains concludingremarks and discusses future work. 2. Applications In this section we will discuss a number of known operational semantics in whic* *h predicates occur so none of the examples satisfy formatsproposed by others. It will turn o* *ut that they are well-founded and satisfy the path format or that they can be easily modifie* *d to satisfying the path format. With the aid of our congruence theorem we then find that bisim* *ulation is a congruence for all the operators that are defined within the operational s* *emantics. We recall that the informal definitions ofwell-founded and the path format can be * *found in the introduction. The examples are taken from CCS , CSP, and ACP . They touch upon concepts l* *iketer- mination, convergence, divergence, weak bisimulation, a zero object, side condi* *tions, functions, real time, discrete time, sequencing, negative premises, negative conclusions, * *and priorities (or a combination of these notions). The first example concerns an operational semantics that originates from Ac* *eto and Hen- nessy[1]. It is an operational semantics of a CCS like process algebra extended* * with a successful termination predicate and apconvergence predicate. Their approach is to first i* *nductively define the termination predicate ,which is a postfix denoted predicate. In table 2 we* *enumerate the rules as they essentially appear in [1]. Infact, Baeten and Van Glabbeek [6] h* *ave the same approach to successful termination.We treat recursion in the same way as Groote* * and Vaan- drager [16]by adding process names recx.t to the signature for each t 2 O() to * *obtain that the recursion rules fit our format.However, it would be a better idea toincorpo* *rate recursion whitin our format as is done for the GSOS format [11]and De Simone's format [25* *]. __________________________________pppp p _x__;y__ ___;y__ nil (x + y)p x(x;y)p p p p p _x_;_y_p __x____p t[recx.t=x]_p (x_j_y)_____@H(x)________recx.t___ p Table 2. The rules for . Next,they define the unsuccessful termination predicate by simply takingpth* *e complement of the successful termination predicate;we will denote this predicate by : . In* * our approach we will have to explicitly define this predicate withpdeduction rules since we * *define the transition system in one step. In table3pwe give our rules for : .It might be argued that* * this is not so intuitive but the rules for : are quite straightforward. Moreover,if only the * *negative version of a predicate is necessary it can be an advantage; see the _6=0 predicate late* *r on. With the aid of both predicates Aceto and Hennessy inductively define their* * convergence predicate #; we list their rules intable 4. ________________________________________________pp p _________ _________ ff: ; ff 2fffi; g [ Act|(xx:+ y):p (y x:+x):p p p p __x:____p __x:____p __x:____p @H(x): (x;y): (y;x): p p p __x:_____p __x:____p t[recx.t=x]:_p ______(x_j_y):__________(yj_x):_______recx.t:___ p Table 3. The rules for : . ____________________________________ ffi # nil# #; 2 Act| __x_#__ t[recx.t=x]#_ x_#;y_#_ @H (x)# recx.t# (x+ y )# p p x_#;y_#_ x_;_y#_ x:_;x_#_ (x_j_y)_#____(x;y)_#_______(x;_y)#__ Table 4. The rules for #. Finally,Aceto and Hennessy give the rules for the non-deterministic choice * *+, the sequen- tial composition ;, the parallel composition j, the binding constructor recx._,* * and the encap- sulation operator @H(). Aceto and Hennessy also have a divergence predicate,whi* *ch is the complement of the convergence predicate. We omitted this predicate since they * *do not need it to define their operational semantics. However it is easy to define this pr* *edicate; we refer to [17]for an explicit operational semantics of the divergence predicate in pat* *h format. For moredetails on the process algebra of Aceto and Hennessy we refer to [1* *]. ______________________________________________________ _x!__x0___ _x!__x0___ __x!__x0__ x + y! x0 y+ x! x0 x; y! x0; y p x_;_y!__y0_ __x!__x0___ ___x!__x0__ x;y! y0 x j y! x0j y y j x! y j x0 x!a_x0;y!a_y0_ ____x!__x0____; =2H t[recx.t=x]!__x0 _x_j_y!|_x0j_y0_@H_(x)!__@H_(x0)__________recx.t!__x0_ Table 5. The action relations for each 2 Act|. The matter that we are interested in at the moment is that the rules in tab* *les 2-5 are well- founded and in path format so with our main result we immediately find that str* *ong bisimulation is a congruence. At this point onemay find that we are not entirely fair since Aceto and Hen* *nessy are, in fact, interested in rooted weak bisimulation and they have a lot of work to do * *to obtain that this is a congruence for their system.Therefore, we will provein the next examp* *le that rooted weak bisimulation is a congruence with our congruence theorem for strong bisimu* *lation. We leave as an open problem whether a similar trick can also be applied for the CC* *S like process algebra of Aceto and Hennessy. We have not succeeded in coding the weak termination and convergence predic* *ates of Aceto and Hennessy [1]in the path format. This seems to involve essential use of nega* *tive premises. This next example isan operational semantics of Van Glabbeek [14]for BPA|, * *which is a fragment of the theory ACP| that originates from Bergstra and Klop [9]. The s* *ubscript | stands for the silent move of Milner [20]. The operational semantics is given b* *y the rules of tables 1 and 6. Van Glabbeek [14]observes that his model is isomorphic to the g* *raph model of Baeten,Bergstra and Klop [4]. This means that two terms are strongly bisimil* *ar [22]in his model if and only if they are rooted weakly bisimilar [20]in the graph model, s* *o since all the rules of tables 1 and 6 are well-founded and in path format we know that strong* * bisimulation is a congruence and thus,rooted weak bisimulation on the graph model is also a con* *gruence. We can also apply this result to the entire operational semantics that Van Glabbee* *k gives for ACP|. _____________________________ a!a | p x!|_y;y!_a_x0_ x!|_y;y!a___p x!a x0 x!a p x!a_y;y!_|_x0_ x!a_y;y!|___p ___x!a_x0__________x!a_______ Table 6. Operational rules for the silent step. The next example is an operational semantics of the language BPA 0that orig* *inates from Baeten and Bergstra [3]. The theory BPA 0is the language BPA (that we already s* *aw above) with a zero object denoted by 0.They have for this constant the following laws x + 0 = x; x0 = 0; 0x = 0: Baeten and Bergstra explicitly state intheir paper: "We cannot define action r* *ules in the format of Groote and Vaandrager[16]or Groote [15]" (see [3], loc. cit. p. 87). * *The problems arise with the rules for the sequential composition: if x!a x0then we will only* * have xy!a x0y if y 6=0. In table 7 we give the rules that define the (postfix) predicate 6= * *0 and we give the rules for the sequential composition.Together with the first five rules of tabl* *e 1 they form an operational semantics for BPA0. It is not hard to check that all the rules are * *well-founded and in path format,so we obtain that bisimulation is a congruence. Our approach als* *o worksfor the extensions that Baeten and Bergstradiscuss. __________________________________________ a 6= 0 __x_6=_0_x + y 6=0x_6=_0y +x 6= 0 p x_6=_0;y6=_0 x!a_x0;y_6=_0 x!a__;_y6=_0_ ___xy6=_0_______xy!a_x0y________xy!a_y____ Table 7. The 6=0 predicate and rules for sequential composition. Often we see thatthe rules of an operational semantics have so-called side * *conditions.For instance, the following rule from Gro ote and Vaandrager [16]has a side conditi* *on: p a!a "; a 6= : This side condition is an abbreviation for the list containing for all a 2 A a * *rule a!a ". Thus,it is in fact a harmless side condition,since the rules can be replaced by an enum* *aration. Often, though, side conditions are notso harmless. This is the case ifa side conditio* *n contains a process term. An example of such a rule can be found in a paper of Moller and T* *ofts [21]on temporal CCS: __P!t_P_0__ ; jQjT < t: (1) P Q!t P0 Here jjT is called the maximal delay, which is a function and not a predicate. * *In theop erational semantics of Moller and Tofts there are no "free" occurrences of the maximal de* *lay function,but only side conditions as in display (1). Since this is the case,we can see the s* *ide condition jQjT < t as a mixfix (or distfix) predicate: jjT _a_:_x6b!_x!_a__;_8_b_>_a_:px6b! (x)! a (x0) (x)!a p _x6a!__ _x!b_x0_;b > a _x!b___;b > a __(x)6a!_____(x)6a!__________(x)6a!_______ Table 11.The additional rules for BPA with priority operator. system in their book, which is not in path format but it can easily be made int* *o path format since this system treats the priority operator (cf. the above example). We also* * want to stress that none of the transition systems in their bo ok satisfy the tyft/tyxt or the* * ntyft/ntyxt format. 3. Term deduction systems All the examples that we treated insection 2 are, in fact, term deduction syste* *ms. In this section we formalize this notion,which generalizes the notion of a transition system sp* *ecification. In a transition system specification we have a transition relation !a for each labe* *l a, whereasin a term deduction system we have just a set of relation symbols and a set of pre* *dicate symbols. Having general relation symbols is an advantage. For instance, the operational * *semantics for temporalCCS of Moller and Tofts (from which we treated the tricky part in sect* *ion 2) provides two transition relations; this can be easily modelled with a term deduction sys* *tem but not with a transition system specification.But we can also think of the combination* * of a transition relation with a totally different relation, such as Wang's syntactical inequali* *ty relation P 6=Q that he uses in an operational semanticsfor probabilistic CCS (q.v. [26]). Before we give the definition of a term deduction system we will list some * *preliminariesfor completenesssake. We assumethat we have an infinite set V of variables with typical elements * *x;y ; z; :.: : A (single sorted) signature is a set offunction symbols together with their ar* *ity. If thearity of a function symbol f 2 is zero we say that f is a constant symbol. The notion* * of a term (over ) is defined as expected: x 2V is a term; if t1; : :;:tn are terms and i* *f f2 is n-ary then f(t1; : :;:tn) is a term. Aterm is also called an open term; if it contain* *s novariables we call it closed. We denote theset of closed terms by C() and the set of open ter* *ms by O() (note that a closed term is also open).We also want to speak about the variable* *s occurring in terms: let t 2 O() then var(t) V is the set of variables occurring in t. A substitution oe is a map from the set of variables into the set of terms * *over a given signature. This map can easily be extended to the set of all terms by substitut* *ing for each variable occurring in an open term its oe -image. Definition (3.1) A term deduction system is a structure (;D) with a signature* * and D a set of deduction rules. The set D = D(Tp;Tr) is parameterized with two sets, * *which are called respectively the set of predicatesymbols and the set of relation symbols* *. Let P 2 Tp and R 2 Tr, and s; t;u 2 O(). We call expressions Ps and tRu formulas. A dedu* *ction rule d 2 D has the form H_ C with H a set of formulas and C a formula. We call the elements of H the hypothe* *ses of d and we call the formula Cthe conclusion of d. If the set of hypotheses of a deducti* *on rule is empty we call such a rule an axiom. We denote an axiom simply by its conclusion provi* *ded that no confusion can arise. The notions "substitution", "var", and "closed" extend to * *formulas and deduction rules as expected. Definition (3.2) Let T = (;D) be a term deduction system. Aproof of a formula* * from T is a well-founded upwardly branching tree of which the nodes are labelle* *d by formulas such that the root is labelled with and if \ is the label of a node q and f\i:* * i 2 Ig is the set of labels belonging to the nodes fqi: i 2 Ig directly above qthen there is a de* *duction rule fOEi:_i_2_Ig OE and a substitution oe: V ! O() such that oe(OE) = \ and oe(OEi) = \ifor i 2 I* *. The length of q is jqj = supfjqij +1 : i 2 I g.The length of a proof is the length of its * *root. If a proof of exists, we say that is provable from T, notation T` . Apro* *of is closed if it contains only closed formulas. Lemma (3.3) If a closed formula is provable from a term deduction system then * *it is provable by a closed proof. Proof. Easy. Confer lemma 3.3 of Groote and Vaandrager [16]. 4. Structured state systems and bisimulation In this section we define the notions of a structured state system and bisimula* *tion. Astructured state system is a generalization of thenotion of a labelled transition system. * * In a labelled transition system we have for each label a transition relation, whereas in a st* *ructured state system we have just relations and predicates. At first sight,this gives rise to* * a stronger notion of bisimulation on a structured state system since we have a transfer property for* * each relation and predicate. But our definition of bisimulation mostly coincides with the ones in* * the literature. For instance, in theexample of Moller and Tofts there are two transition relati* *ons so they need to extend the notion of bisimulation to the two relations. In our setting * *we moreover demand that bisimilar processes must have the same maximal delay. So we have "m* *aximal delay" bisimulation. Moller and Tofts state in their proposition 3.3 that our m* *aximal delay bisimulation coincides with their notion of bisimulation. The same phenomenon * *occurs in Klusener [18]with our UL-bisimulation, Klusener's U-bisimulation,and ordinary b* *isimulation (U means ultimate delay and L meanslatest possible action). Also for the examp* *les with negative premises that we gave in section 2 we have to prove that bisimulationi* *s the same as our "negative" bisimulation.For small term deduction systems this will not be a* * problem but for bigger ones it can become a problem. Therefore, it is better to allow negat* *ive premises in our rules. However, this is out of the scope of this paper (but we are currentl* *y studying this). Definition (4.1) Astructured state system is a triple (S; Sp; Sr) where S is a* * set of states, Sp is a subset of the power set of Sand Sr is a subset of the power set of S S. T* *he sets Sp and Srare called respectively the set of predicates and the set of relations. Remark (4.2) Astructured state system is a generalization of a labelled transi* *tion system. To see this take an empty set of predicates and take for the set of relations t* *he labelled transition relation. Next,we will define the notion of strong bisimulation on a structured state* * system, which is based on Park [22]. Definition (4.3) Let G = (S; Sp; Sr) be a structured state system. A relation * *B S S is called a (strong) bisimulation iffor all s; t 2 Swith sBt the following cond* *itions hold. For all R2 Sr 8s02 S(sRs0) 9t02 S: tRt0^ s0Bt0); 8t02 S(tRt0) 9s02 S: sRs0^ s0Bt0); and for all P 2Sp P s , P t: The first two conditions are known as the transfer property. Two states s;t 2 S* *are bisimilar in the structured state system G if there exists a bisimulation relation containin* *g the pair (s;t). Notation s G t or s t provided that no confusion can arise. Note that bisimila* *rity is an equivalencerelation. A term deduction system induces in a natural way a structured state system. Definition (4.4) Let T =(; D) be a termdeduction system and let D =D(Tp; Tr). * *The structured state system G induced byT has as its set of states S =C(); the pred* *icates and relations are the following. n fifi o Sp = t 2 C() j T ` Pt fiP 2 Tp ; n fifi o Sr = (s;t) 2 C() C() j T ` sRt fiR 2 Tr : We will call s;t 2 C() bisimilar,notation s T t if s G t.Note that T is also an* * equivalence relation. Again we omitthe subscript when it is clear what T is. Definition (4.5) We say thattwo term deduction systems are equivalent if they * *induce the same structured state system. 5. The congruence theorem This section is devoted to the congruence theorem. We expect that our congruenc* *e theorem can be proved by simply adaptingthe proof of the congruence theorem of Groote a* *nd Vaan- drager[16]to the present situation.However, weprove a stronger result than just* * a congruence theorem since we moreover show that every term deduction system in path format * *can be re- duced to a transition system specification intyft/tyxt format and then apply th* *e theorem of Groote and Vaandrager. We strongly conjecture that we can prove a similar reduction/congruence the* *orem for the situation with negative premises by applying the congruence theorem of Groote [* *15](thattreats the situation with negative premises). First,we will define the notions necessary to state the main resultand then* * we will prove it. Definition (5.1) Let T =(; D) be a term deduction system with D =D (Tp; Tr). L* *et in the following I and J be index sets of arbitrary cardinality, let ti; sj; t 2 O* *() for all i 2 I and j 2 J, let Pj; P 2 Tpbe predicate symbols for all j 2 J, and let Ri;R 2 Tr * *be relation symbols for all i 2 I. A deduction rule d 2D is in ptyft format if it has the form fPjsj:_j2_J_g_[_ftiRiyi_:_i 2 Ig f(x1; : :;:xn)Rt with f 2 an n-ary function symbol and X [ Y = fx1; : :;:xng [ fyi: i 2 Ig V a* * set of distinct variables. If var(d) = X [Y we call d pure. Avariable in var(d) that d* *oes not occur in X [Y is called free. A deduction rule d 2D is in ptyxt format if it has the form fPjsj:_j2_J_g_[_ftiRiyi_:_i 2 Ig xRt with X[ Y = fxg [ fyi: i 2 Ig V a set of distinct variables. If var(d) = X[ Y * *we calld pure. A variable invar(d) that does not occur in X[ Y is called free. A deduction rule is in ptyf format if it has the form fPjsj:_j2_J_g_[_ftiRiyi_:_i 2 Ig Pf(x1; : :;:xn) with f 2 an n-ary function symbol and fx1; : :;:xng [ fyi : i 2 Ig V a set of* * distinct variables. The notions pure and free are defined as expected. A deduction rule is in ptyx format if it has the form fPjsj:_j2_J_g_[_ftiRiyi_:_i 2 Ig P x with fxg [ fyi: i 2 Ig V a set of distinct variables.The notions pure and free* * are defined as expected. We explane the names of the deduction rules. The pin the phrases ptyft, pt* *yxt, ptyf, and ptyx refers to the predicates occurring in the rules, the ty refers to the * *relation part in the set of hypotheses, and the ft, xt, f, and x refer to the variousconclusions* *. The names tyft and tyxt are taken from Groote andVaandrager [16]. If a deduction rule d2 D has one of the above forms we say that this rule i* *s in path format, which stands for "predicates and tyft/tyxt hybrid format". A term deduction sy* *stem is in path format if all its rules are.A term deduction system is called pure if all * *its rules are pure. Aterm deduction system is in tyft/tyxt format if it is in path format and i* *ts set of predicate symbols is empty. We need the technical notion of well-foundedness of a term deduction system* *,which will be used in the proof of the congruence theorem. We will use a property in the p* *roof that in general does not hold for a non well-founded term deduction system; we will ret* *urn to this in the proof of the theorem. It is an open question if the requirement of well-* *foundedness is really necessary. However,we heard from Fokkink [12] that the requirement is pr* *obably not necessary for the tyft/tyxt format and that his results easily generalize to ou* *r setting. Definition (5.2) Let T =(;D) be a term deduction system and let F be a set of * *formulas. The dependency graph of F is adirected graph with variables occurring in F as i* *ts nodes.The edge x ! yis an edge of the dependency graph if and only if there is a tRs 2 F* * with x 2 var(t) and y2 var(s). The set Fis called well-founded if any backward chain of edges in its depen* *dency graph is finite. A deduction rule is called well-founded if its set of hypotheses is so.* * Aterm deduction system is called well-founded if allits deduction rules are well-founded. Lemma (5.3) For every well-founded term deduction system in path format there * *is an equivalent pure well-founded term deduction system in path format. Proof. Essentially the proof of Lemma 5.9 in Groote and Vaandrager [16]. Theorem (5.4) Let T = (;D) be a well-founded term deduction system in path for* *mat then strong bisimulation is a congruence for all function symbols occurring in . Proof. Groote and Vaandrager [16]proved this theorem in the case that the set o* *f predicate symbols is empty, that is, if the term deduction system is in tyft/tyxt format.* * Our strategy to prove the non-empty caseis to construct from a term deduction system a new o* *ne without predicates with the property that two terms are bisimilar in the old term deduc* *tion system if and only if they are bisimilar in the new one. We make the new term deduction s* *ystem from the old one by coding each predicatein the old system as a special relation in * *the modified one. To begin with, we construct from a term deduction system a new one by exten* *ding the original signature with a xenoconstant and moving the predicates of the origina* *l system to xenorelations. Let T =(; D) be a term deduction system and suppose that D =D(Tp; Tr) with * *Tp 6= ;. In accordance with lemma (5.3)we may assume that T is pure. We define a new* * term deduction system T0= (0;D0). Let be aconstant function symbol that is strange * *to and define 0= [ fg. Let D0= D0(;;T0r) with T0r= Tr [fRP j P 2 Tpg (disjointunion).* * A relation symbol RP forP 2 Tpis defined as follows. For two terms s and t over 0* *we have sRPt if and only if Ps and t = . The set of deduction rules is D0= fd0j d 2 Dg and a* * deduction rule d0is constructed from an old rule d 2 D asfollows. Let d = H_C. The set of* * hypotheses of d0is the set H but with the "predicate part" fPjsj j j2 J g replaced by fsjR* *Pjzjj j 2 Jg with fzjj j 2 Jg a set of distinct variables disjoint with var(d). If the concl* *usion of the old rule is of the form Pt then the conclusion of the new rule istRP . In the other* * case C remains the same. Note that T0is pure, well-founded and in tyft/tyxt format. Now we will prove that two closed -terms u and v arebisimilar in the origin* *al system T if and only if they are bisimilar in thesystem T 0. In order to do this we use* * a number of properties that are listed below. Let P 2 Tp, R 2 Tr, and u; v 2 C(0) C() (unless otherwise specified) then * *the following properties hold. (We denote the bisimulation relation in T by and in* *T 0by 0.) (i) T 0` uRPv =) v = (ii ) u 2 C (); T0` uRv =) v 2 C() (iii) u; v 2 C(); T0` uRv =) T` uRv (iv) u 2 C (); T0` uRP =) T` P u (v) u 2 C (); T ` Pu =) T 0` uRP (vi) u; v 2 C(); T ` uRv=) T0` uRv (vii) u; v2 C() =) (u v () u 0v) Before we continue, we discuss properties (ii)-(vi). Property (ii) says tha* *t if we can prove in the xenosystem that an old term u isrelated with a term v by means of an old* * relation R that vcannot be a xenoterm. Asimple example due to Fokkink [12]shows that for t* *his property the well-foundedness cannot be missed. Suppose that we have a signature that co* *nsists of a single constant a. We have two rules: xRx; xRx_aSx: Clearly,this system is not well-founded. The xenosystem has the same rules; onl* *y the signature is extended with the xenoconstant . It is easy to see that we can derive in thi* *s new system that aS. The properties (iii)-(vi) actually form two bi-implications saying that eve* *ry provable for- mula in the old system is provable in the xenosystem and vice versa. We split * *these bi- implications into four statements for (proof ) technical reasons. Now we prove the properties. The proof of (i) follows directly from the definition of the deduction rule* *s in D0. We prove (ii ) with transfinite induction on the length of the proof (see s* *ection 3 for the definition of this length). Without loss of generality we may assume that the p* *roof is closed; see lemma (3.3). Suppose that (ii) holds for all lengths ff< fiand that we have* * a proof of uRv of length fi. The last rule d0used in this proof must be of the following form fsjRPjzj:_j2_J_g_[_ftiRiyi:_i_2 Ig sRt : (1) There is a substitution oewith oe(s) = u and oe(t) = v. Note that var(t) var(s* *) [ fyi: i 2 Ig so it suffices to show that oe(yi) 2 C() for all i 2 I since oe(s) 2 C(). We de* *note the set of all yiby Y. Suppose that there is an yi02 Y with oe(yi0) 2 C(0) n C(). This con* *tradicts the well-foundedness of the rule d0, for T0` oe(ti0)Ri0oe(yi0) so with the inductio* *n hypothesiswe find that oe(ti0) 2 C(0) n C(). Since ti0isa -term, this must be the result of * *a substitution. This can only be due to a variable yi12Y . With induction on the subsubscript w* *e find an infinite backward chain of edges yi0 yi1 : :i:n the dependency graph ofd0. We simultaneously verify (iii)-(vi) with transfinite induction on the maxim* *um ff of the lengths of the proofs. Suppose that (iii)-(vi) hold for all maxima ff