**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.

1 [IMAGE ]&[IMAGE ]&[IMAGE ] a =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1a[IMAGE ]& =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1x' =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1x'y& =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1a[IMAGE ] =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1y =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1x'+y =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1x' =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1 y+x& =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1a[IMAGE ]+y =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1a[IMAGE ] =1em 0=[IMAGE ] by 0 <16.11119pt =16.11119pt a 1=to 1=0.3em1 y+x& _d(x){ =1em 0=[IMAGE ]

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.

**1**-
J.F. Groote and F.W. Vaandrager.
Structured operational semantics and bisimulation as a congruence.
*Information and Computation*, 100(2):202-260, October 1992. **2**-
J.A. Bergstra and J.W. Klop.
Process algebra for synchronous communication.
*Information and Computation*, 60(1/3):109-137, 1984. **3**-
G.J. Akkerman and J.C.M. Baeten.
Term rewriting analysis in process algebra.
Report P9006, Programming Research Group, University of Amsterdam,
1990.
**4**-
J.A. Bergstra and J.W. Klop.
Algebra of communicating processes with abstraction.
*Theoretical Computer Science*, 37(1):77-121, 1985. **5**-
G.D. Plotkin.
A structural approach to operational semantics.
Report DAIMI FN-19, Computer Science Department, Aarhus University,
1981.
**6**-
R.J. van Glabbeek.
The linear time - branching time spectrum.
In J.C.M. Baeten and J.W. Klop, editors,
*Proceedings CONCUR 90, Amsterdam*, volume 458 of*Lecture Notes in Computer Science*, pages 278-297. Springer-Verlag, 1990. **7**-
R.J. van Glabbeek.
The linear time - branching time spectrum II (extended
abstract).
In
*Proceedings CONCUR 93, Hildesheim, Germany*, volume 715 of*Lecture Notes in Computer Science*, pages 66-81. Springer-Verlag, August 1993. **8**-
C. Verhoef.
A congruence theorem for structured operational semantics with
predicates and negative premises.
Computing Science Notes 93/18, Eindhoven University of Technology,
1993.
To appear in the proceedings of CONCUR 94.
**9**-
X. Nicollin and J. Sifakis.
The algebra of timed processes ATP: Theory and application (revised
version).
Technical Report RT-C26, LGI-IMAG, Grenoble, France, November 1991.
**10**-
J.F. Groote.
Transition system specifications with negative premises.
Report CS-R8950, CWI, Amsterdam, 1989.
An extended abstract appeared in J.C.M. Baeten and J.W. Klop,
editors,
*Proceedings CONCUR 90*, Amsterdam, LNCS 458, pages 332-341. Springer-Verlag, 1990. **11**-
R.N. Bol and J.F. Groote.
The meaning of negative premises in transition system specifications
(extended abstract).
In J. Leach Albert, B. Monien, and M. Rodríguez, editors,
*Proceedings [IMAGE ] ICALP, Madrid*, volume 510 of*Lecture Notes in Computer Science*, pages 481-494. Springer-Verlag, 1991. Full version appeared as Report CS-R9054, CWI, Amsterdam, 1990. **12**-
L. Aceto, B. Bloom, and F.W. Vaandrager.
Turning SOS rules into equations.
In
*Proceedings [IMAGE ] Annual Symposium on Logic in Computer Science, Santa Cruz, California*, pages 113-124. IEEE Computer Society Press, 1992. Full version available as CWI Report CS-R9218, June 1992, Amsterdam. To appear in the LICS 92 Special Issue of*Information and Computation*. **13**-
D.J.B. Bosscher.
Term rewriting properties of SOS axiomatizations.
In Masami Hagiya and John C. Mitchell, editors,
*Theoretical Aspects of Computer Software*, volume 789 of*Lecture Notes in Computer Science*, pages 425-439. Springer-Verlag, 1994. **14**-
A.S. Klusener.
*Models and axioms for a fragment of real time process algebra*. PhD thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, December 1993. **15**-
J.C.M. Baeten and J.A. Bergstra.
Discrete time process algebra.
In W.R. Cleaveland, editor,
*Proceedings CONCUR 92, Stony Brook, NY, USA*, volume 630 of*Lecture Notes in Computer Science*, pages 401-420. Springer-Verlag, 1992. **16**-
B. Bloom, S. Istrail, and A.R. Meyer.
Bisimulation can't be traced: Preliminary report.
In
*Conference Record of the [IMAGE ] ACM Symposium on Principles of Programming Languages, San Diego, California*, pages 229-239, 1988. Full version available as Technical Report 90-1150, Department of Computer Science, Cornell University, Ithaca, New York, August 1990. Accepted to appear in*Journal of the ACM*. **17**-
C.P.J. Koymans and J.L.M. Vrancken.
Extending process algebra with the empty process [IMAGE ].
Logic Group Preprint Series Nr. 1, CIF, State University of Utrecht,
1985.
The State University of Utrecht is now called Utrecht University.
**18**-
J.C.M. Baeten and W.P. Weijland.
*Process Algebra*. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990. **19**-
J.-P. Jouannaud and M. Muñoz.
Termination of a set of rules modulo a set of equations.
In R. E. Shostak, editor,
*7th International Conference on Automated Deduction*, volume 170 of*Lecture Notes in Computer Science*, pages 175-193. Springer-Verlag, 1984. **20**-
F. Moller and C. Tofts.
A temporal calculus of communicating systems.
In J.C.M. Baeten and J.W. Klop, editors,
*Proceedings CONCUR 90, Amsterdam*, volume 458 of*Lecture Notes in Computer Science*, pages 401-415. Springer-Verlag, 1990. **21**-
R.J. van Glabbeek.
Bounded nondeterminism and the approximation induction principle in
process algebra.
In F.J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, editors,
*Proceedings STACS 87*, volume 247 of*Lecture Notes in Computer Science*, pages 336-347. Springer-Verlag, 1987. **22**-
J.A. Bergstra and J.W. Klop.
Fixed point semantics in process algebras.
Report IW 206, Mathematisch Centrum, Amsterdam, 1982.
**23**-
R. Milner.
A complete inference system for a class of regular behaviours.
*Journal of Computer and System Sciences*, 28:439-466, 1984. **24**-
R.J. van Glabbeek and W.P. Weijland.
Branching time and abstraction in bisimulation semantics (extended
abstract).
In G.X. Ritter, editor,
*Information Processing 89*, pages 613-618. North-Holland, 1989. Full version available as Report CS-R9120, CWI, Amsterdam, 1991. **25**-
J.L.M. Vrancken.
*Studies in Process Algebra, Algebraic Specifications and Parallelism*. PhD thesis, University of Amsterdam, April 1991. **26**-
J.C.M. Baeten and J.A. Bergstra.
Real time process algebra.
*Journal of Formal Aspects of Computing Science*, 3(2):142-188, 1991. **27**-
A.S. Klusener.
Completeness in real time process algebra.
In J.C.M. Baeten and J.F. Groote, editors,
*Proceedings CONCUR 91, Amsterdam*, volume 527 of*Lecture Notes in Computer Science*, pages 376-392. Springer-Verlag, 1991.

- ...
`chrisv@win.tue.nl` - Full support received from the European Communities under CONCUR 2, BRA 7166.

Fri Jun 13 14:42:29 MET DST 1997