C. Verhoef
Department of Mathematics and Computing
Science, Eindhoven University of Technology,
P.O. Box 513, NL-5600 MB Eindhoven, The Netherlands
email chrisv@win.tue.nl
[+]
NOTE: Since this document contains loads of formulas that cannot be processed with a tex to html facility please find a PS file of this document on my SOS page.
We prove a general conservative extension theorem for transition system based process theories with easy-to-check and reasonable conditions. The core of this result is another general theorem giving sufficient conditions for a system of operational rules and an extension ensuring that provable transitions from an original term in the extension are the same as in the original system. As a simple corollary of the conservative extension theorem we prove a completeness theorem. As a first application of our conservativity results, we prove a general theorem giving sufficient conditions to reduce the question of ground confluence modulo some equations for a large term rewriting system associated with an equational process theory to a small term rewriting system under the condition that the large system is a conservative extension of the small one. We provide many other applications to show that our results are useful. The applications include (but are not limited to) various real and discrete time settings in CCS, ACP, and ATP and the notions projection, renaming, state operator, priority, recursion, the silent step (both the weak and branching variants), and the empty process (or combinations of these notions).
Keyword Codes: F.1.2, F.3.2, F.4.3.
Keywords: Concurrency; Operational Semantics; Algebraic language theory.
A frequently used method to prove that an equational theory is a conservative extension of a subtheory is to perform a term rewriting analysis. In process algebra such an analysis is often very complex because the rewriting system associated with a process algebra seems to need in an essential way term rewriting techniques modulo the equations without a clear direction (such as commutativity of the choice). Moreover, these term rewriting systems generally have no ``nice'' properties making a term rewriting analysis a simple tool for conservativity. We mention that such term rewriting systems are not regular, which implies that confluence (modulo some equations) is not straightforward and we mention that the term rewriting relation induced by the rewrite rules is not commuting with the equality induced by the equations without a direction, which means that termination modulo these equations is not at all easy to prove. Let us briefly mention two examples to make the problems a bit more concrete. Bergstra and Klop [2] mention that for the confluence modulo some equations of their term rewriting system, they need to check [IMAGE ] cases (which they left to the reader as an exercise). Jouannaud communicated to us that, 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 [3]. They show that a fragment of ACP with the branching [IMAGE ] is both terminating and confluent modulo associativity and commutativity of the alternative 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 problem to establish these results; needless to say that their term rewriting analysis is rather complicated.
To bypass the abovementioned problems involving term rewriting, we propose an alternative method to prove conservativity. We prove a general theorem with reasonable and easy-to-check conditions giving us immediately the operational and equational conservativity in many cases. For instance, with our results, the conservativity of the above mentioned systems with problematic term rewriting properties is peanuts. The idea is that we transfer the question of equational conservativity to that of operational conservativity rather than to perform a term rewriting analysis. The only thing that remains to be done in order to prove the operational conservativity is to check our simple conditions for the operational rules. For the equational conservativity we moreover demand completeness for the subtheory and soundness for its extension. These conditions are in our opinion reasonable, because relations between equational theories only become important if the theories themselves satisfy well-established basic requirements. Moreover, our result works for a large class of theories, which is certainly not the case with a term rewriting analysis. All this implies that we give a semantical proof of conservativity, which might be seen as a drawback since a term rewriting analysis often is model independent (but see Bergstra and Klop [4] for a semantical term rewriting analysis). However, since the paper of Plotkin [5], the use of labelled transition systems as a model for operational semantics of process theories is widespread; so virtually every process theory has an operational semantics of this kind. Moreover, our equational conservativity result holds for all semantical equivalences that are definable exclusively in terms of transition relations. We recall that the following semantical equivalences are examples of such equivalences: trace equivalence, completed trace equivalence, failure equivalence, readiness equivalence, failure trace equivalence, ready trace equivalence, possible-future equivalence, simulation equivalence, complete simulation equivalence, ready simulation equivalence, nested simulation equivalence, strong bisimulation equivalence, weak bisimulation equivalence, [IMAGE ] bisimulation equivalence, delay bisimulation equivalence, branching bisimulation equivalence, and more equivalences. We refer to Van Glabbeek's linear time - branching time spectra [6] and [7] for more information on these equivalences. In [6] and [7], references to the origins (and their use) of these semantics can be found.
As a result we now can prove conservativity without using the confluence property. However, it is widely recognized that confluence itself is an important property, for instance, for computational or implementational purposes. So, at this point the question arises: ``Why bother about such a general conservative extension theorem if we still have to prove confluence for each particular system and get the conservativity as a by-product?'' The answer is that once we have the conservativity we can considerably reduce the complexity of the ground confluence as a by-product. We prove a general reduction theorem stating that in many cases a conservative extension is ground Church-Rosser modulo some equations if the basic system already has this property. For instance, the 400 cases of Bergstra and Klop [2] reduce to a term rewriting analysis with only five rewrite rules and two equations. We should note, however, 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 in their situation. In fact, we show that conservativity and ground Church-Rosser are, in some sense, equally expressive properties.
Another advantage of our approach is that it also works for process algebras with really bad term rewriting properties, such as process algebras containing the three [IMAGE ] laws of Milner, where the term rewriting approach breaks down; see, e.g., [4]. We will treat these examples in this paper.
Now that we have given some motivation for this paper we discuss its organization.
In section 2 we recall some general SOS definitions of Verhoef [8]. We will provide a running example to elucidate the abstract notions. In section 3 we formally define the notions of operational and equational conservativity. Then we prove a general operational conservativity theorem, a general equational conservativity theorem and a simple corollary concerning completeness. Also here we provide our running example. In the next section we will recall some basic term rewriting terminology to prove the abovementioned reduction theorem on the ground Church-Rosser property modulo some equations. In section 5 we will give the reader an idea of the applicability of our general theorems. Surprisingly, we could not find any conservativity result in the literature for which our conservativity theorem could not be applied, as well. The last section contains concluding remarks and briefly discusses possible future work.
In this subsection we briefly mention related work. Nicollin and Sifakis [9] prove conservativity--in some particular cases--using the same general approach as we propose in this paper, namely a semantical approach. We will discuss their conservativity results (and new results) in section 5. The notion that we call in this paper operational conservativity originates from Groote and Vaandrager [1] under the name conservativity. In Groote [10] and in Bol and Groote [11] this notion also appears. In all these papers this notion is used for a different purpose than ours. Aceto, Bloom and Vaandrager [12] introduce a so-called disjoint extension, which is a more restricted form of an operational conservative extension; they need this restriction for technical reasons. They present an algorithm generating a sound and complete axiomatization if the operational rules satisfy certain criteria. Bosscher [13] studied term rewriting properties of such axiomatizations by looking at the form of the operational rules.
We assume that we have an infinite set V of variables with typical elements [IMAGE ]. A (single sorted) signature [IMAGE ] is a set of function symbols together with their arity. If the arity of a function symbol [IMAGE ] is zero we say that f is a constant symbol. The notion of a term (over [IMAGE ]) is defined as expected: [IMAGE ] is a term; if [IMAGE ] are terms and if [IMAGE ] is n-ary then [IMAGE ] is a term. A term is also called an open term; if it contains no variables we call it closed. We denote the set of closed terms by [IMAGE ] and the set of (open) terms by [IMAGE ]. We also want to speak about variables occurring in terms: let [IMAGE ] then [IMAGE ] is the set of variables occurring in t.
A substitution [IMAGE ] 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 substituting for each variable occurring in an open term its [IMAGE ]-image.
BPA with discrete time.
Next, we formally define the notion of an operational conservative extension and the notion of an operational conservative extension up to some semantical equivalence which is defined exclusively in terms of predicate and relation symbols. The notions operational conservative extension and operational conservative extension up to strong bisimulation equivalence were already defined by Groote and Vaandrager [1] (without the adjective `operational') where they used the first notion to characterize the completed trace congruence induced by their pure well-founded tyft /tyxt format. Groote [10] gives the two definitions in the case that negative premises come into play. He used operational conservativity for a similar characterization result as in [1]. In Bol and Groote [11] the approach of Groote [10] is placed in a wider perspective. Aceto, Bloom and Vaandrager [12] use a restricted form of operational conservative extension for technical reasons; they call it disjoint extension. We will use the notion of operational conservativity to prove equational conservativity.
The next theorem gives sufficient conditions such that [IMAGE ] is an operational conservative extension of [IMAGE ]. The theorem is a threefold generalization of a similar result for Groote's ntyft /ntyxt format [10]. Firstly, because we prove it for the panth format, which is a generalization of the ntyft /ntyxt format. Secondly, since we allow new rules to contain original function symbols in the left-hand side of a conclusion such as, for instance, the last four rules in table 1 of our running example. This is not allowed in the setting of Groote. Thirdly, since Groote requires for the new rules that the left-hand side of a conclusion may not be a single variable, whereas we do not have such a restriction. The first such theorem was formulated in Groote and Vaandrager [1].
We devote the remainder of this section to equational conservativity. We recall that an equational specification is a pair consisting of a signature and a set of equations over this signature.
Next, we recall the well-known definition of conservativity.
[IMAGE ]
Table: The axioms of BPA and DT.
As a first application of our conservativity results we prove a general reduction theorem stating that in many cases checking the Church-Rosser property for closed terms modulo some equations for a large system reduces to verifying this property for a small basic system. Of course, provided that the large system is an equational conservative extension of the small system. From a term rewriting point of view this condition is not realistic since usually you need the Church-Rosser property for closed terms to obtain conservativity. However, in many cases we can prove the conservativity without a term rewriting analysis. Thus, we could argue that conservativity and ground confluence are equally powerful properties, so to speak.
Moller and Tofts [20] discuss an extension of CCS with time: TCCS. Their approach is an operational one, that is, they add operational rules to the well-known operational rules of CCS to define new operators and to extend the meaning of existing operators. With our operational conservativity result it is easily seen that TCCS is an operational conservative extension of CCS. An interesting matter is that Moller and Tofts take for their equational approach a small sublanguage of TCCS, which is a mixture of timed and untimed operators. In fact, they took a small one which is sound and complete with respect to the operational rules such that extensions of this sublanguage have the elimination property, thereby reducing the completeness to the sublanguage. They use a variant of strong bisimulation equivalence, which is definable in terms of transition relations (and predicates) only. So, their extensions are easily seen to be conservative with our theorems. Our operational conservative extension theorem is a useful tool to systematically find such small sublanguages such that their extensions are conservative.
The approach in ACP and ATP is more axiomatical. This is no obstacle for our results: we can also handle this approach in a satisfactory way. Within the ACP community there is a long tradition with conservativity results, completeness results and confluence results. Also in ATP\ there are many conservativity and completeness results. We will simultaneously treat numerous examples from both ACP and ATP\ with the aid of figure 1. And we will treat some typical cases more elaborately. We note that the examples in figure 1 contain both known results and new results.
In the introduction we mentioned the problems concerning the confluence of ACP that Bergstra and Klop [2] used to prove conservativity. We claimed that with our theorems it is very easy to see that the conservativity result holds. Therefore, we elaborately treat the [IMAGE ]-labelled arrow from ACP to _[IMAGE ] in figure 1. We show that all our general results apply to this arrow.
Van Glabbeek [21] gives an operational semantics for Bergstra and Klop's ACP [2] and for their sequential subsystem _[IMAGE ] [2]. With our operational result 3.9 it is easily seen that the large semantics is an operational conservative extension of the small one. Baeten and Weijland [18], for instance, show that _[IMAGE ] is 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 termination predicates, which is definable in terms of transition relations and predicates only. So, our equational result 3.14 immediately implies that ACP is an equational conservative extension of _[IMAGE ]. Since ACP has the elimination property we also find the completeness of ACP with theorem 3.14. Moreover, with our reduction theorem 4.7 we have that the question whether or not ACP is ground Church-Rosser modulo associativity and commutativity of the choice (CR /AC [IMAGE ]) reduces to this question for _[IMAGE ]. The associated term rewriting system of _[IMAGE ] consists of five rewrite rules and two equations, which is a considerable reduction since the term rewriting system for ACP has many more rules.
[IMAGE ]
Figure 1: Some applications.
Now, we discuss figure 1. An arrow [IMAGE ] 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. We will explain the abbreviations that we did not met yet. The abbreviation PA stands for process algebra and this system originates from Bergstra and Klop [22]. The acronym ASP stands for the algebra of sequential processes. This system stems from Milner [23]. The x,y,u and v stand for variables; we use them to treat many examples at the same time.
We begin with the variables x and y; they are present in the ACP-side of figure 1.
Let x=y. And let x be one of PR, RN, [IMAGE ], [IMAGE ], [IMAGE ], or a combination of them. The abbreviations stand for projections, renamings, simple state operators, extended state operators, and the priority operator respectively. A concise reference to these notions, their operational rules, their axiomatizations, and their associated term rewriting systems is the text book of Baeten and Weijland [18]. The variant of bisimulation that is used in these applications is definable in terms of transition relations and predicates exclusively. So, for all these cases we have that all arrows of the ACP side of the picture hold: operational and equational conservativity. Moreover, all these extensions have the elimination property for either the complete BPA or the complete _[IMAGE ] (if the extension contains already a [IMAGE ]); for full proofs see, for instance, [18]. So we find for all these extensions the completeness with our corollary. Moreover, the ground confluence modulo AC for these systems reduces to the ground confluence modulo AC for either BPA or _[IMAGE ].
Now, let x=y and let x be one of rec, dt, or a combination of those (note that we can also combine rec with the already treated notions). The abbreviations stand for recursion and discrete time [15], respectively. Also for these systems we have that all arrows hold. Note that [IMAGE ] was our running example. We do not have the elimination property for subscripted systems to systems without a subscript (for instance [IMAGE ] cannot be written as a BPA term). For the other arrows we have the elimination property [15], so from the completeness of [IMAGE ] we conclude the completeness for all the extensions. The ground confluence of these systems has not yet been studied but with our reduction theorem is it only necessary to study the ground confluence for the [IMAGE ] systems.
Now, let x=y and let x be Milner's silent action [IMAGE ]. We already mentioned in the introduction that systems containing the three [IMAGE ] laws of Milner have in general bad rewriting properties. The conservativity of [IMAGE ] over ACP was proved semantically by Bergstra and Klop [4] since the second and third [IMAGE ] law have no clear term rewriting direction. Next, we will show that our approach also works in cases where the established method breaks down. In fact, we immediately find this result. The operational semantics of [IMAGE ]\ is just the one of ACP but now a ranges also over [IMAGE ] itself. It is easy to see that the conditions of theorem 3.9 are satisfied, so [IMAGE ] is an operational conservative extension of ACP. Now with theorem 3.8 we find that [IMAGE ] is an operational conservative extension up to rooted [IMAGE ] bisimulation equivalence of ACP. We should note that the definition of (rooted) [IMAGE ] bisimulation equivalence in the presence of the predicates [IMAGE ]a[IMAGE ] as given by Baeten and Weijland [18] is wrong, since the first [IMAGE ] law of Milner is not sound. This can be easily repaired. Since ACP is sound and complete and since [IMAGE ] is sound with respect to this equivalence, we find with theorem 3.14 that [IMAGE ]\ is an equational conservative extension of ACP. All the other arrows in our figure go likewise. Since all the extensions have the elimination property for [IMAGE ], we find their completeness with the aid of the completeness of [IMAGE ]. The systems have bad term rewriting properties so the ground confluence results does not apply.
We mentioned in the introduction the rather complicated term rewriting analysis of Akkerman and Baeten [3] of a fragment of ACP with the branching [IMAGE ]. We will show in a moment that our results can be easily applied to this case. With the aid of theorem 3.8 we find that [IMAGE ]\ is an operational conservative extension up to branching bisimulation equivalence [24] of ACP. Also in this case we note that the definition of branching bisimulation equivalence in the presence of the predicates [IMAGE ]a[IMAGE ] as given by Baeten and Weijland [18] is wrong, since the first [IMAGE ] law of Milner is not sound. Having repaired this definition, we find in the same way as above that ACP\ with the branching [IMAGE ] axioms [24], denoted [IMAGE ], is an equational conservative extension of ACP. The same holds for all the other arrows in our figure. Since all the extensions have the elimination property for [IMAGE ] we find the completeness for them with the completeness of [IMAGE ]. The branching [IMAGE ] axioms have better term rewriting properties [3] than the [IMAGE ] laws of Milner (that we discussed above). So our ground confluence result may be useful, as well.
Let x=y be the empty process [IMAGE ] of Koymans and Vrancken [17]; see also Vrancken [25]. We can show operational and equational conservativity for all arrows from a system with an [IMAGE ] to a subsystem also featuring this [IMAGE ] by using the operational semantics that can be found in Baeten and Weijland's text book [18]. In [18] we also find that these systems have the elimination property, so also our completeness and the ground confluence results apply. For the remaining arrows we have to follow a different approach. The operational semantics in [18] features the rule [IMAGE ] so we can never have that this semantics is an operational conservative extension of a semantics without [IMAGE ] (but containing a). For, there is no [IMAGE ] in the subsystem. The solution to this problem is to take another operational semantics that is easily obtained by ``upgrading'' the complete graph model of Koymans and Vrancken [17]. In fact, this operational semantics is that of the subsystem where we include [IMAGE ] as a normal atomic action. So we have, for instance, [IMAGE ]a[IMAGE ]. The special behaviour of the empty process is expressed with the aid of so-called [IMAGE ] bisimulation equivalence of Koymans and Vrancken [17]. Also this definition needs a straightforward upgrade from graphs to transitions (and is definable in terms of transition relations and predicates only). In this way we find the operational and equational conservativity. Since we cannot eliminate the empty process, we cannot apply our completeness corollary and the ground confluence result for these particular systems.
Let x be [IMAGE ] standing for absolute real time [26]. Then the x-arrow in the figure holds. To obtain this result we take the operational semantics of Klusener [27]. Also here we have the elimination property, so our completeness and ground confluence results apply, too.
Now we treat the ATP-side of figure 1. Nicollin and Sifakis [9] studied a timed process algebra called ATP\ with various extensions and restrictions of which the most restricted timed one is ASTP, the algebra of sequential timed processes. Milner's [23] algebra of sequential processes ASP--the untimed version of ASTP--is the most restricted system. The interesting thing here is that they prove some conservativity results with the same strategy as ours: they show that the extensions are operationally conservative up to bisimulation by looking at the transition rules and then conclude the equational conservativity. Our figure intends to show that every possible extension that can be obtained with the so-called delay operators of Nicollin and Sifakis [9] is conservative. However, we should note that we treat recursion as in Groote and Vaandrager [1] to fit the operational semantics in their tyft /tyxt format--and thus Verhoef's panth format--in order to obtain that all our conditions are satisfied. This is not a serious drawback but just an equivalent treatment of recursion. There are four delay operators present in [9]: start delay, unbounded start delay, execution delay, and termination 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 any combination of delay operators. If u does not contain all delay operators yet we can take for v the operators of u and a new one, or if the execution delay operator is in u we can take the termination delay operator in v and we do not necessarily need an extra delay operator for a non-trivial extension. Cases like [IMAGE ] and [IMAGE ] are, in our opinion, the most interesting since in these cases not only a new operator (unit delay and [IMAGE ] resp.) is introduced but also an original operator gets a new rule. Since the elimination property holds [9] for ASTP our completeness corollary applies for all the arrows but the two to ASP. The ground confluence of ATP is not yet studied but its study reduces to that of ASTP with our reduction theorem.
Remarkably, we could not find any conservativity results in the literature for which our equational conservativity theorem does not apply, too. So it may be an interesting idea to investigate whether or not the conditions of this theorem are necessary. We think that our conditions are only sufficient but not necessary.
Acknowledgements Thanks to Jos Baeten (Eindhoven University of Technology) for valuable comments and interesting discussions. Thanks to Gertjan Akkerman (Delft University of Technology), Jean-Pierre Jouannaud (LRI Paris), Jan Willem Klop (CWI), and Xavier Nicollin (IMAG France) for their helpful discussions.
![[IMAGE ]](img1.gif){kind=link}
![[IMAGE ]](img2.gif){kind=link}
![[IMAGE ]](img3.gif){kind=link}
![[IMAGE ]](img4.gif){kind=link}
![[IMAGE ]](img5.gif){kind=link}
![[IMAGE ]](img6.gif){kind=link}
![[IMAGE ]](img7.gif){kind=link}
![[IMAGE ]](img8.gif){kind=link}
![[IMAGE ]](img9.gif){kind=link}
![[IMAGE ]](img10.gif){kind=link}
![[IMAGE ]](img11.gif){kind=link}
![[IMAGE ]](img12.gif){kind=link}
![[IMAGE ]](img13.gif){kind=link}
![[IMAGE ]](img14.gif){kind=link}
![[IMAGE ]](img15.gif){kind=link}
![[IMAGE ]](img16.gif){kind=link}
![[IMAGE ]](img17.gif){kind=link}
![[IMAGE ]](img22.gif){kind=link}
![[IMAGE ]](img23.gif){kind=link}
![[IMAGE ]](img24.gif){kind=link}
![[IMAGE ]](img25.gif){kind=link}
![[IMAGE ]](img26.gif){kind=link}
![[IMAGE ]](img27.gif){kind=link}
![[IMAGE ]](img28.gif){kind=link}
![[IMAGE ]](img29.gif){kind=link}
![[IMAGE ]](img30.gif){kind=link}
![[IMAGE ]](img31.gif){kind=link}
![[IMAGE ]](img32.gif){kind=link}
![[IMAGE ]](img33.gif){kind=link}
![[IMAGE ]](img34.gif){kind=link}
![[IMAGE ]](img35.gif){kind=link}
![[IMAGE ]](img36.gif){kind=link}
![[IMAGE ]](img37.gif){kind=link}
![[IMAGE ]](img38.gif){kind=link}
![[IMAGE ]](img39.gif){kind=link}
![[IMAGE ]](img40.gif){kind=link}
![[IMAGE ]](img41.gif){kind=link}
![[IMAGE ]](img42.gif){kind=link}
![[IMAGE ]](img43.gif){kind=link}
![[IMAGE ]](img44.gif){kind=link}
![[IMAGE ]](img45.gif){kind=link}
![[IMAGE ]](img46.gif){kind=link}
![[IMAGE ]](img47.gif){kind=link}
![[IMAGE ]](img48.gif){kind=link}
![[IMAGE ]](img49.gif){kind=link}
![[IMAGE ]](img50.gif){kind=link}
![[IMAGE ]](img52.gif){kind=link}
![[IMAGE ]](img53.gif){kind=link}
![[IMAGE ]](img54.gif){kind=link}
![[IMAGE ]](img55.gif){kind=link}
![[IMAGE ]](img56.gif){kind=link}
![[IMAGE ]](img57.gif){kind=link}
![[IMAGE ]](img58.gif){kind=link}
![[IMAGE ]](img59.gif){kind=link}
![[IMAGE ]](img60.gif){kind=link}
![[IMAGE ]](img61.gif){kind=link}
![[IMAGE ]](img62.gif){kind=link}
![[IMAGE ]](img63.gif){kind=link}
![[IMAGE ]](img64.gif){kind=link}
![[IMAGE ]](img65.gif){kind=link}
![[IMAGE ]](img66.gif){kind=link}
![[IMAGE ]](img67.gif){kind=link}
![[IMAGE ]](img68.gif){kind=link}
![[IMAGE ]](img69.gif){kind=link}
![[IMAGE ]](img70.gif){kind=link}
![[IMAGE ]](img71.gif){kind=link}
![[IMAGE ]](img72.gif){kind=link}
![[IMAGE ]](img73.gif){kind=link}
![[IMAGE ]](img74.gif){kind=link}
![[IMAGE ]](img75.gif){kind=link}
![[IMAGE ]](img76.gif){kind=link}