Conservative Extension in Structural Operational Semantics Luca Aceto\Lambda Wan Fokkinky Chris Verhoefz 1 Introduction Structural operational semantics (SOS) [44] provides a framework to give an operational semantics to programming and specification languages. In particular, because of its intuitive appeal and flexibility, SOS has found considerable application in the study of the semantics of concurrent processes. SOS generates a labelled transition system, whose states are the closed terms over an algebraic signature, and whose transitions are supplied with labels. The transitions between states are obtained inductively from a transition system specification (TSS), which consists of so-called transition rules of the form premisesconclusion . A typical example of a transition rule is x a! x0 xky a! x0ky stipulating that if t a! t0 holds for closed terms t and t0, then so does tku a! t0ku for each closed term u. In general, validity (or invalidity) of the positive (or negative) premises of a transition rule, under a certain substitution, implies validity of the conclusion of this rule under the same substitution. This column is an excerpt from [2], which gives an overview of recent results in the field of SOS, with an emphasis on existing formats for TSSs. \Lambda BRICS (Basic Research in Computer Science), Centre of the Danish National Research Foundation, Department of Computer Science, Aalborg University, Fredrik Bajers Vej 7-E, DK-9220 Aalborg O/, Denmark. Email: luca@cs.auc.dk. Partially supported by a grant from the Italian CNR, Gruppo Nazionale per l'Informatica Matematica (GNIM). yCWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands. Email: wan@cwi.nl. Partially supported by a grant from the Nuffield Foundation. zUniversity of Amsterdam, Department of Computer Science, Programming Research Group, Kruislaan 403, 1098 SJ Amsterdam, The Netherlands. Email: x@wins.uva.nl. 1 Each of these formats comes equipped with a rich body of results that are guaranteed to hold for any process calculus whose TSS is within that format. Over and over again, process calculi such as CCS [40], CSP [47], and ACP [11] have been extended with new features, and the TSSs that provide the operational semantics for these process algebras were extended with transition rules to describe these features; see, e.g., [10] for a systematic approach. A question that arises naturally is whether or not the the original and the extended TSS induce the same transitions t a! t0 for closed terms t in the original domain. Usually it is desirable that an extension is operationally conservative, meaning that the provable transitions for an original term are the same both in the original and in the extended TSS. Groote and Vaandrager [34, Thm. 7.6] proposed syntactic restrictions on a TSS, which automatically yield that an extension of this TSS with transition rules that contain fresh function symbols in their sources is operationally conservative. Bol and Groote [18, 33] supplied this conservative extension format with negative premises. Verhoef [49] showed that, under certain conditions, a transition rule in the extension can be allowed to have an original term as its source. D'Argenio and Verhoef [22, 23] formulated a generalization in the context of inequational specifications. Fokkink and Verhoef [25] relaxed the syntactic restrictions on the original TSS, and lifted the operational conservative extension result to higher-order languages. This column contains an exposition on existing conservative extension formats for SOS, and their applications with respect to term rewriting systems and completeness of axiomatizations. Predicates in SOS semantics can be coded as binary relations [34]. Moreover, negative premises can often be expressed positively using predicates [9]. However, in the literature SOS definitions are often decorated with predicates and/or negative premises. For example, predicates are used to express matters like (un)successful termination, convergence, divergence [3], enabledness [14], maximal delay, and side conditions [42]. Negative premises are used to describe, e.g., deadlock detection [38], sequencing [17], priorities [7, 21], probabilistic behaviour [39], urgency [19], and various real [37] and discrete time [6, 35] settings. Since predicates and negative premises are so pervasive, and often lead to cleaner semantic descriptions for many features and constructs of interest, we deal explicitly with these notions. The organization of this column is as follows. Sect. 2 gives an overview of the basics of SOS. Sect. 3 presents syntactic constraints to ensure that an extension of a TSS is operationally conservative. Sect. 4 and 5 contain applications of conservative extension in equational specification and term rewriting. Sect. 6 finishes with some conclusions. 2 2 Structural Operational Semantics In this section we present the basic notions from process theory that are needed in the remainder of this column. 2.1 Labelled Transition Systems We begin by reviewing the model of labelled transition systems [36, 44], which are used to express the operational semantics of many process calculi. Definition 2.1 A labelled transition system (LTS) is a quadruple (Proc; Act; n a!j a 2 Acto; Pred); where: ffl Proc is a set of states, ranged over by s; ffl Act is a set of actions, ranged over by a; b; ffl a!` Proc\Theta Proc for each a 2 Act. We use the more suggestive notation s a! s0 in lieu of (s; s0) 2 a!, and write s a9 if s a! s0 for no state s0; ffl P ` Proc for every P 2 Pred. We write sP (resp. s:P ) if state s satisfies (resp. does not satisfy) predicate P . Relations s a! s0 and predicates sP in an LTS are called transitions. In what follows, an LTS is often identified with its collection of transitions. We trust that the meaning will always be clear from the context. LTSs describe the operational behaviour of processes in great detail. In order to abstract away from irrelevant information on the way that processes compute, a wealth of notions of behavioural equivalence over the states of an LTS have been studied in the literature on process theory. A systematic investigation of these notions is presented in [28], where van Glabbeek presents the linear time/branching time spectrum. This lattice contains all the known behavioural equivalences over LTSs, ordered by inclusion. 2.2 Term Algebras We start from a countably infinite set Var of variables, ranged over by x; y; z. 3 Definition 2.2 A signature \Sigma is a set of function symbols, disjoint from Var, together with an arity mapping that assigns a natural number ar (f ) to each function symbol f . A function symbol of arity zero is called a constant, while function symbols of arity one and two are called unary and binary, respectively. The arity of a function symbol represents its number of arguments. Definition 2.3 The set (\Sigma ) of (open) terms over a signature \Sigma , ranged over by t; u, is the least set such that: ffl each x 2 Var is a term; ffl f (t1; : : : ; tar(f)) is a term, if f is a function symbol and t1; : : : ; tar(f) are terms. T(\Sigma ) denotes the set of closed terms over \Sigma , i.e., terms that do not contain variables. For a constant a, the term a() is abbreviated to a. By convention, whenever we write a term-like phrase (e.g., f (t; u)), we intend it to be a term (i.e., f is binary). Definition 2.4 A substitution is a mapping oe : Var ! (\Sigma ). A substitution is closed if it maps each variable to a closed term in T(\Sigma ). A substitution extends to a mapping from terms to terms as usual; the term oe(t) is obtained by replacing occurrences of variables x in t by oe(x). 2.3 Transition System Specifications We proceed to introduce the main objects of study in the field of SOS, viz. transition system specifications. Definition 2.5 Let \Sigma be a signature, and let t and t0 range over (\Sigma ). A transition rule ae is of the form H=ff, with H a collection of positive premises t a! t0 and tP , and of negative premises t a9 and t:P . Moreover, the conclusion ff is of the form t a! t0 or tP . The left-hand side of the conclusion is the source of ae. A transition rule is closed if it does not contain variables. A transition system specification (TSS) is a collection of transition rules. A TSS is positive if its transition rules do not contain negative premises. 4 For the sake of clarity, we will often display transition rules in the form H ff . The first systematic study of TSSs may be found in [48], while the firststudy of TSSs with negative premises appeared in [16]. We proceed to define when a transition is provable from a TSS. The following notion of a proof from [31] generalizes the standard definition (see, e.g., [34]) by allowing for the derivation of closed transition rules. The derivation of a transition ff corresponds to the derivation of the closed transition rule H=ff with H = ?. The case H 6= ? corresponds to the derivation of ff under the assumptions in H. Definition 2.6 Positive literals are transitions t a! t0 and tP , while negative literals are expressions t a9 and t:P , where t and t0 range over the collection of closed terms. A literal is a positive or negative literal. Definition 2.7 Let T be a TSS. A proof of a closed transition rule H=ff from T is a well-founded, upwardly branching tree whose nodes are labelled by literals, where the root is labelled by ff, and if K is the set of labels of the nodes directly above a node with label fi, then 1. either K = ? and fi 2 H, 2. or K=fi is a closed substitution instance of a transition rule in T . If a proof of H=ff from T exists, then H=ff is provable from T . 2.4 Three-Valued Stable Models In the presence of negative premises, the meaning of a TSS is sometimes ambiguous. For example, one can express that a transition holds if it does not hold. In order to associate an LTS to each TSS, we use the notion of a (least) three-valued stable model, introduced by Przymusinski [46] in logic programming. A three-valued stable model partitions the collection of transitions into three disjoint sets: the set C of transitions that are certainly true, the set U of transitions for which it is unknown whether or not they are true, and the set F of remaining transitions that are false. Definition 2.8 A disjoint pair of sets of transitions hC; U i constitutes a three-valued stable model for a TSS T if: - a transition ff is in C iff T proves a closed transition rule N=ff where N contains only negative literals and C [ U j= N ; - a transition ff is in C [ U iff T proves a closed transition rule N=ff where N contains only negative literals and C j= N . 5 Each TSS has one or more three-valued stable models. For example, the TSS a:P 2 aP1 a:P1 aP2 has hfaP1g; ?i, hfaP2g; ?i, and h?; faP1; aP2gi as its three-valued stable models. Each TSS T affords a unique (information-)least three-valued stable model hC; U i, in the sense that the set U is maximal. Przymusinski [46] showed that this least three-valued stable model coincides with the so-called well-founded model that was introduced by van Gelder, Ross, and Schlipf [27] in logic programming. It is advocated in, e.g., [18, 32] that a TSS is meaningful if and only if its least three-valued stable model does not contain unknown transitions. In particular, each TSS that does not contain negative premises in its transition rules satisfies this requirement. The reader is referred to [31, 32] for more information on three-valued stable models and related notions. 3 Operational Conservative Extension Often one wants to add new operators and rules to a given TSS. Therefore, a natural operation on TSSs is to take their componentwise union. The following definition stems from [34]. Definition 3.1 Let T0 and T1 be TSSs whose signatures \Sigma 0 and \Sigma 1 agree on the arity of the function symbols in their intersection. We write \Sigma 0 \Phi \Sigma 1 for the union of \Sigma 0 and \Sigma 1. The sum of T0 and T1, notation T0 \Phi T1, is the TSS over signature \Sigma 0 \Phi \Sigma 1 containing the rules in T0 and T1. An operational conservative extension requires that an original TSS and its extension prove exactly the same closed transition rules that have only negative premises and an original closed term as their source. (This notion of an operational conservative extension is related to an equivalence notion for TSSs in [24, 32]: two TSSs are equivalent if they prove exactly the same closed transition rules that have only negative premises.) Definition 3.2 A TSS T0 \Phi T1 is an operational conservative extension of TSS T0 if for each closed transition rule N=ff such that: - N contains only negative literals; - the left-hand side of ff is in T(\Sigma 0); - N=ff is provable from T0 \Phi T1; we have that N=ff is provable from T0. 6 3.1 Guaranteeing Operational Conservative Extension We start by defining the notion of a source-dependent variable [25, 30], which will be an important ingredient of a rule format to ensure that an extension of a TSS is operationally conservative. In order to conclude that an extended TSS is operationally conservative over the original TSS, we need to know that the variables in the original transition rules are source-dependent. In the literature this criterion is sometimes neglected. For example, in [43] an extended TSS is considered in which each transition rule in the extension contains a fresh operator in its source, and from this fact alone it is concluded that the extension is operationally conservative. In general, however, this characteristic is not sufficient, as is shown in the next example. Example: Let a and b be constants. Consider the TSS over signaturef ag that consists of the transition rule xP=aP . Extend this TSS with the TSS over signature fbg that consists of the transition rule ?=bP , which contains the fresh constant b in its source. The transition aP can be proved in the extended TSS, but not in the original one, so this extension is not operationally conservative. \Lambda Definition 3.3 The source-dependent variables in a transition rule ae are defined inductively as follows: - all variables in the source of ae are source-dependent; - if t a! t0 is a premise of ae and all variables in t are source-dependent, then all variables in t0 are source-dependent. A transition rule is source-dependent if all its variables are. Note that the transition rule xP=aP from the example above is not sourcedependent, because its variable x is not. Thm. 3.4 below, which stems from [25], formulates sufficient criteria for a TSS T0 \Phi T1 to be an operational conservative extension of TSS T0. We say that a term in (\Sigma 0 \Phi \Sigma 1) is fresh if it contains a function symbol from \Sigma 1n\Sigma 0. Similarly, an action or predicate symbol in T1 is fresh if it does not occur in T0. Theorem 3.4 Let T0 and T1 be TSSs over signatures \Sigma 0 and \Sigma 1, respectively. Under the following conditions, T0 \Phi T1 is an operational conservative extension of T0. 1. Each ae 2 T0 is source-dependent. 7 2. For each ae 2 T1, ffl either the source of ae is fresh,ffl or ae has a premise of the form t a! t0 or tP , where: - t 2 (\Sigma 0); - all variables in t occur in the source of ae; - t0, a, or P is fresh. 3.2 Applications to TSSs We apply Thm. 3.4 to some TSSs from the literature. Basic Process Algebra with Empty Process The signature of basic process algebra with empty process [50], denoted by BPAffl(Act), consists of the following operators: - a set Act of constants, representing indivisible behaviour; - a constant ffl, called empty process, representing successful termination; - a binary operator +, called alternative composition, where a term t1 + t2 represents the process that executes either t1 or t2; - a binary operator \Delta , called sequential composition, where a term t1 \Delta t2 represents the process that executes first t1 and then t2. So the BNF grammar [5] for BPAffl(Act) is (with a 2 Act): t ::= a j ffl j t1 + t2 j t1 \Delta t2 : The intuition for the operators in BPAffl(Act) is formalized by the transition rules in Table 1 from [11], which constitute the TSS for BPAffl(Act). This TSS defines transitions t a! t0 to express that term t can evolve into term t0 by the execution of action a 2 Act, and transitions tp to express that term t can terminate successfully. The variables x, x0, y, and y0 in the transition rules range over the collection of closed terms, while the a ranges over Act. The transition rules for BPAffl(Act) are source-dependent. For example, consider the third transition rule for sequential composition in Table 1: x a! x0 x \Delta y a! x0 \Delta y 8 a a! ffl fflp xp x + yp x a! x0 x + y a! x0 yp x + yp y a! y0 x + y a! y0 xp yp x \Delta yp xp y a! y0 x \Delta y a! y0 x a! x0 x \Delta y a! x0 \Delta y Table 1: Transition Rules for BPAffl(Act). The variables x and y are source-dependent, because they occur in the source. Moreover, since x is source-dependent, the premise x a! x0 ensures that x0 is source-dependent. Since the three variables x, x0, and y in this transition rule are source-dependent, the transition rule is source-dependent. Extending the Set of Actions Suppose that Act is extended to a set Actext . The TSS for BPAffl(Actext ) is the TSS for BPAffl(Act) in Table 1, with the proviso that a ranges over Actext . We make the following observations concerning the extra transition rules in the TSS for BPAffl(Actext ): ffl the source of the transition rule a a! ffl for a 2 Actext nAct contains the fresh constant a; ffl each transition rule concerning an a-transition of an alternative or sequential composition with a 2 Actext nAct, such as x a! x0 x + y a! x0 contains a premise with the fresh relation symbol a! and with as lefthand side a variable from the source. So, since the transition rules for BPAffl(Act) are source-dependent, it can be concluded from Thm. 3.4 that BPAffl(Actext ) is an operational conservative extension of BPAffl(Act). 9 Priorities The language BPAffl`(Act) is obtained by adding the priority operator ` from [7] to BPAffl(Act). This function symbol assumes a partial order ! on Act. Intuitively, the process `(t) is obtained by eliminating all transitions s a! s0 from the process t for which there is a transition s b! s00 with a ! b. For example, if a ! b then `(a + b) can execute the action b but not the action a. The TSS for BPAffl`(Act) consists of the transition rules in Tables 1 and 2, where the transition rules in the latter table capture the operational semantics of the priority operator. This TSS has a unique least three-valued stable model, which does not contain unknown transitions. (This follows from the fact that the TSS is stratifiable [33, 45].) xp `(x)p x a! x0 x b9 for a ! b `(x) a! `(x0) Table 2: Transition Rules for the Priority Operator. The two transition rules for the priority operator in Table 2 contain the fresh function symbol ` in their sources. So, since the transition rules for BPAffl(Act) are source-dependent, Thm. 3.4 implies that BPAffl`(Act) is an operational conservative extension of BPAffl(Act). 3.3 Implications for Three-Valued Stable Models In [25] it was noted that the operational conservative extension notion as formulated in Def. 3.2 implies a conservativity property for three-valued stable models. If an extended TSS is operationally conservative over the original TSS, in the sense of Def. 3.2, and if a three-valued stable model of the extended TSS is restricted to those transitions that have an original term as left-hand side, then the result is a three-valued stable model of the original TSS. Proposition 3.5 Let T0 \Phi T1 be an operational conservative extension of T0. If hC; U i is a three-valued stable model of T0 \Phi T1, then C0 \Delta = fff 2 C j the left-hand side of ff is in T(\Sigma 0)g U 0 \Delta = fff 2 U j the left-hand side of ff is in T(\Sigma 0)g is a three-valued stable model of T0. 10 The converse of Prop. 3.5 also holds, in the following sense. If an extended TSS is operationally conservative over the original TSS, then each threevalued stable model of the original TSS can be obtained by restricting some three-valued stable model of the extended TSS to those transitions that have an original term as left-hand side. Proposition 3.6 Let T0\Phi T1 be an operational conservative extension of T0. If hC; U i is a three-valued stable model of T0, then there exists a three-valued stable model hC0; U 0i of T0 \Phi T1 such that C \Delta = fff 2 C0 j the left-hand side of ff is in T(\Sigma 0)g U \Delta = fff 2 U 0 j the left-hand side of ff is in T(\Sigma 0)g : Corollary 3.7 Let T0 \Phi T1 be an operational conservative extension of T0. If hC; U i is the least three-valued stable model of T0 \Phi T1, then C0 \Delta = fff 2 C j the left-hand side of ff is in T(\Sigma 0)g U 0 \Delta = fff 2 U j the left-hand side of ff is in T(\Sigma 0)g is the least three-valued stable model of T0. 4 Applications to Axiomatizations This section discusses how operational conservative extension can be used to derive that an extension of an axiomatization is so-called axiomatically conservative, or that an axiomatization is complete or !-complete with respect to some behavioural equivalence. 4.1 Axiomatic Conservative Extension Definition 4.1 A (conditional) axiomatization over a signature \Sigma consists of a set of (conditional) equations, called axioms, of the form t0 = u0 ( t1 = u1; : : : ; tn = un with ti; ui 2 (\Sigma ) for i = 0; : : : ; n. An axiomatization gives rise to a binary equality relation = on (\Sigma ) thus: ffl if t0 = u0 ( t1 = u1; : : : ; tn = un is an axiom, and oe a substitution such that oe(ti) = oe(ui) for i = 1; : : : ; n, then oe(t0) = oe(u0); ffl the relation = is closed under reflexivity, symmetry, and transitivity; 11 ffl if f is a function symbol and u = u0, then f (t1; : : : ; ti\Gamma 1; u; ti+1; : : : ; tar(f)) = f (t1; : : : ; ti\Gamma 1; u0; ti+1; : : : ; tar(f)): Definition 4.2 Assume an axiomatization E, together with an equivalence relation , on T(\Sigma ). 1. E is sound modulo , iff t = u implies t , u for all t; u 2 T(\Sigma ). 2. E is complete modulo , iff t , u implies t = u for all t; u 2 T(\Sigma ). Note that the above definitions of soundness and completeness, albeit standard in the literature on process algebras, are weaker than the classic ones in logic and universal algebra, where they are required to apply to arbitrary open expressions. Definition 4.3 Let E0 and E1 be axiomatizations over signatures \Sigma 0 and \Sigma 0\Phi \Sigma 1, respectively. The axiomatization E0[E1 is an axiomatic conservative extension of E0 if every equality t = u with t; u 2 T(\Sigma 0) that can be derived from E0 [ E1 can also be derived from E0. The next theorem from [49] can be used to derive that an extension of an axiomatization is axiomatically conservative. Theorem 4.4 Let , be an equivalence relation on T(\Sigma 0 \Phi \Sigma 1). Assume axiomatizations E0 and E1 over \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively, such that: 1. E0 [ E1 is sound over T(\Sigma 0 \Phi \Sigma 1) modulo ,; 2. E0 is complete over T(\Sigma 0) modulo ,. Then E0 [ E1 is an axiomatic conservative extension of E0. The idea behind Thm. 4.4 is as follows. Suppose that t = u can be derived from E0 [ E1 for t; u 2 T(\Sigma 0). Soundness of E0 [ E1 (requirement 1) yields t , u. Hence, completeness of E0 (requirement 2) yields that t = u can be derived from E0. Thm. 4.4 is particularly helpful in the case of an operational conservative extension of a TSS. Assume TSSs T0 and T1 over signatures \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively, where T0 \Phi T1 is an operational conservative extension of T0. Moreover, let , be an equivalence relation on states in LTSs. Since the states in the LTSs associated with T0 and T0 \Phi T1 are closed terms, the equivalence relation , carries over to T(\Sigma 0) and T(\Sigma 0 \Phi \Sigma 1), respectively. 12 Owing to operational conservativity, the equivalence relation , on T(\Sigma 0) as induced by T0 agrees with this equivalence relation on T(\Sigma 0) as induced by T0 \Phi T1. Applications of Thm. 4.4 in process algebra, in the presence of an operational conservative extension of a TSS, are abundant in the literature; we give a typical example. Example: Using Thm. 3.4 it is not hard to see that the process algebra ACP` [7] is an operational conservative extension of ACP. Baeten, Bergstra, and Klop introduced in op. cit. an axiomatization E0 that is complete over ACP modulo bisimulation equivalence, and an axiomatization E0 [ E1 that is sound over ACP` modulo bisimulation equivalence. Hence, Thm. 4.4 says that E0 [E1 is an axiomatic conservative extension of E0. (In [7], fifteen pages were needed to prove this fact for the more general case of open terms, by means of a term rewriting analysis.) \Lambda 4.2 Completeness of Axiomatizations The next theorem from [49] can be used to derive that an axiomatization is complete. Theorem 4.5 Let , be an equivalence relation on T(\Sigma 0 \Phi \Sigma 1). Assume axiomatizations E0 and E1 over \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively, such that: 1. E0 [ E1 is sound over T(\Sigma 0 \Phi \Sigma 1) modulo ,; 2. E0 is complete over T(\Sigma 0) modulo ,; 3. for each t 2 T(\Sigma 0 \Phi \Sigma 1) there is a t0 2 T(\Sigma 0) such that t = t0 can be derived from E0 [ E1. Then E0 [ E1 is complete over T(\Sigma 0 \Phi \Sigma 1) modulo ,. The idea behind Thm. 4.5 is as follows. Let t; u 2 T(\Sigma 0 \Phi \Sigma 1) with t , u. There exist terms t0; u0 2 T(\Sigma 0) such that E0 [ E1 proves t = t0 and u = u0 (requirement 3). Soundness of E0 [ E1 (requirement 1) yields t , t0 and u , u0, which together with t , u implies t0 , u0. Finally, owing to completeness of E0 over T(\Sigma 0) (requirement 2), we may derive t0 = u0, and thus t = t0 = u0 = u. Thm. 4.5 is particularly helpful in the case of an operational conservative extension of a TSS. Assume TSSs T0 and T1 over signatures \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively, where T0 \Phi T1 is an operational conservative extension of T0. Moreover, let , be an equivalence relation on states in LTSs. Since the 13 states in the LTSs associated with T0 and T0 \Phi T1 are closed terms, the equivalence relation , carries over to T(\Sigma 0) and T(\Sigma 0 \Phi \Sigma 1), respectively. Owing to operational conservativity, the equivalence relation , on T(\Sigma 0) as induced by T0 agrees with this equivalence relation on T(\Sigma 0) as induced by T0 \Phi T1. Applications of Thm. 4.5 in process algebra, in the presence of an operational conservative extension of a TSS, are abundant in the literature; we give a typical example. Example: Using Thm. 3.4 it is not hard to see that the process algebra ACP [12] is an operational conservative extension of BPAffi. Bergstra and Klop presented in op. cit. an axiomatization E0 that is complete over BPAffi modulo bisimulation equivalence, and an axiomatization E0 [ E1 that is sound over ACP modulo bisimulation equivalence, and that satisfies requirement 3 above. Hence, Thm. 4.5 says that E0 [ E1 is complete over ACP modulo bisimulation equivalence. \Lambda For the precise proofs of Thm. 4.4 and Thm. 4.5, and for more detailed information such as generalizations of these results to axiomatizations based on inequalities, the reader is referred to [22, 23, 49]. 4.3 !-Completeness of Axiomatizations Definition 4.6 An axiomatization E over a signature \Sigma is !-complete if an equation t = u with t; u 2 (\Sigma ) can be derived from E whenever oe(t) = oe(u) can be derived from E for all closed substitutions oe. Milner [41] introduced a technique to derive !-completeness of an axiomatization using SOS. The idea is to give a semantics to open (as opposed to closed) terms; in particular, variables need to be incorporated in the transition rules. See, e.g., [1, 29] for further applications of this technique in the realm of process algebra. The next theorem can be used to derive that an axiomatization is !- complete. Theorem 4.7 Let , be an equivalence relation on (\Sigma ). Suppose that for all t; u 2 (\Sigma ), t , u whenever oe(t) , oe(u) for all closed substitutions oe. IfE is an axiomatization over \Sigma such that 1. E is sound over T(\Sigma ) modulo ,, and 2. E is complete over (\Sigma ) modulo ,, then E is !-complete. 14 The idea behind Thm. 4.7 is as follows. Let t; u 2 (\Sigma ) and suppose that oe(t) = oe(u) can be derived from E for all closed substitutions oe. Soundness of E over T(\Sigma ) modulo , (requirement 1) yields oe(t) , oe(u) for all closed substitutions oe, so t , u. Then completeness of E over (\Sigma ) modulo , (requirement 2) yields that t = u can be derived from E. Assume a TSS T0 over a signature \Sigma , and let T0 be extended with a TSS T1 that provides semantics to variables; thus, T0 \Phi T1 gives semantics to open terms in (\Sigma ). Suppose that T0 \Phi T1 is an operational conservative extension of T0. Moreover, let , be an equivalence relation on states in LTSs. Since the states in the LTSs associated with T0 and T0 \Phi T1 are closed and open terms, respectively, the equivalence relation , carries over to T(\Sigma 0) and (\Sigma 0). Owing to operational conservativity, the equivalence relation , on T(\Sigma 0) as induced by T0 agrees with this equivalence relation on T(\Sigma 0) as induced by T0 \Phi T1. Applications of Thm. 4.7 in process algebra are abundant in the literature; we give a typical example. Example: Extend the TSS for BPAffl(Act) in Table 1 by letting the symbol a range not only over Act, but also over Var. In a sense this means that variables are considered to be constants. This extension is operationally conservative, which follows from Thm. 3.4 by the following facts:ffl the transition rules for BPAffl(Act) are source-dependent; ffl the sources of transition rules z z! ffl for variables z are fresh; ffl each transition rule for alternative or sequential composition with ztransitions, such as x z! x0 x + y z! x0 contains a premise with the fresh relation symbol z! and as left-hand side a variable from the source. Furthermore, the following properties can be derived for the axiomatizationE of BPAffl(Act) in [50]: 1. E is sound over BPAffl(Act) modulo bisimulation equivalence; 2. open terms t and u in BPAffl(Act) are bisimilar whenever oe(t) and oe(u) are bisimilar for all closed substitutions oe; 3. E is complete over the open terms in BPAffl(Act) modulo bisimulation. So Thm. 4.7 implies that E is !-complete over BPAffl(Act) modulo bisimulation equivalence. \Lambda 15 5 Applications to Rewriting This section discusses how operational conservative extension can be used to derive that an extension of a conditional term rewriting system is so-called rewrite conservative, or that a conditional term rewriting system is ground confluent. 5.1 Rewrite Conservative Extension Definition 5.1 Assume a signature \Sigma . A conditional term rewriting system (CTRS) [4, 13] over \Sigma consists of a collection of rewrite rules t0 ! u0 ( t1 !\Lambda u1; : : : ; tn !\Lambda un with ti; ui 2 (\Sigma ) for i = 0; : : : ; n. Intuitively, a rewrite rule is a directed axiom that can only be applied from left to right. A CTRS induces a binary rewrite relation !\Lambda on terms, similar to the way that an axiomatization induces an equality relation on terms (the only difference is that the rewrite relation is not closed under symmetry), thus: ffl if t0 ! u0 ( t1 !\Lambda u1; : : : ; tn !\Lambda un is a rewrite rule, and oe a substitution such that oe(ti) !\Lambda oe(ui) for i = 1; : : : ; n, then oe(t0) !\Lambda oe(u0); ffl the relation !\Lambda is closed under reflexivity and transitivity; ffl if f is a function symbol and u !\Lambda u0, then f (t1; : : : ; ti\Gamma 1; u; ti+1; : : : ; tar(f)) !\Lambda f (t1; : : : ; ti\Gamma 1; u0; ti+1; : : : ; tar(f)): The definition of sum of TSSs (cf. Def. 3.1) applies equally well to CTRSs. Definition 5.2 Let R0 and R1 be CTRSs over signatures \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively. R0 \Phi R1 is a rewrite conservative extension of R0 if every rewrite relation t !\Lambda u with t 2 T(\Sigma 0) that can be derived from R0 \Phi R1 can also be derived from R0. The conservative extension theorem for TSSs, Thm. 3.4, applies to CTRSs just as well; see [26] for more details. Note that the definition of sourcedependent variables in transition rules, Def. 3.3, also applies to rewrite rules (where, in a rewrite rule t0 ! u0 ( t1 !\Lambda u1; : : : ; tn !\Lambda un, the expression t0 ! u0 is the conclusion and the ti !\Lambda ui for i = 1; : : : ; n are the premises). 16 Theorem 5.3 Let R0 and R1 be CTRSs over signatures \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively. Under the following conditions, R0 \Phi R1 is a rewrite conservative extension of R0. 1. Each ae 2 R0 is source-dependent. 2. For each ae 2 T1, ffl either the source of ae is fresh,ffl or ae has a premise of the form t ! t0 where: - t 2 (\Sigma 0); - all variables in t occur in the source of ae; - t0 is fresh. 5.2 Ground Confluence of CTRSs Definition 5.4 A CTRS is ground confluent if for all t; t0; t1 2 T(\Sigma ) with t !\Lambda t0 and t !\Lambda t1 there is a u 2 T(\Sigma ) with t0 !\Lambda u and t1 !\Lambda u. Ground confluence is an important property, for instance, to prove that an axiomatization is complete modulo some behavioural equivalence relation. The next theorem from [49] can be used to derive that a CTRS is ground confluent. We say that a CTRS R is sound modulo an equivalence relation, on T(\Sigma ) if t !\Lambda u implies t , u for all t; u 2 T(\Sigma ). Theorem 5.5 Let , be an equivalence relation on T(\Sigma 0 \Phi \Sigma 1). Assume CTRSs R0 and R1 over \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively, such that: 1. R0 \Phi R1 is sound over T(\Sigma 0 \Phi \Sigma 1) modulo ,; 2. if t; t0 2 T(\Sigma 0) with t , t0, then there is a u 2 T(\Sigma 0) such that t !\Lambda u and t0 !\Lambda u can be derived from R0; 3. for each t 2 T(\Sigma 0 \Phi \Sigma 1) there is a t0 2 T(\Sigma 0) such that t !\Lambda t0 can be derived from R0 \Phi R1. Then R0 \Phi R1 is ground confluent over T(\Sigma 0 \Phi \Sigma 1). The idea behind Thm. 5.5 is as follows. Let t 2 T(\Sigma 0 \Phi \Sigma 1) such that t !\Lambda t0 and t !\Lambda t1 can be derived from R0 \Phi R1. There exist t00; t01 2 T(\Sigma 0) such that t0 !\Lambda t00 and t1 !\Lambda t01 can be derived from R0 \Phi R1 (requirement 3). Soundness of R0 \Phi R1 (requirement 1) yields t , t0 , t00 and t , t1 , t01, 17 so t00 , t01. Then there exists a u 2 T(\Sigma 0) such that t00 !\Lambda u and t01 !\Lambda u (requirement 2). Hence, t0 !\Lambda u and t1 !\Lambda u. Thm. 5.5 is particularly helpful in the case of an operational conservative extension of a TSS. Assume TSSs T0 and T1 over signatures \Sigma 0 and \Sigma 0 \Phi \Sigma 1, respectively, where T0 \Phi T1 is an operational conservative extension of T0. Moreover, let , be an equivalence relation on states in LTSs. Since the states in the LTSs associated with T0 and T0 \Phi T1 are closed terms, the equivalence relation , carries over to T(\Sigma 0) and T(\Sigma 0 \Phi \Sigma 1), respectively. Owing to operational conservativity, the equivalence relation , on T(\Sigma 0) as induced by T0 agrees with this equivalence relation on T(\Sigma 0) as induced by T0 \Phi T1. Applications of Thm. 5.5, in the presence of an operational conservative extension of a TSS, are abundant in the literature; we give a typical example. Example: Using Thm. 3.4 it is not hard to see that the process algebra ACP [12] is an operational conservative extension of BPAffi. Bergstra and Klop presented in op. cit. an (unconditional) CTRS R0\Phi R1 for the process algebra ACP, which reduces each closed term in ACP to a closed term in BPAffi. Moreover, R0 \Phi R1 is sound over ACP modulo bisimulation equivalence, and it is easily shown that R0 can reduce bisimilar closed terms in BPAffi to the same closed term in BPAffi. Hence, Thm. 4.4 says that R0 \Phi R1 is ground confluent. (In [12, p. 122], an analysis of about 400 cases was needed to prove this fact for the more general case of open terms.) \Lambda 6 Conclusion Operational conservativity of an extension of a TSS can in general be concluded in a straightforward fashion from the syntactic form of the transition rules. Operational conservative extension seems such a natural notion that in the literature this property is often a hidden assumption: its formulation and proof are omitted without justification. For example, this happens in the design of process algebras, and in applications of the strategy to prove !-completeness mentioned in Sect. 4.3. Paying attention to operational conservative extension not only leads to more accurate contemplations on concurrency theory, but is also beneficial in other respects. Namely, operational conservative extension can be applied to derive useful results in the realm of equational reasoning, which are much harder to obtain using more classical term rewriting approaches or customized techniques. 18 References [1] L. Aceto, W. Fokkink, R. van Glabbeek, and A. Ing'olfsd'ottir, Axiomatizing prefix iteration with silent steps, Information and Computation, 127 (1996), pp. 26-40. [2] L. Aceto, W. Fokkink, and C. Verhoef, Structural operational semantics, in Handbook of Process Algebra, J. Bergstra, A. Ponse, and S. Smolka, eds., Elsevier, 1999. To appear. [3] L. Aceto and M. Hennessy, Termination, deadlock and divergence, J. Assoc. Comput. Mach., 39 (1992), pp. 147-187. [4] F. Baader and T. Nipkow, Term Rewriting and All That, Cambridge University Press, 1998. [5] J. Backus, The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM conference, in Proceedings ICIP, Unesco, 1960, pp. 125-131. [6] J. Baeten and J. Bergstra, Discrete time process algebra, in Cleaveland [20], pp. 401-420. [7] J. Baeten, J. Bergstra, and J. W. Klop, Syntax and defining equations for an interrupt mechanism in process algebra, Fundamenta Informaticae, IX (1986), pp. 127-168. [8] J. Baeten and J. W. Klop, eds., Proceedings 1st Conference on Concurrency Theory, Amsterdam, The Netherlands, vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990. [9] J. Baeten and C. Verhoef, A congruence theorem for structured operational semantics with predicates, in Best [15], pp. 477-492. [10] , Concrete process algebra, in Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T. Maibaum, eds., vol. IV, Oxford University Press, 1995, pp. 149-268. [11] J. Baeten and P. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990. [12] J. Bergstra and J. W. Klop, Process algebra for synchronous communication, Information and Control, 60 (1984), pp. 109-137. 19 [13] , Conditional rewrite rules: Confluence and termination, J. Comput. System Sci., 32 (1986), pp. 323-362. [14] J. Bergstra, A. Ponse, and J. van Wamel, Process algebra with backtracking, in Proceedings REX School/Symposium on A Decade of Concurrency: Reflections and Perspectives, Noordwijkerhout, The Netherlands, J. de Bakker, W. d. Roever, and G. Rozenberg, eds., vol. 803 of Lecture Notes in Computer Science, Springer-Verlag, 1994, pp. 46-91. [15] E. Best, ed., Proceedings 4th Conference on Concurrency Theory, Hildesheim, Germany, vol. 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993. [16] B. Bloom, S. Istrail, and A. Meyer, Bisimulation can't be traced: preliminary report, in Conference Record 15th ACM Symposium on Principles of Programming Languages, San Diego, California, 1988, pp. 229-239. Preliminary version of [17]. [17] , Bisimulation can't be traced, J. Assoc. Comput. Mach., 42 (1995), pp. 232-268. [18] R. Bol and J. F. Groote, The meaning of negative premises in transition system specifications, J. Assoc. Comput. Mach., 43 (1996), pp. 863-914. [19] T. Bolognesi and F. Lucidi, Timed process algebras with urgent interactions and a unique powerful binary operator, in Proceedings REX Workshop on Real-Time: Theory in Practice, Mook, The Netherlands, June 1991, J. de Bakker, C. Huizing, W. d. Roever, and G. Rozenberg, eds., vol. 600 of Lecture Notes in Computer Science, Springer-Verlag, 1992, pp. 124-148. [20] R. Cleaveland, ed., Proceedings 3rd Conference on Concurrency Theory, Stony Brook, NY, vol. 630 of Lecture Notes in Computer Science, Springer-Verlag, 1992. [21] R. Cleaveland and M. Hennessy, Priorities in process algebras, Information and Computation, 87 (1990), pp. 58-77. [22] P. D'Argenio, A general conservative extension theorem in process algebras with inequalities, in Proceedings 2nd Workshop on the Algebra of Communicating Processes, Eindhoven, The Netherlands, A. Ponse, 20 C. Verhoef, and B. van Vlijmen, eds., Report CS-95-14, Eindhoven University of Technology, 1995, pp. 67-79. [23] P. D'Argenio and C. Verhoef, A general conservative extension theorem in process algebras with inequalities, Theoretical Comput. Sci., 177 (1997), pp. 351-380. [24] W. Fokkink and R. van Glabbeek, Ntyft/ntyxt rules reduce to ntree rules, Information and Computation, 126 (1996), pp. 1-10. [25] W. Fokkink and C. Verhoef, A conservative look at operational semantics with variable binding, Information and Computation, 146 (1998), pp. 24-54. [26] , Conservative extension in positive/negative conditional term rewriting with applications to software renovation factories, in Proceedings 2nd Conference on Fundamental Approaches to Software Engineering, Amsterdam, The Netherlands, J.-P. Finance, ed., vol. 1577 of Lecture Notes in Computer Science, Springer-Verlag, 1999, pp. 98-113. [27] A. van Gelder, K. Ross, and J. Schlipf, The well-founded semantics for general logic programs, J. Assoc. Comput. Mach., 38 (1991), pp. 620-650. [28] R. van Glabbeek, The linear time - branching time spectrum, in Baeten and Klop [8], pp. 278-297. [29] , A complete axiomatization for branching bisimulation congruence of finite-state behaviours, in Proceedings 18th Symposium on Mathematical Foundations of Computer Science 1993, Gdansk, Poland, A. Borzyszkowski and S. Sokolowski, eds., vol. 711 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 473-484. [30] , Full abstraction in structural operational semantics (extended abstract), in Proceedings 3rd Conference on Algebraic Methodology and Software Technology, Enschede, The Netherlands, M. Nivat, C. Rattray, T. Rus, and G. Scollo, eds., Workshops in Computing, Springer-Verlag, 1993, pp. 77-84. [31] , The meaning of negative premises in transition system specifications II, in Automata, Languages and Programming, 23rd Colloquium, F. Meyer auf der Heide and B. Monien, eds., vol. 1099 of Lecture Notes in Computer Science, Paderborn, Germany, 1996, SpringerVerlag, pp. 502-513. 21 [32] , The meaning of negative premises in transition system specifications II, Report STAN-CS-TN-95-16, Department of Computer Science, Stanford University, 1996. [33] J. F. Groote, Transition system specifications with negative premises, Theoretical Comput. Sci., 118 (1993), pp. 263-299. [34] J. F. Groote and F. Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation, 100 (1992), pp. 202-260. [35] M. Hennessy and T. Regan, A process algebra for timed systems, Information and Computation, 117 (1995), pp. 221-239. [36] R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371-384. [37] S. Klusener, Completeness in real time process algebra, in Proceedings 2nd Conference on Concurrency Theory, Amsterdam, The Netherlands, J. Baeten and J. F. Groote, eds., vol. 527 of Lecture Notes in Computer Science, Springer-Verlag, 1991, pp. 376-392. [38] K. G. Larsen, Modal specifications, Tech. Rep. R 89-09, Institute for Electronic Systems, University of Aalborg, 1989. [39] K. G. Larsen and A. Skou, Compositional verification of probabilistic processes, in Cleaveland [20], pp. 456-471. [40] R. Milner, Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989. [41] , A complete axiomatisation for observational congruence of finitestate behaviors, Information and Computation, 81 (1989), pp. 227-247. [42] F. Moller and C. Tofts, A temporal calculus of communicating systems, in Baeten and Klop [8], pp. 401-415. [43] X. Nicollin and J. Sifakis, The algebra of timed processes, ATP: theory and application, Information and Computation, 114 (1994), pp. 131-178. [44] G. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981. 22 [45] T. Przymusinski, On the declarative semantics of deductive databases and logic programs, in Foundations of Deductive Databases and Logic Programming, J. Minker, ed., Morgan Kaufmann Publishers, Inc., Los Altos, California, 1988, pp. 193-216. [46] , The well-founded semantics coincides with the three-valued stable semantics, Fundamenta Informaticae, 13 (1990), pp. 445-463. [47] A. Roscoe, The Theory and Practice of Concurrency, Prentice-Hall International, 1998. [48] R. de Simone, Calculabilit'e et Expressivit'e dans l'Algebra de Processus Parall`eles Meije, th`ese de 3e cycle, Univ. Paris 7, 1984. [49] C. Verhoef, A general conservative extension theorem in process algebra, in Proceedings IFIP Working Conference on Programming Concepts, Methods and Calculi, San Miniato, Italy, E.-R. Olderog, ed., IFIP Transactions A-56, Elsevier, 1994, pp. 149-168. [50] J. Vrancken, The algebra of communicating processes with empty process, Theoretical Comput. Sci., 177 (1997), pp. 287-328. 23