# Concrete process algebra

J.C.M. Baeten and C. Verhoef

Algebra may be considered, in its most general form, as the science which treats of the combinations of arbitrary signs and symbols by means of defined through arbitrary laws ...[Peackock1830]Peackock, G..

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 ACP page.

1 Introduction Concurrency theory is the branch of computer science that studies the mathematics of concurrent or distributed systems. In concurrency theory, the design of such mathematics is studied and issues concerning the specification and verification of such systems are analysed. Often, a concurrent system is called a process. In order to analyse a large and complex process it is desirable to be able to describe it in terms of smaller and simpler processes. Thus, it seems natural to have some simple processes--the ones that are not subject to further investigation--and operators on them to compose larger ones thus resulting in an algebraic structure. In order to reason about large processes it is often useful to have a set of basic identities between processes at one's disposal. The most relevant identities among them are normally called axioms. The axiomatic and algebraic point of view on concurrency theory is widely known as process algebra.

The most well-known algebraic concurrency theories are the ones known by the acronyms CCS voidCCSCCS : communicating concurrent processes, CSP voidCSPCSP : communicating sequential processes, and ACP voidACPACP : algebra of communicating processes. CCS voidCCSCCS : communicating concurrent processes is the Calculus of Communicating Systems of [Milner1980]Milner, R.. Theoretical CSP voidCSPCSP : communicating sequential processes originates from [Brookes et al. 1984]Brookes, S.D.Hoare, C.A.R.Roscoe, A.W.; the acronym CSP voidCSPCSP : communicating sequential processes stands for Communicating Sequential Processes. ACP voidACPACP : algebra of communicating processes is the Algebra of Communicating Processes; the original reference to ACP voidACPACP : algebra of communicating processes is [Bergstra and Klop1984a]Bergstra, J.A.Klop, J.W.; we note that recently the full version of [Bergstra and Klop1984a]Bergstra, J.A.Klop, J.W. has appeared; see [Bergstra and Klop1995]Bergstra, J.A.Klop, J.W.. Of these three, (theoretical) CSP voidCSPCSP : communicating sequential processes is the most abstract (it identifies more processes than the other two), and tends in the direction of a specification language. The other two, CCS voidCCSCCS : communicating concurrent processes\ and ACP voidACPACP : algebra of communicating processes, are based on the same notion of equivalence (bisimulation equivalence), and are more operationally oriented than CSP voidCSPCSP : communicating sequential processes. They tend in the direction of a programming language. Of the two, CCS voidCCSCCS : communicating concurrent processes has links to logic and [IMAGE ]-calculus, and ACP voidACPACP : algebra of communicating processes may be best characterized as a purely algebraical approach.

In this survey we focus on concrete process algebra. Concrete process algebra is the area of algebraic concurrency theory that does not incorporate a notion called abstraction. Abstraction is the ability to hide information, to abstract information away. The reason that we refrain from incorporating this important issue is that concrete process algebra is already such a large part of the theory that it justifies its own survey. Moreover, it is more and more recognized that for the understanding of issues in large languages it is often convenient first to study such issues in a basic language, a language with less features. For instance, some decidability results in process algebra are obtained in this way. Other examples of such basic languages are Milner's basic CCS voidCCSCCS : communicating concurrent processes\ [Milner1980]Milner, R., BCCSP voidBCCSPBCCSP : basic CCS /CSP [Glabbeek1990]Glabbeek, R.J. van, ASTP voidASTPASTP : algebra of sequential timed processes [Nicollin and Sifakis1994]Nicollin, X.Sifakis, J., TCCS[IMAGE ] voidTCCS0TCCS[IMAGE ] : subsystem of temporal CCS [Moller and Tofts1990]Moller, F.Tofts, C.M.N., BPP voidBPPBPP : basic parallel processes\ [Christensen et al. 1993]Christensen, S.Hirschfeld, Y.Moller, F., and the pair BPA voidBPABPA : basic process algebra/PA voidPAPA : process algebra [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W.. The results that may be obtained for a basic language are almost always useful when the language is extended with additional constructs. Most of the time, these basic languages are concrete. In this survey we will see many examples where a result for a basic language is very useful for an extended version of the language.

Another reason to focus on concrete process algebra is that it is indeed purely algebraically a neat theory. On the other hand, the theory with a form of abstraction and thus with some special constant such as Milner'sMilner, R. silent action ([IMAGE ]voidtau[IMAGE ]: Milner's silent action) or the empty process [IMAGE ] of [Koymans and Vrancken1985]Koymans, C.P.J.Vrancken, J.L.M. is not (yet) stabilized. That is, there are many variants of the theory and it is not clear if there exists a superior variant. For instance, there are two closely related competitive equivalences for the theory with so-called [IMAGE ] abstraction: observational congruence [Milner1980]Milner, R. and branching bisimulation equivalence [Glabbeek and Weijland1989]Glabbeek, R.J. vanWeijland, W.P..

To obtain a uniform notation, since the majority of the available concrete process algebras are ACP voidACPACP : algebra of communicating processes-like ones, and since the ACP voidACPACP : algebra of communicating processes approach is the most algebraical approach, we survey the algebraical part in the ACP voidACPACP : algebra of communicating processes-style process algebra of [Bergstra and Klop1984a, Bergstra and Klop1995]Bergstra, J.A.Klop, J.W.. As for the semantics of the various languages we deviate from the approach of [Bergstra and Klop1984a, Bergstra and Klop1995]Bergstra, J.A.Klop, J.W. since nowadays many process algebras have an operational semantics in the style of [Plotkin1981]Plotkin, G.D.. So, we equip all the languages with such an operational semantics. In the articles [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W., [Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W., BPA voidBPABPA : basic process algebra, PA voidPAPA : process algebra, and ACP voidACPACP : algebra of communicating processes\ were introduced with a semantics in terms of projective limit models. When we restrict ourselves to guarded recursion, projective limit models identify exactly the (strongly) bisimilar processes. The projective limit models are an algebraic reformulation of the topological structures used in [Bakker and Zucker1982]Bakker, J.W. deZucker, J.I.. Regarding syntax as well as semantics, [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W. reformulates [Bakker and Zucker1982]Bakker, J.W. deZucker, J.I. in order to allow more efficient algebraic reasoning.

For those readers who want to know more about possibly other approaches to process algebra (with abstraction), we refer to the following four text books in the area [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P., [Hennessy1988]Hennessy, M., [Hoare1985]Hoare, C.A.R., and [Milner1989]Milner, R.; see also section 4.

Finally, we briefly review what can be expected in this survey. The survey is organized into three sections (not counting this section).

The first section (2) describes concrete sequential processes; that is, in this section we even refrain from discussing parallelism. In this section, we will meet and tackle many problems that accompany the design of any algebraic language. Since the languages are simple, it is relatively easy to explain the solutions. The solutions that we obtain for the concrete sequential processes turn out to be useful for other languages, too. In particular, we will use these solutions in section 3 where we discuss concrete concurrent processes. Lastly, section 4 gives directions for further reading.

#### Acknowledgements

We thank the proof readers, Jan Bergstra (University of Amsterdam and Utrecht University) and Jan Willem Klop (CWI and Free University Amsterdam) for their useful comments. Also comments by Twan Basten (Eindhoven University of Technology), Kees Middelburg (PTT Research and Utrecht University), Alban Ponse (University of Amsterdam), and Michel Reniers (Eindhoven University of Technology) were appreciated. Special thanks go to Joris Hillebrand (University of Amsterdam) for his essential help in the final stages of the preparation of the document.

# 2 Concrete sequential processes

In this section we will introduce some basic concepts that can be found in process algebra. We will do this in a modular way. That is, first we treat a basic theory that is the kernel for all the other theories that we will discuss subsequently. The basic theory describes finite, concrete, sequential non-deterministic processes. Then we add features to this kernel that are known to be important in process algebra: for instance, deadlock or recursion to mention a few. Such features make the kernel more powerful for both theoretical and practical purposes. We also show that each feature is a so-called conservative extension of the original theory; thus, we may argue that our approach is modular.

## 2.1 Introduction

In this subsection we give the reader an idea of what can be expected in the subsections of the sequential part of this survey.

We start with the basic language. Once we have treated this language, we will extend it in the following subsections with important features. We discuss the notions of recursion in subsection 2.3, projection in 2.4, deadlock (or inaction) in 2.5, empty process in 2.6, and we discuss the following operators: renaming operators in subsection 2.7, state operators in 2.8 and 2.9, the priority operator in 2.10, and Kleene's binary star operator in 2.11. Next, we focus in subsection 2.12 on an extension with time. Then subsection 2.13 follows with pointers to extensions that we do not discuss in this survey. Finally, we discuss decidability and expressiveness issues in subsection 2.14 for some of the languages introduced.

## 2.2 Basic process algebra

First, we list some preliminaries. Then we treat the basic language of this chapter. Next, we devote subsection 2.2.2 to term rewriting analysis; we discuss a powerful method that we will frequently need subsequently. In the next, and last, subsection 2.2.3 we discuss an operational semantics for our basic language. In 2.2.3 we also treat a meta-theorem on operational semantics that we will often use in the rest of this survey.

We assume that we have an infinite set V of variables with typical elements [IMAGE ]. A (single sorted) signaturesignature [IMAGE ]voidSigma[IMAGE ]: signature is a set of functionfunction symbol symbolssymbol!function together with their arityarity. If the arity of a function symbol [IMAGE ] is zero we say that f is a constantconstant symbol symbolsymbol!constant. The notion of a termterm (over [IMAGE ]) is defined as expected: [IMAGE ] is a term; if [IMAGE ] are terms and if [IMAGE ] is n-aryvoidn-aryn-ary: arity of function symbol then [IMAGE ] is a term. A term is also called an openopen term termterm!open; if it contains no variables we call it closedclosed termterm!closed. We denote the set of closed terms by [IMAGE ]voidCSigma[IMAGE ]: closed terms and the set of open terms by [IMAGE ]voidOSigma[IMAGE ]: open terms (note that a closed term is also open). We also want to speak about the variables occurring in terms: let [IMAGE ] then [IMAGE ]voidvart[IMAGE ]: variables in a term t is the set of variables occurring in t.

A substitutionsubstitution [IMAGE ]voidsigma[IMAGE ]: substitution 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.

### 2.2.1 The theory Basic Process Algebra

We will give the theorytheory Basic Process Algebra or BPA voidBPABPA : basic process algebra in terms of an equationalequational specification specificationspecification!equational. BPA voidBPABPA : basic process algebra is due to [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W..

[IMAGE ]

We define the definition of derivability of an equation from an equational specification.

Now we give the theory [IMAGE ].

We begin with the signature [IMAGE ]voidSigmaBPA[IMAGE ]: signature of BPA. There are two binary operators present in [IMAGE ]; they are denoted +voidA AAA+: alternative composition and [IMAGE ]voidA AAB[IMAGE ]: sequential composition. The signature [IMAGE ] also contains a number of constants with typical names [IMAGE ]. We will use the capital letter AvoidAA: set of atomic actions for the set of constants. The set A can be seen as a parameter of the theory BPA voidBPABPA : basic process algebra: for each application the set A will be specified. For now it is only important that there are constants. This ends our discussion of the signature.

The set of equations [IMAGE ]voidEBPA[IMAGE ]: axioms of BPA consists of the five equations A1-5voidA1-5A1-5: axioms of BPA in table 1. The variables x,y, and z in table 1 are universally quantified. They stand for elements of some arbitrary model of BPA voidBPABPA : basic process algebra. These elements are often called processesprocess.

[IMAGE ]

[IMAGE ]
Table 1: BPA.

#### Intuition

We will give an intuitive meaning of the signature and the axioms respectively. Formal semantics can be found in 2.2.3.

The constants [IMAGE ] are called atomicatomic actionaction!atomic actions or stepsstep. We consider them as processes, which are not subject to any investigation whatsoever.

We think of the centered dot [IMAGE ] as sequential compositionsequential compositioncomposition!sequential. The process xy is the process that first executes the process x and when (and if) it is completed y starts.

The sumsum!of two processesprocess!sum of two [IMAGE ]es or alternativealternative compositioncomposition!alternative composition x+y of two processes x and y represents the process that either executes x or y but not both.

Now we will discuss the axioms of table 1.

Axiom A1 expresses the commutativitycommutativity of the alternative composition. It says that the choice between x and y is the same as the choice between y and x.

Axiom A2 expresses the associativityassociativity of the plus. It says that first choosing between x+y and z and then (possibly) a choice between x and y is the same as choosing between x and y+z and then (possibly) a choice between y and z.

Axiom A3 expresses the idempotencyidempotency of the alternative composition. A choice between x and x is the same as a choice for x.

Axiom A4 expresses the rightright distributivitydistributivity!right distributivity of the sequential composition over the alternative composition. A choice between x and y followed by z is the same as a choice between x followed by z and y followed by z.

Axiom A5 expresses the associativity of the sequential composition. First xy followed by z is the same as first x followed by yz.

#### Full distributivity

We will explain why only right distributivity is presented in table 1. An axiom that does not appear in BPA voidBPABPA : basic process algebra is the axiom that expresses the leftleft distributivitydistributivity!left distributivity (LD) of the sequential composition over the alternative composition:

[IMAGE ]

Axioms A4 and LD together would give fulldistributivity!fullfull distributivity distributivity. Axiom LD is not included on intuitive grounds. In the left-hand side of LD the moment of choice is later than in the right-hand side. For in a(b+c) the choice between b and c is made after the execution of a, whereas in ab+ac first the choice between ab and ac must be made and then the chosen term can be executed, as in figure 1, where we depict two deduction graphs. See definition 2.2.24 later on for a formal definition of a deduction graph.

The right-hand side of LD is often called a non-deterministicnon-deterministic choice, which is a subject of research on its own.

[IMAGE ]
Figure: Two deduction graphs with the same execution paths ab and ac but with different choice moments.

#### Structural induction

Structural inductionstructural inductioninduction!structural is a basic proof technique in process algebra when closed terms are involved. We will inductively define the class of basic terms. It will turn out that every closed term can be written as a basic term.

[IMAGE ]

In the next proposition we see that if we want to prove a statement correct for all closed terms (see subsection 2.2 for the definition of a closed term), it suffices to prove it for basic terms. Since they are inductively defined we can use structural induction.

[IMAGE ]

### 2.2.2 Term rewriting systems

In this subsection we will introduce a result from the field of term rewriting systems that is a powerful tool in process algebra. We will do this by means of an example: we will prove the essential step of proposition 2.2.6 using the result. General references to this theory are [Dershowitz and Jouannaud1990]Dershowitz, N.Jouannaud, J.-P. and [Klop1992]Klop, J.W..

[IMAGE ]

A useful property for a term reduction system is that there are no infinite reductions possible. Below we define some more notions.

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

The method of the recursive path ordering is not convenient for rewriting rules such as [IMAGE ]. We will discuss a variant of the above method which is known as the lexicographical variant of the recursive path ordering. The idea is that we give certain function symbols the so-called lexicographical statuslexicographical statusstatus!lexicographical (the remaining function symbols have the multiset statusmultiset statusstatus!multiset). The function symbols with a lexicographical status have, in fact, an arbitrary but fixed argument for which this status holds. For instance, we give the sequential composition the lexicographical status for the first argument.

We also have an extra rule to cope with function symbols with a lexicographical status. For a k-ary function symbol H with the lexicographical status for the ith argument we have the following extra rule in table 4. The idea behind this rule is that if the complexity of a dedicated argument is reduced and the complexity of the other arguments increases (but not unboundedly) the resulting term will be seen as less complex as a whole.

[IMAGE ]

[IMAGE ]
Table 4: The extra rule for the lexicographical variant of the recursive path ordering. We have that H has the lexicographical status for the ith argument.

[IMAGE ]

So with the aid of the above theorem we conclude that the term rewriting system of table 2 is strongly normalizing (we leave the case RA3 to the reader). To prove strong normalization we will henceforth confine ourselves to giving a partial ordering > on the signature and to saying which function symbols do have the lexicographical status (and for which argument).

### 2.2.3 Semantics of basic process algebra

In this subsection we will give an operational semantics of BPA voidBPABPA : basic process algebra in the style of Plotkin; see [Plotkin1981]Plotkin, G.D.. The usual procedure to give an operational semantics is to only give a table with so-called transition rules; see, for instance, table 5. In this subsection we will make a small excursion to the so-called general theory of structured operational semantics because in that framework we can formulate general theorems that hold for large classes of languages. The reason for this detour is that we will use such general results many times in this chapter.

To start with, we define the notion of a term deduction system, which is taken from [Baeten and Verhoef1993]Baeten, J.C.M.Verhoef, C.. It is a modest generalization of the notion of a transition system specificationtransition system specificationspecification!transition system that originates from [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W.. The idea of a term deduction system is that it can be used not only to define a transition relationtransition relationrelation!transition but also to define unary predicates on states that turn out to be useful. See table 5 for a typical term deduction system; it is a definition of both transition relations [IMAGE ] and unary predicates [IMAGE ]a[IMAGE ] for each [IMAGE ].

First we list some preliminaries for completeness sake.

We recall that the meaning or semanticssemantics of an equational specification [IMAGE ] is given by a modelmodel or an algebraalgebra [IMAGE ]voidA[IMAGE ]: an algebra. Such an algebra consists of a set of elements UvoidUU: the universe of [IMAGE ] (called the universeuniverse or domaindomain of [IMAGE ]) together with constants in U and functions from [IMAGE ] to U. We call [IMAGE ] a [IMAGE ]-algebravoidSigma-algebra[IMAGE ]-algebra: an algebraalgebra![IMAGE ]- when there is a correspondence between the constant symbols in [IMAGE ] and the constants in U, and between the function symbols in [IMAGE ] and the functions in [IMAGE ] (of the same arity). We call such a correspondence an interpretationinterpretation. Now if [IMAGE ] is a [IMAGE ]-algebra of the equational specification [IMAGE ], then an equation s=t over [IMAGE ] has a meaning in [IMAGE ], when we interpret the constant and function symbols in s and t by the corresponding constants and functions in [IMAGE ]. Moreover, the variables in s and t are universally quantified. So when for all variables in s and t we have that the statement s=t is true in [IMAGE ] we write [IMAGE ] and we say [IMAGE ] satisfiessatisfy s=t or s=t holdshold (an equation [IMAGE ]s in a model) in [IMAGE ]. We call [IMAGE ]voidA AAL[IMAGE ]: the satisfiability relation the satisfiability relationsatisfiability relationrelation!satisfiability. If a [IMAGE ]-algebra [IMAGE ] satisfies all equations s=t over [IMAGE ] we write [IMAGE ] (or [IMAGE ]) and we say that [IMAGE ] is an algebra for E, or a model of E. We also say that E is a sound axiomatizationsound axiomatizationaxiomatization!sound of [IMAGE ]. See remark 2.2.34 and theorem 2.2.35 for an example.

[IMAGE ]
Table: Derivation rules of [IMAGE ].

Next, we give the definition of a proof of a formula from a set of deduction rules. This definition is taken from [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W..

[IMAGE ]

[IMAGE ]

[IMAGE ]
Figure 2: A proof

Next, we define the notion of a deduction graph. It generalizes the well-known notion of a labelled state transition diagramstate transition diagram in the sense that it can also handle unary predicates on states. First, we need a reachability definition.

Next, we define the notion of a structured state system [Baeten and Verhoef1993]Baeten, J.C.M.Verhoef, C.. It is a generalization of the well-known notion of a labelled transition systemlabelled transition systemsystem!labelled transition.

A term deduction system induces in a natural way a structured state system.

[IMAGE ]

Many different equivalence notions have been defined in order to identify states that have the same behaviour; see [Glabbeek1990]Glabbeek, R.J. van and [Glabbeek1993]Glabbeek, R.J. van for a systematic approach. The finest among them is the so-called strong bisimulation equivalence of [Park1981]Park, D.M.R.. We will take the formulation of [Baeten and Verhoef1993]Baeten, J.C.M.Verhoef, C. for this well-known notion.

It will turn out that the two deduction graphs of example 2.2.27 are bisimilar.

Considered as deduction graphs, the two processes x=ab and y=ab+a(b+b) are not equal, but from a process algebraic point of view, we want them to be. That is, they both first execute the atomic process a and then the b. So we would like to have a model for which ab=ab+a(b+b). The usual approach to obtain this is to work with an equivalence relation and to identify equivalent objects. We then say that the objects are equal modulo this equivalence relation. If x is a process and [IMAGE ] denotes bisimulation equivalence, the equivalence class is defined [IMAGE ]voidx[x]: bisimulation equivalence class. So, in the above example the two processes x=ab and y=ab+a(b+b) are equal modulo bisimulation equivalence: [x]=[y]. Now it would be very nice if the equivalence class is independent of the chosen representative. If this is the case, we can easily define our process algebra operators on these classes. For instance, the alternative composition can be defined as [x]+[y]=[x+y]. In general, the assumption that a relation is an equivalence relation is too weak for this purpose. The additional property that does the job is called congruency. In the next definition we define this well-known notion.

[IMAGE ]

Next, we define some syntactical constraints on the rules of a term deduction system for which it can be proved that if a term deduction system satisfies these constraints then strong bisimulation equivalence will always be a congruence. Below we discuss the so-called path formatvoidpathpath: a format; this stands for ``predicates and tyft /tyxt hybrid format'' and is proposed by [Baeten and Verhoef1993]Baeten, J.C.M.Verhoef, C.. It is a modest generalization of the tyft /tyxt  formatvoidtyfttyxttyft /tyxt : a formattyft/tyxt formatformat!tyft/tyxt originating from [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W.. The name tyft /tyxt refers to the syntactical form of the deduction rules.

We refer to [De Simone1985]De Simone, R. for the first paper that discusses syntactical constraints on operational rules. Nowadays, the syntactical constraints formulated in that paper are often referred to as the ``De Simone formatDe Simone formatformat!De Simone''.

Next, we formulate the congruence theorem for the path format. It is taken from [Baeten and Verhoef1993]Baeten, J.C.M.Verhoef, C.. There the so-called well-founded subcase is proved. [Fokkink1994]Fokkink, W.J. showed that this requirement is not necessary, thus yielding the following result. Note that we do not use the notion pure in the theorem below. We just define it since we will need this notion later on when we will have our second excursion into the area of general SOS theory.

[IMAGE ]

[IMAGE ]

Next we will show that BPA voidBPABPA : basic process algebra is a complete axiomatization of the set of closed terms modulo bisimulation equivalence. We recall that an axiomatization is completecomplete(ness) if bisimilar x and y are provably equal with these axioms. Note that we only talk about closed process terms here: complete axiomatizations for open terms are much more difficult, see, e.g. [Groote1990a]Groote, J.F.. But first we will need some preliminaries to prove this; they are listed in the next lemma.

[IMAGE ]

[IMAGE ]

## 2.3 Recursion in BPA

In this subsection we will add recursion to the theory BPA voidBPABPA : basic process algebra.

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

At this point we have all the necessary definitions to define the equational specification BPA rec voidBPArecBPA rec : BPA with recursion, in which rec voidrecrec: recursion is an abbreviation for recursion. The signature of BPA rec voidBPArecBPA rec : BPA with recursion consists of the signature of BPA voidBPABPA : basic process algebra plus for all recursive specifications E(V) and for all [IMAGE ] a constant [IMAGE ]. The axioms of BPA rec voidBPArecBPA rec : BPA with recursion consist of the axioms of BPA voidBPABPA : basic process algebra plus for all recursive specifications [IMAGE ] and for all [IMAGE ] an equation [IMAGE ].

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

The next two definitions are taken from [Bergstra and Klop1986]Bergstra, J.A.Klop, J.W..

[IMAGE ]

[IMAGE ]

Together, ^-[IMAGE ]voidRDPmin[IMAGE ]: restricted recursive definition principle and RSP voidRSPRSP : recursive specification principle say that a guarded recursive specification has a unique solutionsolution!uniqueunique solution.

#### Semantics

The semantics of BPA rec voidBPArecBPA rec : BPA with recursion can be given completely analogously to the semantics for BPA voidBPABPA : basic process algebra that we gave in subsection 2.3.

We consider the term deduction system [IMAGE ] with as signature the signature of BPA rec voidBPArecBPA rec : BPA with recursion and as rules the rules in table 5 together with those in table 6. Bisimulation equivalence is a congruence on the structured state system [IMAGE ] induced by [IMAGE ]; see 2.2.32. So on the quotient of the algebra of closed BPA rec voidBPArecBPA rec : BPA with recursion terms with respect to bisimulation equivalence we can define the operators of BPA rec voidBPArecBPA rec : BPA with recursion by taking representatives. The next theorem states that this quotient algebra is a model of BPA rec voidBPArecBPA rec : BPA with recursion.

[IMAGE ]

[IMAGE ]
Table 6: Derivation rules for recursion ([IMAGE ]).

[IMAGE ]
Figure: Two deduction graphs of the processes X and Y that can be found in example 2.3.2.

## 2.4 Projection in BPA

In subsection 2.3 we introduced guarded recursive specifications. They are mainly used to specify infinite processes such as a counter: see example 2.14.5. With the principles RDP voidRDPRDP : recursive definition principle\ and RSP voidRSPRSP : recursive specification principle we can prove statements involving such infinite processes. See example 3.6.1 for an application of RSP voidRSPRSP : recursive specification principle. In this subsection we will introduce another method for this purpose. The idea is that we approximate an infinite process by its finite projections. The finite projections for their part turn out to be closed terms and they can therefore be taken care of by structural induction (see also 2.2 for structural induction). This material is based on the paper [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W..

We will define the equational specification +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections, in which PRvoidPRPR: projection is an abbreviation for projection.

The signature of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections consists of the signature of BPA voidBPABPA : basic process algebra\ plus for each [IMAGE ] a unary function [IMAGE ]voidpin[IMAGE ]: projection operator that is called a projection operator of order nprojection operatoroperator!projection or the nth projection. The axioms of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections consist of the axioms of table 7 and the axioms of BPA voidBPABPA : basic process algebra; we call the axioms PR1-4voidPR1-4PR1-4: projection axioms. In table 7 we have [IMAGE ], the letter a ranges over all the atomic actions, and the variables x and y are universally quantified.

We will now discuss the axioms of table 7.

The idea of projections is that we want to be able to cut off a process at a certain depth. An atomic action is intrinsically the most ``shallow'' process so we cannot cut off more. Axiom PR1 expresses this: a projection operator is invariant on the set of atomic actions.

The subscript n of the projection operator serves as a counter for the depth of a process. Axioms PR2 and PR3 illustrate how this counter can be decremented.

Axiom PR4 says that the projection operator distributes over the alternative composition: choosing an alternative does not alter the counter of the projection operator.

[IMAGE ]
Table 7: Projection.

#### Proof rule

We will discuss a proof rule expressing that a process is determined by its finite projections. This rule is due to [Bergstra and Klop1986]Bergstra, J.A.Klop, J.W..

[IMAGE ]

The following theorem states that projection operators can be eliminated from closed terms. To prove this we will use a method that we briefly explained in subsection 2.2.2. First, we define what we mean by the elimination of operators.

[IMAGE ]
Table: A term rewriting system for +PR [IMAGE ].

[IMAGE ]

Next, we formulate a traditional theorem in process algebra. It states that the term rewriting system associated to the equational specification +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections behaves neatly: it terminates modulo the equations without a clear direction (viz. the commutativity and the associativity of alternative composition) and it is confluentconfluent modulo these equations. In term rewriting theory, this is expressed by saying that the term rewriting system is completecomplete. Incidentally, note that we proved in theorem 2.4.4 that the associated term rewriting system terminates, but not that it terminates modulo the equations A1 and A2.

The main application of the next result is that it is usually used to prove the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over BPA voidBPABPA : basic process algebra (an extension is conservative if no new identities can be derived between original terms in the extended system). The proof of this term rewriting theorem requires much term rewriting theory, which is beyond the scope of this chapter. For more information on these term rewriting techniques we refer to [Jouannaud and Muñoz1984]Jouannaud, J.-P.Muñoz, M. and [Jouannaud and Kirchner1986]Jouannaud, J.-P.Kirchner, H.. Nevertheless, we want to mention the theorem anyway, since it has an importance of its own, for instance for implementational purposes. We will prove the conservativity with an alternative method that we will explain in the next subsection; see subsection 2.4.1.

The next theorem states that for a closed term s the sequence

[IMAGE ]

converges to the term s itself. It is a nice example of the use of structural induction.

[IMAGE ]

[IMAGE ]
Table 9: Derivation rules for projections.

#### Semantics

The semantics of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections can be given in the same way as the semantics for BPA voidBPABPA : basic process algebra.

We consider the term deduction system [IMAGE ]+PR [IMAGE ] with as signature the signature of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections and as deduction rules the rules in tables 5 and 9. Bisimulation equivalence is a congruence on the structured state system induced by [IMAGE ]+PR [IMAGE ]; see 2.2.32. So the quotient of closed +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections terms with respect to bisimulation equivalence is well-defined; that is, the operators of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections can be defined on this quotient by taking representatives. The following theorem states that this quotient is a model of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections.

[IMAGE ]

### 2.4.1 Conservativity

Here, we will explain how to prove the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over BPA voidBPABPA : basic process algebra without using theorem 2.4.5. We recall that the main application of theorem 2.4.5 is that we can prove that adding the projection operators does not yield new identities between BPA voidBPABPA : basic process algebra terms. This important property is called conservativity. We did not give a proof of theorem 2.4.5, but instead we will provide an alternative powerful method for proving the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over BPA voidBPABPA : basic process algebra (and all the other conservativity theorems in this chapter). This method is based on the format of the operational rules of both systems rather than on a term rewriting analysis. So, we will make a second expedition into the area of general theory on structured operational semantics and we will illustrate the theory with a running example. This example will yield, of course, the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over BPA voidBPABPA : basic process algebra. We will base ourselves on [Verhoef1994b]Verhoef, C..

First we formalize how we can join two given signatures.

[IMAGE ]

[IMAGE ]

Next, we define how to ``add'' two operational semantics.

[IMAGE ]

[IMAGE ]

Next, we define what we will call operational conservativity. This definition is taken from [Verhoef1994b]Verhoef, C., but this notion is already defined by [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W. for the case without extra predicates on states.

[IMAGE ]

Before we can continue with a theorem that gives sufficient conditions when a term deduction system is an operationally conservative extension of another such system, we need one more definition. This definition originates from [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W..

[IMAGE ]

Now, we are in a position to state a theorem providing us with sufficient conditions so that a term deduction system is an operationally conservative extension of another one. This theorem is based on a more general theorem of [Verhoef1994b]Verhoef, C.. A more restrictive version of this theorem was first formulated by [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W..

[IMAGE ]

Now that we have the operational conservativity, we need to make the connection with the usual conservativity. Following [Verhoef1994b]Verhoef, C., henceforth we will call this well-known property equational conservativity to exclude possible confusion with the already introduced notion of operational conservativity. As an intermediate step, we will first define the notion of operational conservativity up to [IMAGE ] equivalence. Here, [IMAGE ] equivalence is some (semantical) equivalence that is defined in terms of relation and predicate symbols only. Strong bisimulation equivalence is an example of an equivalence that is definable exclusively in terms of relation and predicate symbols. This definition was first formulated by [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W. for the case of operational conservativity up to strong bisimulation equivalence. Roughly, if original terms s and t are bisimilar in the extended system, if and only if they are bisimilar in the original system we call the large system a conservative extension up to bisimulation equivalence of the original one. The next definition expresses this for any equivalence.

[IMAGE ]

[IMAGE ]

Next, we formulate a theorem stating that if a large system is an operationally conservative extension of a small system, then it is also an operationally conservative extension up to any equivalence that is definable in terms of relation and predicate symbols only. This theorem is taken from [Verhoef1994b]Verhoef, C.. This theorem was formulated by [Groote and Vaandrager1992]Groote, J.F.Vaandrager, F.W. for the case of strong bisimulation equivalence.

[IMAGE ]

Now that we have the intermediate notion of operational conservativity up to some equivalence, we will come to the well-known notion that in this chapter we will call equational conservativity. We recall that an equational specification is a pair consisting of a signature and a set of equations over this signature. First we define how we combine equational specifications into larger ones.

[IMAGE ]

[IMAGE ]

Next, we define the notion of equational conservativity.

[IMAGE ]

Now we have all the prerequisites to formulate the equational conservativity theorem. This theorem is taken from [Verhoef1994b]Verhoef, C..

Now, we can apply the equational conservativity theorem to prove the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over BPA voidBPABPA : basic process algebra.

[IMAGE ]

Now that we have the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections, we can immediately prove its completeness from the completeness of the subsystem BPA voidBPABPA : basic process algebra. We will not do this directly, but we will formulate a general completeness theorem that can be found in [Verhoef1994b]Verhoef, C.; it is a simple corollary of the equational conservativity theorem. This completeness theorem states that the combination of conservativity, elimination of extra operators, and the completeness of the subsystem yields the completeness of the extension. For the formulation of the next theorem, we stick to the notations and assumptions stated in theorem 2.4.24.

[IMAGE ]

[IMAGE ]

### 2.4.2 Recursion and projection

In this subsection we will add recursion and projections to the theory BPA voidBPABPA : basic process algebra.

We will define the equational specification +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections by means of a combination of BPA rec voidBPArecBPA rec : BPA with recursion and +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections.

The signature of +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections consists of the signature of BPA rec voidBPArecBPA rec : BPA with recursion plus for each [IMAGE ] a unary function [IMAGE ] (projections). The axioms of +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections are the axioms of BPA rec voidBPArecBPA rec : BPA with recursion and the axioms of table 7.

#### Proof rule

We will discuss a proof rule expressing that a process that can be specified with the aid of a guarded recursive specification is determined by its finite projections. This rule is a restricted version of the rule that is defined in definition 2.4.1 and is also due to [Bergstra and Klop1986]Bergstra, J.A.Klop, J.W..

[IMAGE ]

[IMAGE ]

The following corollary is called the projection theorem.

[IMAGE ]

[IMAGE ]

#### Semantics

The semantics of +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections is given by means of a term deduction system [IMAGE ]+PR [IMAGE ] with as signature the signature of +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections and as rules the rules in tables 56, and 9. Bisimulation equivalence is a congruence on the structured state system [IMAGE ]+PR [IMAGE ] induced by [IMAGE ]+PR [IMAGE ]; see 2.2.32. So the quotient of closed +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections terms modulo strong bisimulation equivalence is well-defined; that is, the operators of +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections can be defined on this quotient by taking representatives. The next theorem states that this quotient is a model of +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections.

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

The following theorem concerns the theory BPA rec voidBPArecBPA rec : BPA with recursion. The result was already stated in theorem 2.3.13. We postponed the proof of this until now, since we want to use the fact that RSP voidRSPRSP : recursive specification principle holds in +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections.

[IMAGE ]

Usually deadlock stands for a process that has stopped its executions and cannot proceed. In this subsection we will extend the theory BPA voidBPABPA : basic process algebra with a process named deadlock. We can distinguish between successfulsuccessful terminationtermination!successful and unsuccessfulunsuccessful terminationtermination!unsuccessful termination in the presence of deadlock. This subsection is based on [Bergstra and Klop1984a, Bergstra and Klop1995]Bergstra, J.A.Klop, J.W..

Let [IMAGE ] be a sequential composition of two processes. The process y starts if x has terminated. But if x reaches a state of inaction due to deadlock, we do not want y to start: we want it only to start when x terminates successfully. We will axiomatize the behaviour of a deadlocked process called [IMAGE ] in table 10.

The signature of the equational specification _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock is the signature of BPA voidBPABPA : basic process algebra extended with a constant [IMAGE ]voiddelta[IMAGE ]: deadlock called deadlockdeadlockprocess!deadlocked, or inactioninaction. The axioms of the equational specification _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock are the axioms of BPA voidBPABPA : basic process algebra in table 1 plus the two axioms in table 10 (A6 and A7voidA6-7A6-7: deadlock axioms). We will discuss them now.

Equation A6 expresses that [IMAGE ] is a neutral element with respect to the alternative composition; it says that no deadlock will occur as long as there is an alternative that can proceed. Axiom A7 says that the constant [IMAGE ] is a left-zero element for the sequential composition. It says that after a deadlock has occurred, no other actions can possibly follow. Actually, inaction would be a better name for the constant [IMAGE ], for a process [IMAGE ] ([IMAGE ]) contains no deadlock. Deadlock only occurs if there is no alternative to [IMAGE ], as in [IMAGE ].

So using the process [IMAGE ] we can distinguish between successful and unsuccessful termination. Thus, the process [IMAGE ] terminates unsuccessfully whereas a terminates successfully.

[IMAGE ]

#### Structural induction

In _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock we can use the technique of structural induction just like in BPA voidBPABPA : basic process algebra (compare page [*]). We will adjust the definition of a basic term (see definition 2.2.4) and we will mention the result that every closed term over _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock can be written as a basic term.

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

#### Semantics

As usual, we give the semantics by means of a term deduction system. Take for the signature of [IMAGE ]_[IMAGE ] the signature of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock and for the set of rules just the ones of BPA voidBPABPA : basic process algebra of table 5. Since bisimulation equivalence is a congruence (2.2.32), the quotient of closed _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock terms modulo bisimulation equivalence is well-defined so the operators of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock can be defined on this quotient using representatives. This quotient is a model of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock.

[IMAGE ]

[IMAGE ]

### Extensions of _[IMAGE ]

In this subsection we will discuss the extensions of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with recursion and/or projections.

#### Recursion

We can add recursion to _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock in exactly the same way as we did for BPA voidBPABPA : basic process algebra. The equational specification _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion contains the signature of BPA rec voidBPArecBPA rec : BPA with recursion and a constant [IMAGE ]. The axioms of _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion are the axioms of BPA rec voidBPArecBPA rec : BPA with recursion plus the axioms of table 10.

Note that [IMAGE ] so it cannot serve as a guard: [IMAGE ] is not completely guarded but it is guarded since [IMAGE ].

The semantics of _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion can be given by means of the term deduction system [IMAGE ] that has as its signature the signature of _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion and as rules the rules of tables 5 and 6. Since bisimulation equivalence is a congruence (2.2.32), the operators of _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion\ can be defined on the quotient algebra of closed _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion terms with respect to bisimulation equivalence. This quotient is a model of _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion and it satisfies RDP voidRDPRDP : recursive definition principle. To prove this, combine the proofs of theorems 2.3.13 and 2.5.4. Moreover this model satisfies RSP voidRSPRSP : recursive specification principle, which can be proved when we combine _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion\ with projections.

#### Projection

We can extend _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with projections in exactly the same way as we did for BPA voidBPABPA : basic process algebra. The equational specification +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections has as its signature the signature of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections and a constant [IMAGE ]. Its axioms are the axioms of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections and the ones concerning deadlock (tables 17, and 10). We assume that a ranges over [IMAGE ] in table 7 on projections.

The following theorem states that projection operators can be eliminated from closed terms.

[IMAGE ]

[IMAGE ]

[IMAGE ]

The semantics of +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections can be given with the term deduction system [IMAGE ]+PR [IMAGE ] that has as its signature the signature of +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections and as rules the rules of tables 5 and 9. Since bisimulation equivalence is a congruence (2.2.32), it follows that the operators of +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections can be defined on the quotient algebra of closed +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections terms with respect to bisimulation equivalence. This quotient is a model of +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections and it satisfies AIP voidAIPAIP : approximation induction principle. To prove this, combine the proofs of theorems 2.4.7 and 2.5.4. Moreover, according to theorem 2.4.24 we have that +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections is a conservative extension of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock. So with theorem 2.4.26 we find that +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections is a complete axiomatization of this model (use also theorem 2.5.6).

#### Recursion and projection

Here we extend _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with recursion and projections. The equational specification +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections has as its signature the signature of _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion plus for each [IMAGE ] a unary function [IMAGE ]. The axioms are the axioms of _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion and the axioms concerning projections (table 7). We assume that a ranges over [IMAGE ] in this table.

The standard facts (and their proofs) of subsection 2.4.2 are easily transposed to the present situation. Their translation is, in short: every projection of a solution of a guarded recursive specification can be rewritten into a closed _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock term; the projection theorem 2.4.31 holds; and ^-[IMAGE ]voidAIPmin[IMAGE ]: restricted approximation induction principle implies RSP voidRSPRSP : recursive specification principle.

The semantics of +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections is given by means of a term deduction system [IMAGE ]+PR [IMAGE ]. Its signature is the signature of +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections\ and its rules are those of [IMAGE ]+PR [IMAGE ] plus the rules concerning recursion that are presented in table 6. Since bisimulation equivalence is a congruence, the quotient algebra of closed +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections terms with respect to bisimulation equivalence is well-defined, and the operators of +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections can be defined on this quotient. This quotient is a model of +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections and it satisfies RDP voidRDPRDP : recursive definition principle, RSP voidRSPRSP : recursive specification principle, and ^-[IMAGE ]voidAIPmin[IMAGE ]: restricted approximation induction principle, but not its unrestricted version AIP voidAIPAIP : approximation induction principle. We can prove that _[IMAGE ]rec voidBPAdeltarec[IMAGE ]rec : [IMAGE ] with recursion satisfies RSP voidRSPRSP : recursive specification principle. This is proved in the same way as theorem 2.4.36.

## 2.6 Empty process

In many situations it is useful to have a constant process that stands for immediate successful termination. In this subsection we will extend the equational specifications BPA voidBPABPA : basic process algebra and _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with a process that is only capable of terminating successfully. We will call such a process the empty process and we will denote it by [IMAGE ]. This constant originates from [Koymans and Vrancken1985]Koymans, C.P.J.Vrancken, J.L.M.. Another reference to this constant is [Vrancken1986]Vrancken, J.L.M..

[IMAGE ]
Table 11: Empty process.

The empty process is a counterpart of the process deadlock. The process deadlock stands for immediate unsuccessful terminationunsuccessful terminationtermination!unsuccessful while the empty process stands for immediate successful terminationsuccessful terminationtermination!successful. Moreover, the combination of the two axioms A8 and A9 of table 11 express that [IMAGE ] is a neutral element with respect to the sequential composition whereas axioms A1 and A6 express that [IMAGE ] is a neutral element with respect to the alternative composition. Note that successful termination (not in a sum context) after the execution of at least one action can already be expressed in systems without [IMAGE ], as [IMAGE ] ([IMAGE ]).

The equational specifications _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process and _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process are defined as follows.

The signature of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process consists of the signature of BPA voidBPABPA : basic process algebra extended with a constant [IMAGE ]voidepsilon[IMAGE ]: empty process called the empty processempty processprocess!empty. The equations of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process are the axioms of BPA voidBPABPA : basic process algebra and the axioms A8 and A9voidA8-9A8-9: empty process axioms of table 11.

The signature of _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process consists of the signature of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock extended with a constant [IMAGE ]. The axioms of _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process are the ones of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock plus A8 and A9.

#### Structural induction

In _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process and _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process we can use the technique of structural induction just like in BPA voidBPABPA : basic process algebra or _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock since every closed term can be written as a basic term. We will adjust the definition of a basic term to the present situation and we will mention that closed terms over _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process or _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process\ can be written as basic terms.

[IMAGE ]

[IMAGE ]

[IMAGE ]

[IMAGE ]

#### Semantics

We give the semantics of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process and _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process by means of term deduction systems. We handle both cases at the same time. Take for the signature of [IMAGE ]_()[IMAGE ] the signature of _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] and for the set of rules the ones that are presented in table 12. This operational semantics is taken from [Baeten and Glabbeek1987]Baeten, J.C.M.Glabbeek, R.J. van.

The term deduction systems that we consider here differ from the ones that we treated before: instead of successful termination predicates [IMAGE ]a[IMAGE ] we now have a termination option predicatetermination option predicatepredicate!termination option; it is denoted postfix: [IMAGE ]voidA AAO[IMAGE ]: termination option predicate (postfix predicate). Since they both are unary predicates on states we can still use the general theory on structured operational semantics that we treated in subsection 2.2.3. In particular we can use theorem 2.2.32 to prove that bisimulation equivalence is a congruence. So, the quotient algebra of closed _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] terms with respect to bisimulation equivalence is well-defined for the operators of _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ]. This quotient is a model for _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ].

[IMAGE ]
Table: Derivation rules of [IMAGE ]_()[IMAGE ].

[IMAGE ]

[IMAGE ]

### 2.6.1 Conservativity

In this subsection we will explain how to prove that _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process is a conservative extension of BPA voidBPABPA : basic process algebra. We cannot immediately use the theory of subsection 2.4.1, since the operational semantics of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process\ presented in table 12 is not an operationally conservative extension of the operational semantics of BPA voidBPABPA : basic process algebra that we listed in table 5. For we can prove in the extended system that [IMAGE ], whereas in the subsystem we can prove that [IMAGE ]a[IMAGE ]. So we can ``reach'' a new term if we start with an original term. A possible solution for this problem is to give an alternative operational semantics for _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process than the one that we present in table 12.

The special behaviour of the constant [IMAGE ] is expressed in the operational semantics of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process as it is presented in table 12. Another possibility is to express the special behaviour of the empty process with the aid of the equivalence relation. A well-known example of this kind is observational congruence due to [Milner1980]Milner, R.. There, Milner's silent action [IMAGE ]voidtau[IMAGE ]: Milner's silent action is treated as a normal atomic action in the operational rules and its special behaviour is expressed with the equivalence relation: observational congruence. In the case of the empty process a similar approach is reported on by [Koymans and Vrancken1985]Koymans, C.P.J.Vrancken, J.L.M.. In that paper a graph model was constructed featuring the empty process as an ordinary atomic action. A notion called [IMAGE ] bisimulation was defined to express the special behaviour of the empty process. With the approach of [Koymans and Vrancken1985]Koymans, C.P.J.Vrancken, J.L.M. we can use the theory of subsection 2.4.1 to prove the conservativity of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process over BPA voidBPABPA : basic process algebra. We will sketch the idea and leave the details as an exercise to the interested reader. For the operational rules we just take the operational semantics of BPA voidBPABPA : basic process algebra\ where we let a also range over [IMAGE ]. This means that we have, for instance, the rule [IMAGE ]a[IMAGE ]. Note that this adds a new relation [IMAGE ] and a new predicate [IMAGE ]a[IMAGE ] to the operational rules for BPA voidBPABPA : basic process algebra. Now with the aid of theorem 2.4.15 it is not hard to see that this term deduction system is an operationally conservative extension of the term deduction system in table 5. By way of an example we will check the conditions of theorem 2.4.15 for one deduction rule in the extended system:

[IMAGE ]

The crucial place to look at is the left-hand side of the conclusion: x+y. There an original function symbol occurs: +. Now we need to check that this rule is pure and well-founded. This is easy. Also the terms x and x' must be original terms; this is the case since they are variables. And there must be a premise containing only original terms and a new relation or predicate symbol. This is also the case. The other rules are treated equally simply. So, we may apply theorem 2.4.15 and find the operational conservativity. Now this notion termed [IMAGE ] bisimulation can be defined exclusively in terms of relation and predicate symbols. So with theorem 2.4.19 we find that the term deduction system belonging to _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process is an operationally conservative extension up to [IMAGE ] bisimulation equivalence of the term deduction system belonging to BPA voidBPABPA : basic process algebra (note that [IMAGE ] bisimulation becomes normal strong bisimulation for BPA voidBPABPA : basic process algebra\ where no [IMAGE ] is present). Now we can apply the equational conservativity theorem 2.4.24 if we know in addition that the model induced by the operational rules modulo [IMAGE ] bisimulation equivalence is sound with respect to the axioms of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process that we listed in tables 1 and 11. This is shown for the graph model by [Koymans and Vrancken1985]Koymans, C.P.J.Vrancken, J.L.M. and this proof transposes effortlessly to the situation with operational rules that we sketched above. This proves that _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process is a conservative extension of BPA voidBPABPA : basic process algebra.

### Extensions of _()[IMAGE ]

In this subsection we will discuss the extensions of _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] with recursion and/or projections.

#### Recursion

We can add recursion to _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] in exactly the same way as we did for _()[IMAGE ]voidBPAdelta[IMAGE ]: BPA or [IMAGE ]. The equational specification _()[IMAGE ]rec voidBPAdeltaepsilonrec[IMAGE ]: [IMAGE ] with recursion contains the signature of BPA rec voidBPArecBPA rec : BPA with recursion and [IMAGE ]. The axioms are the ones of BPA rec voidBPArecBPA rec : BPA with recursion and the axioms of table 11 (and table 10).

Since [IMAGE ], they cannot serve as a guard. For instance, [IMAGE ] is neither completely guarded nor guarded.

The semantics of _()[IMAGE ]rec voidBPAdeltaepsilonrec[IMAGE ]: [IMAGE ] with recursion can be given by means of a term deduction system [IMAGE ] that has as its signature the signature of _()[IMAGE ]rec voidBPAdeltaepsilonrec[IMAGE ]: [IMAGE ] with recursion and as its rules the ones of [IMAGE ]_()[IMAGE ] plus the rules of table 13. Since bisimulation equivalence is a congruence (2.2.32), we can define the operators of _()[IMAGE ]rec voidBPAdeltaepsilonrec[IMAGE ]: [IMAGE ] with recursion on the quotient algebra of closed _()[IMAGE ]rec voidBPAdeltaepsilonrec[IMAGE ]: [IMAGE ] with recursion terms with respect to bisimulation equivalence. This quotient is a model of _()[IMAGE ]rec voidBPAdeltaepsilonrec[IMAGE ]: [IMAGE ] with recursion and it satisfies RDP voidRDPRDP : recursive definition principle and RSP voidRSPRSP : recursive specification principle.

[IMAGE ]
Table 13: Derivation rules for recursion and empty process.

#### Projection

We extend the theory _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] with projections. The equational specification +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections has as its signature the one of +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections plus a constant [IMAGE ] (and [IMAGE ]). The axioms of +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections are the axioms of +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections plus the axioms of table 11. Moreover, we assume for axiom PR1 (table 7) that a may also be [IMAGE ].

The results that we inferred for +PR [IMAGE ]voidBPAdelta PR[IMAGE ]: [IMAGE ] with projections also hold for +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections: we can eliminate projections occurring in closed terms and the sequence [IMAGE ] has [IMAGE ] as its tail. We can also prove many conservativity results using subsection 2.4.1. We can, for instance, show that +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections is conservative over _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ]. We already showed that _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] is a conservative extension of BPA voidBPABPA : basic process algebra, so with transitivity we find that +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections is a conservative extension of BPA voidBPABPA : basic process algebra. We use the transitivity argument here since the proof that _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] is a conservative extension of BPA voidBPABPA : basic process algebra uses another semantics. See subsection 2.6.1 for more information.

The semantics of +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections can be given by means of a term deduction system [IMAGE ]+PR [IMAGE ]. Its signature is the signature of +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections and its rules are the rules of tables 12 and 14. We can define the quotient algebra of closed +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections terms with respect to bisimulation equivalence and the operators of +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections as usual. The quotient is a model of +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections and it satisfies AIP voidAIPAIP : approximation induction principle. The theory +PR [IMAGE ]voidBPAdeltaepsilon PR[IMAGE ]: [IMAGE ] with projections is complete.

[IMAGE ]
Table 14: Derivation rules for projections with empty process.

#### Recursion and projection

Here we discuss the combination of recursion, projection, and the empty process. The theory +PR [IMAGE ]voidBPAdeltaepsilonrec PR[IMAGE ]: [IMAGE ] with projections has as its signature the signature of +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections and a constant [IMAGE ] (and [IMAGE ]). The axioms of +PR [IMAGE ]voidBPAdeltaepsilonrec PR[IMAGE ]: [IMAGE ] with projections are the ones of +PR [IMAGE ]voidBPAdeltarec PR[IMAGE ]: [IMAGE ] with projections and the axioms of table 11. Moreover, we assume for axiom PR1 (table 7) that a may also be [IMAGE ].

The standard facts (and their proofs) of subsection 2.4.2 are easily translated to the present situation.

The semantics of +PR [IMAGE ]voidBPAdeltaepsilonrec PR[IMAGE ]: [IMAGE ] with projections is given by means of a term deduction system [IMAGE ]+PR [IMAGE ]. Its signature is the signature of +PR [IMAGE ]voidBPAdeltaepsilonrec PR[IMAGE ]: [IMAGE ] with projections and its rules are those of [IMAGE ]+PR [IMAGE ] plus the rules concerning recursion that are presented in table 13. Since bisimulation equivalence is a congruence, we can define the operators of +PR [IMAGE ]voidBPAdeltaepsilonrec PR[IMAGE ]: [IMAGE ] with projections on the quotient algebra of closed +PR [IMAGE ]voidBPAdeltaepsilonrec PR[IMAGE ]: [IMAGE ] with projections terms with respect to bisimulation equivalence. This quotient is a model of +PR [IMAGE ]voidBPAdeltaepsilonrec PR[IMAGE ]: [IMAGE ] with projections and it satisfies RDP voidRDPRDP : recursive definition principle, RSP voidRSPRSP : recursive specification principle, and ^-[IMAGE ]voidAIPmin[IMAGE ]: restricted approximation induction principle, but not its unrestricted version AIP voidAIPAIP : approximation induction principle. As a consequence, we can prove that _()[IMAGE ]rec voidBPAdeltaepsilonrec[IMAGE ]: [IMAGE ] with recursion satisfies RSP voidRSPRSP : recursive specification principle. This is proved in the same way as theorem 2.4.36.

### 2.6.3 CCS termination

A variant of the empty process is given by the CCS voidCCSCCS : communicating concurrent processes process NIL voidNILNIL : a CCS constant\ [Milner1980]Milner, R.. We can extend the signature of BPA voidBPABPA : basic process algebra by the constant NIL voidNILNIL : a CCS constant, and formulate the operational rules in table 15. These rules are taken from [Aceto and Hennessy1992]Aceto, L.Hennessy, M..

[IMAGE ]
Table: Derivation rules of [IMAGE ]_NIL[IMAGE ].

The crucial difference between the necessary termination predicatenecessary termination predicatepredicate!necessary termination [IMAGE ]a[IMAGE ] and the termination option predicate [IMAGE ] is in the rule for +: for [IMAGE ]a[IMAGE ], both components must terminate in order for the sum to terminate. As a result, NIL voidNILNIL : a CCS constant satisfies the laws for [IMAGE ] but at the same time the law [IMAGE ]. A consequence is that the law A4 (distributivity of [IMAGE ] over +) does not hold for all processes, and so _NIL[IMAGE ]voidBPANIL[IMAGE ]: BPA with NIL cannot be axiomatized using the axioms of BPA voidBPABPA : basic process algebra. The following complete axiomatization is taken from [Baeten and Vaandrager1992]Baeten, J.C.M.Vaandrager, F.W.; for more information, we refer to this paper.

[IMAGE ]
Table: _NIL[IMAGE ].

As before, we can add [IMAGE ] without any operational rules. Its axioms have to be adapted in the presence of NIL voidNILNIL : a CCS constant, though. We show this in table 17.

[IMAGE ]
Table 17: [IMAGE ] in the presence of NIL.

## 2.7 Renaming in BPA

Sometimes it is useful to have the possibility of renaming atomic actions. The material of this subsection is based on [Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A. with improvements by [Vaandrager1990a]Vaandrager, F.W.. Renaming operators occur in most concurrency theories; see, for example, [Milner1980, Milner1989]Milner, R., [Hennessy1988]Hennessy, M., and [Hoare1985]Hoare, C.A.R..

The signature of the equational specification [IMAGE ]+RN [IMAGE ] consists of the signature of BPA voidBPABPA : basic process algebra plus for each function f from the set of atomic actions to itself a unary operator [IMAGE ]voidrhof[IMAGE ]: renaming operator called a renaming operatorrenaming operatoroperator!renaming. Such a function fvoidff: renaming function is called a renaming functionrenaming functionfunction!renaming. The axioms of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming are the ones for BPA voidBPABPA : basic process algebra plus the axioms concerning renaming operators displayed in table 18voidRN1-3RN1-3: renaming axioms.

[IMAGE ]
Table 18: Renaming.

#### Structural induction

In +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming we can use structural induction just as in BPA voidBPABPA : basic process algebra, since closed +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming terms can be rewritten into basic BPA voidBPABPA : basic process algebra terms. To that end, we will first prove that the term rewriting system associated to +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming is strongly normalizing. We display the rewrite rules concerning the renaming operators in table 19. Note that, in rule RRN1, f(a) stands for the atomic action that a is renamed into.

[IMAGE ]

With the aid of the above termination result, we can show the elimination theorem for basic process algebra with renaming operators.

[IMAGE ]

[IMAGE ]
Table: A term rewriting system for +RN [IMAGE ].

[IMAGE ]

#### Semantics

We give the semantics for +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming\ by means of a term deduction system [IMAGE ]+RN [IMAGE ], whose signature is the one of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming and whose rules are the rules of tables 5 and 20. Bisimulation equivalence is a congruence, so the quotient of closed +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming terms modulo bisimulation equivalence is well-defined. This means that the operators of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming can be defined on this quotient, which is a model of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming.

[IMAGE ]
Table 20: Derivation rules concerning renaming operators.

[IMAGE ]

At this point we have all the ingredients necessary to state and prove that +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming is a conservative extension of BPA voidBPABPA : basic process algebra.

[IMAGE ]

[IMAGE ]

With the aid of the above conservativity result and the elimination theorem for +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming, we find the completeness of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming.

[IMAGE ]

### Extensions of +RN [IMAGE ]

In this subsection we will discuss the extensions of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming with recursion and/or projections.

#### Recursion

We can add recursion to +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming in the same way as we added recursion to BPA voidBPABPA : basic process algebra. The equational specification +RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming has as its signature the signature of BPA rec voidBPArecBPA rec : BPA with recursion plus for all functions f from A to A a renaming operator [IMAGE ]. The equations of +RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming are the axioms of BPA rec voidBPArecBPA rec : BPA with recursion plus the axioms concerning renaming; see table 18. We can turn the set of closed +RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming terms into a model of +RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming that satisfies RDP voidRDPRDP : recursive definition principle and RSP voidRSPRSP : recursive specification principle as usual.

#### Projection

Projections can be added in an obvious way to +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming: just add the projection functions and their axioms to the equational specification +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming to obtain +PR [IMAGE ]voidBPA RN PR[IMAGE ]: +RN [IMAGE ] with projections. The standard facts that hold for +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections also hold for +PR [IMAGE ]voidBPA RN PR[IMAGE ]: +RN [IMAGE ] with projections. As we did for +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections we can infer that +PR [IMAGE ]voidBPA RN PR[IMAGE ]: +RN [IMAGE ] with projections is sound and complete, and that AIP voidAIPAIP : approximation induction principle is valid.

#### Recursion and projection

The extension with both recursion and projection of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming, called +PR [IMAGE ]voidBPArec RN PR[IMAGE ]: +RN [IMAGE ]\ with projections, can be obtained just like in the case of BPA voidBPABPA : basic process algebra.

### 2.7.2 Renaming in basic process algebra with deadlock

In this subsection we will extend the _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock family with renaming operators. We begin with _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock itself. The equational specification _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming has as its signature the one of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock and for each function [IMAGE ], with [IMAGE ], a unary operator [IMAGE ] called a renaming operator. The axioms of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming are the axioms of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming plus the axioms concerning deadlock; see table 10. We assume for axiom RN1 (table 18) that a ranges over [IMAGE ]. Note that we have [IMAGE ], for all renaming operators. This is necessary: it is easy to derive a contradiction if we allow [IMAGE ] to be renamed into an atomic action.

#### Structural induction

We can use structural induction as before, since closed _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming terms can be rewritten into basic _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock terms. This follows from the next elimination theorem.

[IMAGE ]

[IMAGE ]

#### Semantics

The semantics for _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming can be given just like the semantics for +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming. Let [IMAGE ]_+RN [IMAGE ] be the term deduction system with the signature of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming and with the rules of tables 5 and 20. In the latter table we further assume that [IMAGE ]. Since bisimulation equivalence is a congruence, the quotient of the set of closed _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming terms with respect to bisimulation equivalence is well-defined. This quotient is a model of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming; from this, the completeness of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock, and the elimination result, the completeness of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming follows.

### Extensions of _+RN [IMAGE ] and _[IMAGE ]

In this subsection we discuss the extensions of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming with recursion and/or projections and we discuss the extension of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with a particular renaming operator.

#### Recursion and/or projection

The extensions of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming with recursion, projection, or a combination of both are obtained in the same way as these extensions without deadlock; see section 2.7.1.

#### Encapsulation

In most concurrency theories in which a form of deadlock is present there usually is the notion of an encapsulation or restriction operatorrestriction operatoroperator!restriction; this is a renaming operator that renames certain atomic actions into [IMAGE ]. The notion of encapsulation and the notation [IMAGE ]voiddeltaH[IMAGE ]: encapsulation operator stem from [Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W.. The notion named restriction is due to [Milner1980]Milner, R..

In this subsection we will add the encapsulation operator to _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock.

The equational specification +ð[IMAGE ]voidBPAdelta deltaH[IMAGE ]: [IMAGE ] with encapsulation has as its signature the one of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock plus for each [IMAGE ] a unary operator ð\ called the encapsulation operatorencapsulation operatoroperator!encapsulation. The axioms of +ð[IMAGE ]voidBPAdelta deltaH[IMAGE ]: [IMAGE ] with encapsulation\ are the equations of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock and the equations defining ð in table 21voidD1-4D1-4: encapsulation axioms. We assume in this table that a ranges over [IMAGE ], so in particular we find with D1 that [IMAGE ].

[IMAGE ]
Table 21: The encapsulation operator.

The semantics of +ð[IMAGE ]voidBPAdelta deltaH[IMAGE ]: [IMAGE ] with encapsulation can be derived just like in the case of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming. We can take [IMAGE ] with

[IMAGE ]

For completeness sake, we give the operational rules for the encapsulation operator in table 22.

It is also straightforward to extend +ð[IMAGE ]voidBPAdelta deltaH[IMAGE ]: [IMAGE ] with encapsulation with recursion and/or projections.

[IMAGE ]
Table 22: Derivation rules for the encapsulation operator.

### 2.7.4 Renaming in basic process algebra with empty process

In this subsection we will add renaming operators to both _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty process and _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process with extensions. We will simultaneously refer to both of them as before with parentheses: _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ]. Arbitrary combinations of renaming operators and the empty process introduce a form of abstraction, which is beyond the scope of concrete process algebra. Therefore, we will restrict ourselves to the concrete subcase that prohibits renaming into the empty process.

The signature of the equational specification +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming is the signature of +RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ] with renaming plus a constant [IMAGE ] ([IMAGE ]). We do not allow renaming into [IMAGE ] so for the functions f we assume (moreover) that [IMAGE ] if [IMAGE ] and [IMAGE ] [IMAGE ]. The axioms of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming are the ones of _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] and the equations for renaming; see table 18. Note that [IMAGE ] (and [IMAGE ]).

#### Abstraction

We have an abstractionabstraction mechanism if we allow renaming into the empty process. For instance, suppose that we have two atomic actions, say a and b. Let f(a)=a and [IMAGE ]. Then [IMAGE ] and we have abstracted from b.

#### Structural induction

We can use structural induction as before, since closed +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming terms can be rewritten into basic _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] terms. This can be shown along the same lines as the elimination theorem for the theory without the empty process; see, for instance, theorem 2.7.2.

Note that proposition 2.7.3 also holds for +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming.

#### Semantics

The semantics of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming will be given by means of a term deduction system. Let [IMAGE ]+RN [IMAGE ] be the term deduction system with +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming as its signature and with rules displayed in tables 12 and 23. Bisimulation equivalence is a congruence, so we can define the operators of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming\ on the quotient of closed +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming terms modulo bisimulation equivalence. It is straightforward to prove that this is a model of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming. The completeness of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming is also standard to prove.

[IMAGE ]
Table 23: Derivation rules for renaming operators and empty process.

If we allow renaming into the empty process, we need two more derivation rules that concern renaming; they introduce a look-aheadlook-ahead as can be seen in table 24. The operational rules that we list in this table are due to [Baeten and Glabbeek1987]Baeten, J.C.M.Glabbeek, R.J. van.

We will give an example. Suppose that [IMAGE ] and f(b)=b. Then we can derive [IMAGE ], for each [IMAGE ].

[IMAGE ]
Table: Extra rules when we allow renaming into [IMAGE ].

### Extensions of +RN [IMAGE ] and _()[IMAGE ]

In this subsection we discuss the extensions of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming with recursion and/or projections and we discuss the extension of _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] with a particular renaming operator.

#### Recursion and/or projection

The extensions of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming with recursion and/or projection can be obtained just like before. However, if we allow renaming into the empty process the definition of a guarded recursive specification has to be adapted. We will show in an example that RSP voidRSPRSP : recursive specification principle no longer holds with the present definition. This example is taken from [Baeten et al. 1987]Baeten, J.C.M.Bergstra, J.A.Klop, J.W.. Suppose that we have at least three elements in the set of atomic actions, say a,i, and j. Let [IMAGE ] resp. [IMAGE ] be the renaming operators that rename i resp. j into [IMAGE ] and further do nothing. Then the guarded recursive specification

[IMAGE ]

has the solution [IMAGE ] for all [IMAGE ]. So RSP voidRSPRSP : recursive specification principle cannot hold.

A possible solution can be to prohibit the occurrences of renaming operators in the body of guarded recursive specifications. Also more sophisticated solutions can be obtained in terms of restrictions on the renaming operators that do occur in the body of a guarded recursive specification.

#### Encapsulation

The extension of _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \ with deadlock and empty process with the encapsulation operator can be obtained in the same way as in the case without the empty process; see subsection 2.7.3.

## 2.8 The state operator

In this subsection we extend BPA voidBPABPA : basic process algebra with the (simple) state operator, which is a generalization of a renaming operator. It is a renaming operator with a memory to describe processes with an independent global state. We denote the state operator by [IMAGE ]; the subscript is the memory cell containing the current state s. This subsection is based on [Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A.. Another treatment of state operators can be found in [Verhoef1992]Verhoef, C..

Next, we will discuss the signature of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator. It consists of the usual signature of BPA voidBPABPA : basic process algebra extended with for each [IMAGE ] and [IMAGE ] a unary operator [IMAGE ]voidlambdams[IMAGE ]: simple state operator called the (simple) state operatorsimple state operatoroperator!simple state. MS, and A are mutually disjoint. The set S is the state spacestate space and MvoidMM: set of objects is the set of object namesobject names; the  M stands for machine.

We describe the state operator by means of two total functions actionvoidactionaction: action functionaction functionfunction!action and effectvoideffecteffect: effect functioneffect functionfunction!effect. The function action describes the renaming of the atomic actions and the function effect describes the contents of the memory. We have

[IMAGE ]

Mostly, we write a(m,s) for [IMAGE ] and s(m,a) for [IMAGE ].

Intuitively, we think of the process [IMAGE ] as follows: m represents a machine (say a computer), s describes its state (say the contents of its memory), x is its input (say a program). Now [IMAGE ] describes what happens when x is presented to machine m in state s.

Now we discuss the equations of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operatorvoidSO1-3SO1-3: simple state operator axioms. They are the axioms of BPA voidBPABPA : basic process algebra (see table 1) and the axioms of table 25. The first axiom SO1 gives the renaming part of the state operator. The second axiom SO2 shows the effect of renaming an atomic action on the current state. Note that if a renaming has no effect on states we obtain an ordinary renaming operator. Axiom SO3 expresses that the state operator distributes over the alternative composition.

[IMAGE ]
Table 25: The axioms defining the state operator.

### 2.8.1 Termination and elimination

Next, it is our aim to show that the state operator can be eliminated. Therefore, we will use that the term rewriting system associated to _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator is strongly normalizing. We will prove the latter fact with the aid of the method of the recursive path ordering. However, we cannot apply this method immediately. This is due to the fact that we cannot hope to find a strict partial ordering on the signature of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator\ that does the job. The problematical rule is the rewrite rule RSO2 (see table 26). Suppose that we have one atomic action a. Let us have two different states, which shall remain nameless. Take an inert action function, that is it does nothing, and let the effect function act as a switch. This yields the following instantiation for the rewrite rule RSO2:

[IMAGE ]

For the first rewrite rule the ordering that works is [IMAGE ]. But for the second rule, the ordering should be the opposite, thus yielding an inconsistency. We solve this by giving the state operator a rank; the rank of a state operator depends on the weight of its operand. This idea is taken from [Verhoef1992]Verhoef, C.; he based this idea on a method that [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W. give for the termination of a concurrent system (see theorem 3.2.3 where we treat their method).

[IMAGE ]
Table 26: The rewrite rules for the simple state operator.

[IMAGE ]

[IMAGE ]

[IMAGE ]

Now, we can state the elimination theorem for basic process algebra with the state operator.

[IMAGE ]

#### Semantics

We give the semantics for _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator\ by means of a term deduction system [IMAGE ]_[IMAGE ]. Its signature is that of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator and its rules are the rules of tables 5 and 27. According to theorem 2.2.32 bisimulation equivalence is a congruence so the operators of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator can be defined on the quotient of the closed _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator terms modulo bisimulation equivalence. Moreover, it is a model of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator. With the aid of the method explained in subsection 2.4.1, it is not hard to see that _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator\ is a conservative extension of BPA voidBPABPA : basic process algebra. Then it easily follows with theorem 2.4.26 that the axioms in tables 1 and 25 constitute a complete axiomatization of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator.

[IMAGE ]
Table: Derivation rules of [IMAGE ]_[IMAGE ].

#### Extensions

The extensions of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator with recursion and/or projection are obtained in the same way as those of BPA voidBPABPA : basic process algebra.

The extension of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with the state operator is obtained in the same way as the extension of BPA voidBPABPA : basic process algebra with it. We also allow [IMAGE ] so the action function can rename into [IMAGE ]. There is only one extra axiom: we need to know what the state operator should do with the extra constant [IMAGE ]. Therefore, we need to know how the functions action and effect are extended to [IMAGE ]. We define [IMAGE ] and [IMAGE ]. The extra axiom is

[IMAGE ]

The extensions of _[IMAGE ]voidBPAdeltalambda[IMAGE ]: [IMAGE ] with the simple state operator with recursion and/or projection are obtained in the same way as those of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock.

The following example is due to Alban Ponse [Ponse1993]Ponse, A..

[IMAGE ]

## 2.9 The extended state operator

In the following, we will discuss BPA voidBPABPA : basic process algebra with the extended state operator, which is a generalization of the simple state operator. We denote the extended state operator by [IMAGE ]. The difference with the (simple) state operator is that we can rename an atomic action into a closed term of a particular form, namely a finite sum of atomic actions. With this extra feature it is possible to translate an instruction like read(x) into process algebra.

This subsection is based on [Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A..

We discuss the signature of _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator. It consists of the usual signature of BPA voidBPABPA : basic process algebra extended for each [IMAGE ] and [IMAGE ] with a unary operator [IMAGE ]voidLambdams[IMAGE ]: extended state operator called the extended state operatorextended state operatoroperator!extended state. MS, and A are mutually disjoint. The set S is the state spacestate space and MvoidMM: set of objects is the set of object namesobject names; the  M stands for machine.

We describe the extended state operator by means of two functions action and effect. The function action action functionfunction!action describes the renaming of the atomic actions and the function effect effect functionfunction!effect describes the contents of the memory. We have

[IMAGE ]

We write a(m,s) for [IMAGE ] and s(m,a,b) for [IMAGE ].

[IMAGE ]
Table 28: The axioms defining the generalized state operator.

[IMAGE ]
Table: Derivation rules of [IMAGE ]_[IMAGE ].

The axioms of _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator are those of BPA voidBPABPA : basic process algebra and the axioms of table 28voidGS1-3GS1-3: extended state operator axioms. Next, we discuss them. The first axiom GS1 states that an atomic action is renamed into a sum of atomic actions. Axiom GS2 shows the side effects of the renaming on the state space. Axiom GS3 expresses that the extended state operator distributes over the alternative composition.

#### Termination

In the previous subsection (2.8) we mentioned that we cannot use the method of the recursive path ordering immediately. The same phenomenon occurs with the extended state operator. Fortunately, the solution of the problems is the same as for the simple state operator. We have to define ranked extended state operators and prove the termination of this system. We omit the details and refer to subsection 2.8 for more information. We only mention the main result.

[IMAGE ]
Table 30: The rewrite rules for the extended state operator.

#### Semantics

We give the semantics for _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator\ by means of a term deduction system [IMAGE ]_[IMAGE ]. Its signature is that of _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator and its rules are the rules of tables 5 and 29. According to 2.2.32 bisimulation equivalence is a congruence so the quotient of the closed _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator terms modulo bisimulation equivalence is well-defined. Moreover, it is easily seen that the quotient is a model of _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator. With the theory of section 2.4.1, we find that _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator is a conservative extension of BPA voidBPABPA : basic process algebra. With the termination theorem 2.9.1 and an elimination result, similar to 2.8.4, we find using theorem 2.4.26 that the axioms of tables 1 and 28 constitute a complete axiomatization of _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator.

#### Extensions

The extensions of _[IMAGE ]voidBPALambda[IMAGE ]: BPA with the extended state operator and _[IMAGE ]voidBPAdeltaLambda[IMAGE ]: [IMAGE ] with the extended state operator with recursion and/or projection are obtained in the same way as those with _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator\ and _[IMAGE ]voidBPAdeltalambda[IMAGE ]: [IMAGE ] with the simple state operator. The only difference is that we can now allow [IMAGE ] if in addition we define

[IMAGE ]

As before, we have [IMAGE ].

[IMAGE ]

## 2.10 The priority operator

In this subsection we introduce _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with the priority operator that originates from [Baeten et al. 1986]Baeten, J.C.M.Bergstra, J.A.Klop, J.W..

The signature of the equational specification _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with the priority operatorpriority operatoroperator!priority, _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator, consists of the signature of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock plus a unary operator [IMAGE ]voidtheta[IMAGE ]: priority operator and an auxiliary binary operatorunless operatoroperator!unless [IMAGE ]voidA AAF[IMAGE ]: unless operator pronounced ``unless''. Furthermore, a partial ordering <, called the priority orderingpriority orderingordering!priority on the set of atomic actions A is presumed. The axioms of the equational specification _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator are the usual axioms of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock (see tables 1 and 10) and the axioms of tables 31voidU1-6U1-6: unless axioms and 32voidTH1-3TH1-3: priority axioms. The axioms that we present in these tables make use of [IMAGE ]. We can imagine a system without [IMAGE ] (_[theta][IMAGE ]voidBPAtheta[IMAGE ]: BPA with the priority operator) but such a system has a laborious axiomatization; see [Bergstra1985]Bergstra, J.A. for such an axiomatization.

[IMAGE ]
Table 31: The axioms defining the unless operator.

Next, we will discuss the axioms concerning priority.

The axioms of table 31 define the auxiliary unless operator. It is used to axiomatize the priority operator. The intended behaviour of the unless operator is that the process [IMAGE ] filters out all summands of x with an initial action smaller than some initial action of y. So, one could say that the second argument y is the filter. If, for instance, a>b>c then we want that

[IMAGE ]

To model the filter behaviour we use the constant process [IMAGE ] to rename the unwanted initial actions of x into [IMAGE ]. The axioms U1 and U2 essentially define the mesh of the filter: they say which actions can pass the filter and which cannot. Axiom U3 expresses the fact that the initial actions of y are the same as the initial actions of yz. Axiom U4 says that it is the same to filter the initial actions of x with filter y+z as to filter first the initial actions of x with filter y and filter the result with filter z. Axiom U5 expresses that z is a disposable filter: once in xy the process x is filtered through z, the process y can freely pass. Axiom U6 expresses that filtering a sum is the same as adding the filtered summands.

The priority operator uses the unless operator to filter out the summands with low priority. Thus, the priority operator is invariant under atomic actions and sequential composition. This is expressed in the axioms TH1 and TH2. The priority operator does not distribute over the alternative composition, since in a prioritized sum [IMAGE ] there is an interaction between the restrictions concerning the priorities imposed on each other by x and y, whereas in [IMAGE ] we do not have such an interaction. Axiom TH3 states that the prioritized sum equals the sum of the prioritized summands with the remaining alternatives as filters. So, for instance, we have

[IMAGE ]

[IMAGE ]
Table 32: The axioms defining the priority operator.

#### Intuition

The partial order < is used in order to describe which actions have priority over other actions. If for instance a<b and b and c are not related we want to have that [IMAGE ] and [IMAGE ]. The priority operator thus respects the alternative composition for actions without priority but gives the alternative with the highest priority, in the < hierarchy, if the sum contains prioritized actions. A typical example of a low priority action is an atomic action expressing time-out behaviour: as long as there are alternatives with a higher priority no time-out will be performed within the scope of the priority operator. The priority operator has been used to specify and verify time critical protocols in an untimed setting; see, for instance, [Vaandrager1990b]Vaandrager, F.W..

Next, we list some properties of the unless operator and the priority operator that can be derived from _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator. The first identity expresses that the ordering of filtering does not matter. The second equation expresses that when a process is filtered once, a second application of the same filter has no effect. The third one expresses that a prioritized process [IMAGE ] is automatically filtered with its subprocess x without priority.

[IMAGE ]

[IMAGE ]

Next, we formulate a term rewriting result for basic process algebra with priorities. It states that the term rewriting system associated to _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator is strongly normalizing. To prove this we use the method of the recursive path ordering that we introduced in subsection 2.2.2. We need the lexicographical variant of this method. Note that the rewrite rules concerning the unless operator (table 33) form a conditional term rewriting systemconditional term rewriting systemterm rewriting system!conditionalsystem!conditional term rewriting. We can, however, see the rewrite rules RU1 and RU2 as a scheme of rules; for all a and b there is a rule. So, in fact, this term rewriting system is unconditional. Thus, we may use the method of the recursive path ordering.

[IMAGE ]
Table 33: Rewrite rules for the unless operator.

[IMAGE ]
Table 34: The rewrite rules for the priority operator.

[IMAGE ]

[IMAGE ]

Next, we formulate the elimination theorem for basic process algebra with priorities.

[IMAGE ]

### 2.10.1 Semantics of basic process algebra with priorities

In this subsection we discuss the operational semantics of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator.

The operational semantics of the priority operator can be found in [Baeten and Bergstra1988b]Baeten, J.C.M.Bergstra, J.A.. A more accessible reference is, for instance, [Groote1990b]Groote, J.F. or [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P.. In table 35 we give the characterization presented in [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P.. In [Bol and Groote1991]Bol, R.N.Groote, J.F. we find rules that operationally define the unless operator, essentially as in table 36 (but we follow the approach of [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P.,16ex).

We note that it is possible to operationally characterize the priority operator without the use of the unless operator. The latter one is used for the axiomatization of the priority operator. However, [Bergstra1985]Bergstra, J.A. gives a not so well-known finite axiomatization of the priority operator without the unless operator. Moreover, in this approach the special constant [IMAGE ] is not necessary. For more information on this axiomatization we refer to [Bergstra1985]Bergstra, J.A..

We also note that on the basis of an operational semantics for the priority operator it is possible to find the unless operator in a systematical way. This can be done with the paper [Aceto et al. 1994]Aceto, L.Bloom, B.Vaandrager, F.W. where an algorithm is given to generate a sound and complete axiomatization from a set of operational rules that satisfy a certain SOS format (the so-called GSOS format, see further on).

An interesting point concerning the operational rules of the priority operator and the unless operator is the appearance of negative premises in them. Clearly, such rules do not satisfy the path format. Therefore, in this subsection we will make a third journey to the area of general theory on operational semantics. Next, we will generalize the theory that we already treated in subsection 2.2.3. As a running example we take the operational semantics of basic process algebra with priorities. This subsection is based on [Verhoef1994a]Verhoef, C..

[IMAGE ]
Table 35: Derivation rules for the priority operator.

[IMAGE ]
Table 36: Derivation rules for the unless operator.

In the following definition we generalize the notion of a term deduction system (cf. definition 2.2.19) in the sense that deduction rules may also contain negative premises. [Bloom et al. 1988]Bloom, B.Istrail, S.Meyer, A.R. formulated the first format with negative premises; it is called the GSOS formatGSOS formatformat!GSOS. [Groote1990b]Groote, J.F. generalized this substantially and he proposed the so-called ntyft /ntyxt  formatvoidntyftntyxtntyft /ntyxt : a format.

[IMAGE ]

[IMAGE ]

Next, we formalize the notion when a formula holds in a term deduction system with negative premises.

[IMAGE ]

The purpose of a term deduction system is to define a set of positive formulas that can be deduced using the deduction rules. For instance, if the term deduction system contains only positive formulas then the set of deducible formulas comprises all the formulas that can be proved by a well-founded proof tree. If we allow negative formulas in the premises of a deduction rule it is no longer obvious which set of positive formulas can be deduced using the deduction rules. [Bloom et al. 1988]Bloom, B.Istrail, S.Meyer, A.R. formulate that a transition relation must agree with a transition system specification. We will use their notion; it is only adapted in order to incorporate predicates.

[IMAGE ]

[Groote1990b]Groote, J.F. showed that if for each rule the conclusions are in some sense more difficult than the premises, there is always a set of formulas that agrees with the given rules. [Verhoef1994a]Verhoef, C. generalized this to the case where predicates come into play. Next, we will formalize this notion that is termed a stratification.

[IMAGE ]

[IMAGE ]

Next, it is our aim to define a set of positive formulas that agrees with a given term deduction system. Therefore, we will use the following notion. Just think of it as a uniform upper bound to the number of positive premises in a given term deduction system. In general, it is not the least upper bound.

[IMAGE ]

[IMAGE ]

Next, we will define this set of positive formulas for which it can be shown that it agrees with a given term deduction system. This definition originates from [Groote1990b]Groote, J.F. and is adapted to our situation by [Verhoef1994a]Verhoef, C..

[IMAGE ]

The next theorem is taken from [Verhoef1994a]Verhoef, C. but its proof is essentially the same as a similar theorem of [Groote1990b]Groote, J.F.. It states that for a stratifiable term deduction system the set that we defined above agrees with it. Moreover, this is independent of the choice of the stratification.

[IMAGE ]

[IMAGE ]

So, now we only know that when a term deduction system has a stratification there exists some set of positive formulas that agrees with it. Next, we are interested in the conditions under which strong bisimulation equivalence is a congruence relation. Just as in subsection 2.2.3 we define a syntactical restriction on a term deduction system. We will generalize the path format to the so-called panth format, which stands for ``predicates and ntyft /ntyxt hybrid format''. The ntyft /ntyxt  formatntyft/ntyxt formatformat!ntyft/ntyxt stems from [Groote1990b]Groote, J.F..

[IMAGE ]

[IMAGE ]

Next, we define the notion of strong bisimulation for term deduction systems with negative premises. In definition 2.2.28 we gave the positive case. This definition is based on [Park1981]Park, D.M.R. and its formulation is taken from [Verhoef1994a]Verhoef, C..

[IMAGE ]

At this point we have all the ingredients that we need to formulate the theorem that is interesting for our purpose: the congruence theorem for the panth format. It states that in many situations strong bisimulation equivalence is a congruence. The congruence theorem is taken from [Verhoef1994a]Verhoef, C. albeit that there the well-founded subcase is proved. [Fokkink1994]Fokkink, W.J. showed that this condition is not necessary. Thus, we dropped the extra assumption.

[IMAGE ]

According to the above example we find that the quotient of the closed _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator terms modulo bisimulation equivalence is well-defined; this means that the operators of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator can be defined on this quotient. By a straightforward proof we can show that it is a model of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator.

We postpone the proof of the completeness of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator until we have shown that it is a conservative extension of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock.

### 2.10.2 Conservativity

In this subsection we take care of the conservativity of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\ over BPA voidBPABPA : basic process algebra. We are used to proving this via the conservativity theorem for the path format but since the operational rules of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\ do not fit this format, we cannot simply apply this theorem. Just as with the conservativity of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator (see subsection 2.10.1) over BPA voidBPABPA : basic process algebra we will generalize below the theory that we already treated on conservativity--yet another trip into the general theory on operational semantics. This time we will mainly extend the theory of section 2.4.1 so that we can also deal with negative premises. This subsection is based on [Verhoef1994b]Verhoef, C..

Since we treated some theory on negative premises and some theory on conservative extensions, their combination will be not too much work. We have to update the notions of pure, well-founded, and operationally conservative extension. Then only the operationally conservative extension theorem for the path format needs a little modification.

Below, we give the update of the notion pure. It was defined in the positive case in definition 2.2.31.

[IMAGE ]

[IMAGE ]

Now, we update the definition of well-founded. This notion is defined in definition 2.4.13 for the positive case. The update is in the same vein as the one for the purity.

[IMAGE ]

[IMAGE ]

Next, we update the notion of an operationally conservative extension. Also this definition does not look very different from its positive counterpart. Note that in the positive case proofs are well-founded trees, whereas in the negative case we use the notion of agreeing with. More information on this can be found in subsection 2.10.1. We also refer to this subsection for the definition of stratifiability.

[IMAGE ]

Now we have all the updates of the definitions that we need in order to state the operationally conservative extension theorem for the panth format. The following theorem is taken from [Verhoef1994b]Verhoef, C..

[IMAGE ]

In the above example we have shown the operational conservativity of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator over BPA voidBPABPA : basic process algebra. We are in fact interested in the equational conservativity. The other theorems, in particular the equationally conservative extension theorem, that we treated in subsection 2.4.1, do not need any updates, since in those theorems we only refer to term deduction systems and we do not specify which ones. [Verhoef1994b]Verhoef, C. showed that these theorems hold for term deduction systems with negative premises.

So, we can formulate and prove the following theorem.

[IMAGE ]

[IMAGE ]

Now that we have the conservativity result, the completeness of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator follows more or less from the completeness of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock. We will see this in the following theorem.

[IMAGE ]

[IMAGE ]

### Extensions of _[theta][IMAGE ]

In this subsection we discuss extensions of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator with the notions of recursion, projections, renaming, and/or the encapsulation operator, and the state operator. In fact, all extensions but the one with recursion can be obtained just as for the BPA voidBPABPA : basic process algebra or _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock case.

#### Recursion

The problem with the extension of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\ with recursion is purely technical. Since there are negative premises in the operational characterization of the priority and unless operators, we introduced the notion of a stratification to ensure that the semantical rules indeed define a transition relation. We recall that in example 2.10.10 we give a stratification for the operational semantics of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator. The map defined there counts the total number of occurrences of [IMAGE ] and [IMAGE ]. This approach no longer works in the presence of the operational rules for recursion that we presented in table 6. We illustrate this with a simple example. Suppose that we have the following recursive specification:

[IMAGE ]

In this case, the operational rule takes the form

[IMAGE ]

So with the above stratification we have that the stratification of the premise is not less than or equal to the stratification of the conclusion. To solve this problem we use infinite ordinals. We adapt the stratification as follows:

[IMAGE ]

where n is the number of unguarded occurrences of [IMAGE ] and m is the total number of occurrences of [IMAGE ] and occurrences of [IMAGE ] (so the m part is the original stratification). With the modified stratification, the problem is solved. We leave it as an exercise to the reader to check the details.

#### Projection

The extension of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator with projection is obtained in the same way as this extension for BPA voidBPABPA : basic process algebra; see subsection 2.4.

#### Renaming and encapsulation

It is straightforward to extend the equational specification _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator with renaming operators or the encapsulation operator; cf. subsection 2.7.3.

#### State operator

The extension of the theory _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\ with either the simple or extended state operator is obtained in the same way as for the theory BPA voidBPABPA : basic process algebra; see subsections 2.8 and 2.9.

#### Inconsistent combinations

Remarkably, if we combine recursion with the equational specification _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator plus renaming operators we will find an inconsistency. [Groote1990b]Groote, J.F. gives the following example. Take a renaming function f such that
• f(b)=a,
• f(a)=c,
• f(d)=d for all [IMAGE ].
Consider the recursive equation

[IMAGE ]

Now it can be shown that

[IMAGE ]

if we take a>b as the partial ordering on the atomic actions.

Observe also that the combination of recursion with _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator plus state operators is inconsistent since state operators are a generalization of renamings.

## 2.11 Basic process algebra with iteration

In this subsection we extend basic process algebra with an iterative construct. This construct is, in fact, Kleene's star operator, a binary infix operator denoted *. We will call this operator Kleene's binary star operator, since there are two versions of Kleene's star operator: one unary and one binary. The binary construct originates from [Kleene1956]Kleene, S.C. and its more commonly known unary version is due to [Copi et al.1958]Copi, I.M.Elgot, C.C.Wright, J.B.. This subsection is based on the papers [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A. and [Fokkink and Zantema1994]Fokkink, W.J.Zantema, H..

We want to note that using iteration we can also define infinite processes. We already discussed recursion, the standard way to define infinite processes, in subsection 2.3. The advantage of the approach that we explain in this subsection is that there is no need for proof rules like the recursive definition principle or the recursive specification principle, to guarantee that a recursive specification has a possibly unique solution. In this setting, the recursive construct is just some binary operator that we may add to a process language.

#### The theory

The equational specification ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration consists of the signature of BPA voidBPABPA : basic process algebra and a binary infix operator *voidA AAG*: Kleene's binary star operator, called Kleene's binary star operatorKleene's binary star operatoroperator!Kleene's binary star. Its equations are the ones of BPA voidBPABPA : basic process algebra plus the axioms in table 37voidBKS!-3BKS1-3: iteration axioms.

[IMAGE ]
Table 37: The axioms defining Kleene's binary star operator.

We will comment on these axioms. The first one BKS1 is the defining equation for the star operator that [Kleene1956]Kleene, S.C. gives in the context of finite automata. Only the notation is adapted to the present situation. The second equation originates from [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A.; it is a simple equation needed for the completeness. The third axiom BKS3 is more sophisticated; it stems from [Troeger1993]Troeger, D.R.. Troeger used this equation for a slightly different process specification formalism.

Next, we will show some properties that can be derived from the equational specification ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration. For instance, if we apply Kleene, S.C.Kleene's axiomKleene's axiomaxiom!Kleene's to the first term in the display below we find a term to which we can apply Troeger, D.R.Troeger's axiomTroeger's axiomaxiom!Troeger's with x+y substituted for y. Thus, this yields the following identity:

[IMAGE ]

The next identity expresses that applying the star operator in a nested way for the same process reduces to applying it once. First, we apply Kleene's axiom, then we use the idempotence of the alternative composition, then we use Troeger's identity, and then one application of idempotence finishes the calculation. We display this below.

[IMAGE ]

#### Semantics

We give the semantics of the equational specification ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration by means of a term deduction system [IMAGE ]^*[IMAGE ]. Its signature is the signature of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration. Its deduction rules are the rules for BPA voidBPABPA : basic process algebra that we met many times before (see table 5) plus the rules that characterize Kleene's binary star operator. We list them in table 38.

[IMAGE ]
Table 38: Operational rules for Kleene's binary star operator.

[IMAGE ]

[IMAGE ]

It is easy to see that ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration is a conservative extension of BPA voidBPABPA : basic process algebra; see subsection 2.4.1. However, we cannot eliminate Kleene's binary star operator. See subsection 2.14 where we discuss expressivity results. This can be easily seen as follows. Call a term deduction system T operationally terminating if there are no infinite reductions

[IMAGE ]

possible. It is easy to see by inspection of the operational rules for BPA voidBPABPA : basic process algebra that its term deduction system is operationally terminating (cf. lemma 2.2.36 where a ``weight'' function is defined). It is also easy to see that the term deduction system belonging to ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration is not operationally terminating. We have, for instance, the infinite reduction

[IMAGE ]

Now suppose that Kleene's binary star operator can be eliminated in favour of the operators of BPA voidBPABPA : basic process algebra. Then [IMAGE ] must be bisimilar to a BPA voidBPABPA : basic process algebra term, say t. Because of the bisimilarity with [IMAGE ] we must have that t can mimic the above steps that [IMAGE ] is able to perform. So t must have an infinite reduction. This contradicts the fact that the semantics of BPA voidBPABPA : basic process algebra is operationally terminating.

As a corollary, we cannot use the completeness theorem 2.4.26 to prove the completeness of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration. The proof that our axiomatization is nevertheless complete is due to [Fokkink and Zantema1994]Fokkink, W.J.Zantema, H. and is beyond the scope of this chapter. The reason for this is that the proof makes use of a sophisticated term rewriting analysis. Below, we will list their main result.

[IMAGE ]

[IMAGE ]

#### Extensions of ^*[IMAGE ]

The extension of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration with deadlock (^*[IMAGE ]voidBPAdeltastar[IMAGE ]: [IMAGE ] with iteration) is as usual. This system is obtained by taking the syntax of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock plus Kleene's binary operator *. The axioms of ^*[IMAGE ]voidBPAdeltastar[IMAGE ]: [IMAGE ] with iteration are the ones of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration plus those for deadlock.

Since ^*[IMAGE ]voidBPAdeltastar[IMAGE ]: [IMAGE ] with iteration is more expressive (see subsection 2.14) than ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration we cannot use the usual machinery to prove basic properties such as completeness. There is no completeness result for the system ^*[IMAGE ]voidBPAdeltastar[IMAGE ]: [IMAGE ] with iteration so we will not discuss the extensions of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration\ (or ^*[IMAGE ]voidBPAdeltastar[IMAGE ]: [IMAGE ] with iteration) with the notions that we usually extend our systems with. Moreover, at the time of writing this survey the only studied extensions of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration are those with abstraction, fairness principles, deadlock, and parallel constructs. We will discuss some of these extensions after we have introduced such parallel constructs.

## 2.12 Basic process algebra with discrete relative time

Now, we treat an extension of BPA voidBPABPA : basic process algebra with a form of discrete relative time; we abbreviate this as _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time. We speak of discrete time since the system works with so-called time slices. It is called relative since the system refers to the current time slice, the next time slice, and so on. _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time stems from [Baeten and Bergstra1992a]Baeten, J.C.M.Bergstra, J.A.. For other approaches to discrete time process algebra we refer to [Moller and Tofts1990]Moller, F.Tofts, C.M.N. and [Nicollin and Sifakis1994]Nicollin, X.Sifakis, J..

#### Theory

The equational specification _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time has as its signature the one of BPA voidBPABPA : basic process algebra and a unary function called discrete time unit delaydiscrete time unit delaytime!discrete, which is denoted [IMAGE ]voidsigmad[IMAGE ]: discrete time unit delay. The [IMAGE ] is some fixed symbol, which is a measure for the delay. The axioms of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time are the ones of BPA voidBPABPA : basic process algebra that we listed in table 1 plus the equations defining the discrete time unit delay; see table 39voidDT1-2DT1-2: [IMAGE ] axioms.

[IMAGE ]
Table 39: The axioms defining the discrete time unit delay.

We denote the atomic action a in the current time slice by [IMAGE ]voida[IMAGE ]: a in the current time slice. We distinguish [IMAGE ] from a because also other embeddings of BPA voidBPABPA : basic process algebra\ into _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time are possible, where a is interpreted as a occurs at some time, that is, we have [IMAGE ]. The intended interpretation of the unary operator [IMAGE ] is that it pushes a process x to the next time slice. The length of a time slice is measured with the positive real [IMAGE ]. This is operationally expressed by the rule [IMAGE ], where [IMAGE ] is a special relation that describes the pushing behaviour. Note that the label [IMAGE ] is not part of the signature of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time.

Axiom DT1 is called ``time factorizing axiomtime factorizing axiomaxiom!time factorizing''. It expresses that the passage of time by itself cannot determine a choice. We note that the form of choice here is called ``strong choicestrong choicechoice!strong'' (the other two approaches mentioned above have weak choiceweak choicechoice!weak), so in [IMAGE ] both a in the current time slice and b in the next time slice are possible. We do have in the closed term above that by moving to the next time slice, we disable a.

Next, we will show that the term rewriting system associated to _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time\ is terminating. Although this result has importance of its own, we cannot use it to prove an elimination result. For the discrete time unit delay cannot be eliminated.

[IMAGE ]
Table 40: The rewrite rules for the discrete time unit delay.

[IMAGE ]

Now that we know that the term rewriting system associated to _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time\ is terminating, we discuss what form the normal forms can take. Following [Baeten and Bergstra1992a]Baeten, J.C.M.Bergstra, J.A., we define these normal forms, called basic terms.

[IMAGE ]

Next, we formulate some facts from [Baeten and Bergstra1992a]Baeten, J.C.M.Bergstra, J.A.. They can be easily proved.

#### Semantics

Next, we formally define the semantics by way of a term deduction system for _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time. The signature of this system consists of the one for the equational specification _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time. The deduction rules are those for + and [IMAGE ] of BPA voidBPABPA : basic process algebra in table 1, and the rules for constants and the discrete time unit delay in table 41.

[IMAGE ]
Table 41: The operational semantics for the discrete time unit delay.

Note the appearance of negative premises in the operational rules. By means of the theory that we discussed in subsection 2.10.1, we can find that this system indeed defines a set of positive formulas. We recall that we, therefore, have to find a stratification. Let n be the number of + signs that occurs in a closed _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time term t. Then we define a stratification S by assigning to [IMAGE ] and to [IMAGE ]a[IMAGE ] the number n. For the other formulas [IMAGE ] we simply define [IMAGE ]. It is not hard to see that this function is a stratification. So the term deduction system is well-defined.

It is easy to see that the deduction rules are in panth format (see subsection 2.10.1), so we find with theorem 2.10.19 that strong bisimulation equivalence is a congruence.

[IMAGE ]

[IMAGE ]

Next, we formulate a conservativity result for _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time.

[IMAGE ]

[IMAGE ]

### Extensions of _dt[IMAGE ]

We will only discuss the extension of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time with deadlock and recursion. We will not treat the other extensions that we usually have. The reason for this is that at the time of writing this survey these have not been formulated.

First, we will discuss how to extend _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time with deadlock and then we discuss the extension with recursion.

#### Recursion

The extension of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time with recursion has the same technical problem as the extension of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator with recursion. We recall that the problem is that we need to define a new stratification on the operational rules of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time with recursion in order to guarantee that the transition relation is well-defined. For a solution we refer to subsection 2.10.3 where extensions of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\ are discussed.

## 2.13 Basic process algebra with other features

When we want to describe parallel or distributed systems, the most important extensions are the ones with some form of parallel composition. We devote section 3 to such extensions. Below, we list a number of other extensions that we will not cover in this survey. We remark that this list is incomplete and in random order.

#### Abstraction

In this survey we only treat concrete process algebra, hence any extension of the systems that we discuss with some notion of abstractionabstraction will not be covered by this survey. For more information on process algebras that incorporate abstraction we mention [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W. that treats an extension of BPA voidBPABPA : basic process algebra with abstraction. Other systems that feature abstraction are CCS voidCCSCCS : communicating concurrent processes [Milner1980, Milner1989]Milner, R., Hennessy's system [Hennessy1988]Hennessy, M., and CSP voidCSPCSP : communicating sequential processes\ [Hoare1985]Hoare, C.A.R.. We note that the latter two systems are not extensions of BPA voidBPABPA : basic process algebra but treat basic notions in a different way. But also CCS voidCCSCCS : communicating concurrent processes is not an extension of BPA voidBPABPA : basic process algebra because there is no sequential composition in CCS voidCCSCCS : communicating concurrent processes.

There are many other process algebras (with abstraction) such as CIRCAL voidCIRCALCIRCAL : a process calculus\ [Milne1983]Milne, G.J., MEIJE voidMeijeMEIJE : a process algebra [Austry and Boudol1984]Austry, D.Boudol, G., SCCS voidSCCSSCCS : Synchronous CCS [Milner1983]Milner, R., and the -calculus[IMAGE ]voidpi calculus-calculus[IMAGE ]: higher order process calculus [Milner et al. 1992]Milner, R.Parrow, J.Walker, D. to mention some.

#### Backtracking

A well-known notion in logic programming is backtrackingbacktracking. [Bergstra et al. 1994c]Baeten, J.C.M.Ponse, A.Wamel, J.J. van extended process algebra with this notion. They discuss an algebraic description of backtracking by means of a binary operator. For more details on this extension we refer to [Bergstra et al. 1994c]Baeten, J.C.M.Ponse, A.Wamel, J.J. van.

#### Combinatory logic

In [Bergstra et al. 1994b]Bergstra, J.A.Bethke, I.Ponse, A., process algebra is extended with combinatory logiccombinatory logic. An interesting point of this combination is the possibility to verify the well-known alternating bit protocol without any conditional axiom, that is, the verification is purely equational. For more information on this combination and the equational verification we refer to [Bergstra et al. 1994b]Bergstra, J.A.Bethke, I.Ponse, A..

#### Real-time

In recent years, much effort has been spent on the extension of several process algebras with a notion of time. We discuss in this survey just one such extension: process algebra with relative discrete time. However, there are many more (concrete) extensions present in the literature. We mention the distinction between relative and absolute time, and the choice of the time domain: discrete or dense. We refer to [Klusener1993]Klusener, A.S. for more information on real timereal timetime!real process algebra in many and diverse forms.

#### Real-space

In [Baeten and Bergstra1993]Baeten, J.C.M.Bergstra, J.A. a form of real time process algebra is extended with real spacereal space. The paper surveys material from former reports on this topic. We refer the interested reader to [Baeten and Bergstra1993]Baeten, J.C.M.Bergstra, J.A. for more information.

#### Nesting

In this survey, we discuss the extension of process algebra with iteration, or Kleene's binary star. An extension that we do not discuss is one with an operator called the nestingnesting operatoroperator!nesting operator. Like Kleene's binary star operator, the nesting operator also is a recursive operator (though it defines irregular recursion). We refer to [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A. for more information on this topic.

#### Signals

In [Baeten and Bergstra1992b]Baeten, J.C.M.Bergstra, J.A. process algebra is extended with stable signalsstable signalsignal!stable. These are attributes of states of a process. They introduce a signal insertionsignal insertion operatoroperator!signal insertion and a signal termination operatorsignal termination operatoroperator!signal termination to be able to describe signals with a certain duration. A typical example that can be described with this theory is a traffic light system. For more information on the extension with signals we refer to [Baeten and Bergstra1992b]Baeten, J.C.M.Bergstra, J.A..

#### Conditionals

An extension with conditionals or guards can be found in the just mentioned paper [Baeten and Bergstra1992b]Baeten, J.C.M.Bergstra, J.A.. They introduce an if-then-elseif-then-else operator operator in the notation of [Hoare et al. 1987]Hoare, C.A.R.Hayes, I.J.He, JifengMorgan, C.C.Roscoe, A.W.Sanders, J.W.Sorensen, I.H.Spivey, J.M.Surfin, B.A.. [Baeten and Bergstra1992b]Baeten, J.C.M.Bergstra, J.A. also introduce a variant of this conditional operator, called the guarded commandguarded commandcommand!guarded that originates from [Baeten et al. 1991]Baeten, J.C.M.Bergstra, J.A.Mauw, S.Veltink, G.J.. [Groote and Ponse1994]Groote, J.F.Ponse, A. developed a substantial amount of theory for a similar conditional construct called a guardguard.

For more information on the extension of BPA voidBPABPA : basic process algebra with conditional constructs we refer to the above papers.

#### Invariants and assertions

Often, it is useful to have a connection between algebraic expressions and expressions in a logical language. Logical formulas can be used to express invariants ,16ex(see [Bezem and Groote1994]Bezem, M.Groote, J.F.,16ex) or as assertions ,16ex(see [Ponse1991]Ponse, A.,16ex).

#### Probabilities

Often, systems exhibit behaviour that is probabilistic or statistical in nature. For example, one may observe that a faulty communication link drops a message 2% of the time. Algebraic formulations of probabilistic behaviour can be found in [Baeten et al. 1992]Baeten, J.C.M.Bergstra, J.A.Smolka, S.A., [Giacalone et al. 1990]Giacalone, A.Jou, C.-C.Smolka, S.A., [Larsen and Skou1992]Larsen, K.G.Skou, A., and [Tofts1990]Tofts, C.M.N., to mention some.

## 2.14 Decidability and expressiveness results in BPA

In this subsection we briefly mention decidability and expressiveness issues for the family of process algebras that we have introduced thus far.

### 2.14.1 Decidability

In our case, the decidabilitydecidability problems concern the question whether or not two finitely specified processes in, for instance BPA rec voidBPArecBPA rec : BPA with recursion, are bisimilar; see [Baeten et al. 1993]Baeten, J.C.M.Bergstra, J.A.Klop, J.W., [Caucal1990]Caucal, D., and [Christensen et al. 1992]Christensen, S.Hüttel, H.Stirling, C.. Informally, we refer to this as the question whether or not BPA rec voidBPArecBPA rec : BPA with recursion is decidable. It turns out that BPA rec voidBPArecBPA rec : BPA with recursion is decidable for all guarded processes; see [Christensen et al. 1992]Christensen, S.Hüttel, H.Stirling, C.. For almost all extensions of BPA voidBPABPA : basic process algebra the decidability problem is open. Only for some extensions of BPA rec voidBPArecBPA rec : BPA with recursion with the state operator we have some information at the time of writing this survey. We refer the interested reader to [Baeten and Bergstra1991]Baeten, J.C.M.Bergstra, J.A. and [Blanco1995]Blanco, J.O. for more details on the systems [IMAGE ]voidlambdaBPAdeltarec[IMAGE ]: [IMAGE ] not allowed in recursion and [IMAGE ]_[IMAGE ]voidBPAdeltalambda[IMAGE ]_[IMAGE ]: _[IMAGE ]voidBPAdeltalambda[IMAGE ]: [IMAGE ] with the simple state operator with recursion and their decidability problems.

The following theorem is taken from [Christensen et al. 1992]Christensen, S.Hüttel, H.Stirling, C.. The proof of this theorem is beyond the scope of this survey.

[IMAGE ]

### 2.14.2 Expressiveness

For the family of systems that we introduced it is natural to address the question of expressivityexpressivity. The result that is known states that BPA rec voidBPArecBPA rec : BPA with recursion can express non-regular processes. So, we first need to know what exactly are regular processes. This well-known definition is formulated below and is taken from [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P.. Roughly, a process is regular if it has a finite graph.

First, we define when a process is regular in some model.

Next, we define when a guarded recursive specification is linear. It will turn out that a regular process can always be specified by a finite linear specification.

[IMAGE ]

[IMAGE ]

[IMAGE ]

Next, we show that there is a non-regular process that is finitely expressible in the theory BPA rec voidBPArecBPA rec : BPA with recursion, namely a counter.

[IMAGE ]
Figure: The deduction graph of the counter C.

#### Recursion versus iteration

In subsection 2.3 we discussed the extension of BPA voidBPABPA : basic process algebra with recursion. In subsection 2.11 we discussed a similar construct: iteration. We can compare both approaches in the following sense: ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration is less expressive than BPA lin voidBPAlinBPA lin : BPA with finite linear recursion. BPA lin voidBPAlinBPA lin : BPA with finite linear recursion is BPA rec voidBPArecBPA rec : BPA with recursion where only finite linear specifications are allowed[+]. In other words, ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration does not contain non-regular processes. In [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A. a simple example is given that shows the strictness of the inclusion. Consider the following regular process:

[IMAGE ]

In figure 7 we give the graph that belongs to this process. This process is not definable in ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration. In the next theorem we summarize the results. For the proof we refer to [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A..

[IMAGE ]
Figure 7: The deduction graph of a regular process.

[IMAGE ]

# 3 Concrete concurrent processes

Up to now, we have discussed the language BPA voidBPABPA : basic process algebra with many of its extensions. Next, we want to discuss an extension of such significance that we devote a new section to it. It is the notion of parallelism or concurrency that we add to our family of basic systems that we treated in the previous section. We will restrict ourselves to concrete concurrency; that is, we do not consider abstraction.

We follow the ACP voidACPACP : algebra of communicating processes approach of [Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W.. For other approaches to concurrency we refer to Milner's CCS voidCCSCCS : communicating concurrent processes [Milner1980, Milner1989]Milner, R., [Hennessy1988]Hennessy, M., and Hoare's CSP voidCSPCSP : communicating sequential processes\ [Hoare1985]Hoare, C.A.R..

## 3.1 Introduction

In this section, we first extend the BPA voidBPABPA : basic process algebra family with a parallel construct without interaction; that is, processes can be put in parallel by means of this operator but they cannot communicate with each other. This system is called PA voidPAPA : process algebra. Then we will extend this theory with extensions that we discussed in the case of BPA voidBPABPA : basic process algebra (and new extensions). It will turn out that in most cases the extensions can be obtained in the same way as in the BPA voidBPABPA : basic process algebra case.

Secondly, we extend the parallel construct itself such that communication between parallel processes is also possible, that is, we discuss the system ACP voidACPACP : algebra of communicating processes. Then we discuss extensions of ACP voidACPACP : algebra of communicating processes, which is in most cases an easy job since they can be obtained in the same way as the extensions for BPA voidBPABPA : basic process algebra.

Finally, we discuss decidability and expressiveness issues for various systems.

## 3.2 Syntax and semantics of parallel processes

In this subsection we will describe the syntax and semantics of concrete concurrent processes.

### 3.2.1 The theory PA

We will discuss the equational theory [IMAGE ]. This section is based on [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W..

The signature [IMAGE ] consists of the signature of BPA voidBPABPA : basic process algebra plus two binary operators [IMAGE ]voidA AACmerge[IMAGE ]: parallel composition and [IMAGE ]voidA AADmerge[IMAGE ]: left merge. The operator [IMAGE ] is called (free) mergemergemerge!freefree merge or parallel compositionparallel compositioncomposition!parallel and the operator [IMAGE ] is called left mergeleft mergemerge!left. The left merge was introduced in [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W. in order to give a finite axiomatization for the free merge. [Moller1989]Moller, F. proved that it is impossible to give a finite axiomatization of the merge without an auxiliary operator.

The set of equations [IMAGE ] consists of the equations of BPA voidBPABPA : basic process algebra\ in table 1 and the axioms concerning the merge in table 42voidM1-4M1-4: axioms for the free merge. We assume in this table that a ranges over the set of atomic actions. So axioms M2 and M3 are in fact axiom schemes: for each atomic action there are axioms M2 and M3.

We assume that sequential composition binds stronger than both merges and they in turn bind stronger than the alternative composition. So, for instance, the left-hand side of M3 stands for [IMAGE ] and the brackets in the left-hand side of M4 are necessary.

#### Intuition

Before we provide the semantics of PA voidPAPA : process algebra, we give an intuitive meaning to the non-BPA voidBPABPA : basic process algebra part of PA voidPAPA : process algebra: the part concerning both merges. We already discussed the BPA voidBPABPA : basic process algebra part informally in 2.2.1. We recall that we consider the execution of an atomic action to occur at (or to be observed at) a point in time. We start with the signature and then we treat the axioms.

We think of the merge of two processes x and y as the process that executes both x and y in parallel. We think of the left merge of x and y as precisely the same, with the restriction that the first step of the process [IMAGE ] comes from its left-hand side x. We disregard the simultaneous execution of atomic actions here (but see subsection 3.5 where communication comes into play). This leads to the so-called interleavinginterleaving view, which clarifies the behaviour of the left merge.

This intuition clarifies that axiom M1 is defined in terms of the left merge: the merge of two processes starts either with the left-hand side or with its right-hand side.

The remaining axioms M2-4 define the left merge following the structure of basic terms.

The parallelism in axiom M2 collapses into sequential composition since the first step at the left-hand side is also the last one. After the first step in M3, we obtain full parallelism for the remainders. Axiom M4 simply says that the left merge distributes over the alternative composition. Note that, in general, [IMAGE ][IMAGE ][IMAGE ][IMAGE ]. So, here we describe an interleaving parallel compositioninterleaving parallel compositionparallel composition!interleavingcomposition!parallel!interleaving. Also, other forms of parallel composition can be formulated. We already mentioned interleaving extended with simultaneous execution, to be discussed from subsection 3.5 on, but also want to mention so-called synchronous parallel compositionsynchronous parallel compositionparallel composition!synchronouscomposition!parallel!synchronous, by which we can describe clocked systemsclocked systemsystem!clocked, where all components proceed in lock-steplock stepstep!lock. A well known process algebra with synchronous parallel composition is SCCS voidSCCSSCCS : Synchronous CCS \ [Milner1983]Milner, R., two references using the present framework are [Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W. and [Weijland1989]Weijland, W.P..

[IMAGE ]
Table 42: Axioms for the free merge.

#### Structural induction

We can use structural induction for PA voidPAPA : process algebra as before for BPA voidBPABPA : basic process algebra, since basic PA voidPAPA : process algebra terms are just basic BPA voidBPABPA : basic process algebra terms. This follows immediately from the theorem to follow (theorem 3.2.4). It states that parallel composition can be eliminated from closed PA voidPAPA : process algebra terms.

[IMAGE ]
Table: A term rewriting system for PA.

#### Termination

Next, it is our aim to prove that the term rewriting system associated to the equational specification PA voidPAPA : process algebra is strongly normalizing. In subsection 2.2.2 we already discussed the powerful method of the recursive path ordering. Indeed, we will use this method to prove the desired result but we cannot apply it immediately. We recall that the termination problem more or less reduces to finding the appropriate strict partial ordering on some operators in the signature. The problem that we have with this particular system is that we cannot define a consistent partial ordering on the elements of the signature. First, we will explain this problem and then we will see that a possible solution can be obtained in the same way as for the termination of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with the simple state operator; see section 2.8.1. The problematical pair consists of the rules [IMAGE ]. Analysing this pair we find that if we take the rule RM1 on the one hand, the ordering that does the job is [IMAGE ][IMAGE ]. On the other hand, if we look at RM3, the right choice is the other way around: [IMAGE ][IMAGE ]. This particular problem is tackled by [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W.. More detailed information on this problem can be found in a survey on term rewriting that appeared in this series [Klop1992, remark 4.11,16ex(ii,16ex),]Klop, J.W.. The idea of [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W. was to equip the operators [IMAGE ][IMAGE ] and [IMAGE ] with a rank. Thus yielding a ranked signature for which it is possible to define the desired strict partial ordering. To formalize the ranked signature we first need a notion termed ``weight''. Its definition stems from [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W.. Note that we already defined this notion in the case of BPA voidBPABPA : basic process algebra with the state operator; see definition 2.8.1.

Below we give the definition of a ranked operator as defined by [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W.. And we list the new signature.

Now that we are equipped with the right tools we formulate the termination theorem for the system PA voidPAPA : process algebra.

[IMAGE ]

By means of the termination of PA voidPAPA : process algebra we can now formulate the following elimination theorem, which states that the merge and the left merge can be eliminated for closed terms.

[IMAGE ]

#### Standard concurrency

Some properties concerning both merges cannot be derived from PA voidPAPA : process algebra, but can only be proved for closed PA voidPAPA : process algebra terms, for instance the associativity of the merge. In many applications these properties are useful and thus assumed to hold. Hence, following [Bergstra and Tucker1984]Bergstra, J.A.Tucker, J.V., they are often referred to as axioms for standard concurrencyaxiom!standard concurrencystandard concurrency. In the next theorem we will treat two such equalities.

[IMAGE ]

#### Expansion

An important result in PA voidPAPA : process algebra with standard concurrency is the so-called expansionexpansion theorem, which is a generalization of axiom M1 ,16ex(see [Bergstra and Tucker1984]Bergstra, J.A.Tucker, J.V.,16ex). It tells us how the merge of more than two processes can be evaluated. For instance, the merge of three processes x,y, and z yields

[IMAGE ]

[IMAGE ]

### Semantics of PA

We will give the semantics of PA voidPAPA : process algebra by means of a term deduction system [IMAGE ]. Take for its signature the one of PA voidPAPA : process algebra and for its rules the ones of BPA voidBPABPA : basic process algebra in table 5 and the rules concerning the merge in table 44. Bisimulation equivalence is a congruence; see 2.2.32. So the operators of PA voidPAPA : process algebra\ can be defined on the quotient of closed PA voidPAPA : process algebra terms with respect to bisimulation equivalence. The following theorem says that this quotient is a model of PA voidPAPA : process algebra.

[IMAGE ]
Table: Derivation rules of [IMAGE ].

[IMAGE ]

Next, we take care of the conservativity of PA voidPAPA : process algebra over BPA voidBPABPA : basic process algebra.

[IMAGE ]

[IMAGE ]

Below we give the completeness theorem for PA voidPAPA : process algebra.

[IMAGE ]

## Extensions of PA

In this subsection we will discuss extensions of PA voidPAPA : process algebra with various features. We already met these extensions when we discussed BPA voidBPABPA : basic process algebra. We treat the extension of PA voidPAPA : process algebra with recursion, projections, renaming, the state operator, and iteration. We postpone the extensions of PA voidPAPA : process algebra with the priority operator and discrete time until we extended the theory PA voidPAPA : process algebra\ with deadlock. We deal with _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock in subsection 3.3.2. In subsection 3.3.3, we present an application of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock\ with the state operator, namely in the description of asynchronous communication. We explain in 3.3.4 why we do not treat PA voidPAPA : process algebra with the empty process.

An extension that is new here is the extension of PA voidPAPA : process algebra with a process creation mechanism. The reason we did not discuss this extension before, is that this extension makes essential use of the parallel operator. We discuss this extension in subsection 3.3.1.

#### Recursion

Here we will add recursion to PA voidPAPA : process algebra. This is done in the same way as we did for BPA voidBPABPA : basic process algebra.

The equational specification PA rec voidPArecPA rec : PA with recursion has as its signature the signature of BPA rec voidBPArecBPA rec : BPA with recursion plus the two binary operators [IMAGE ][IMAGE ] and [IMAGE ] present in the signature of PA voidPAPA : process algebra. The axioms of PA rec voidPArecPA rec : PA with recursion are the ones of BPA rec voidBPArecBPA rec : BPA with recursion\ plus the axioms of table 42.

The definition of a guard and a guarded recursive specification are the same as in subsection 2.3. Note that there are more guarded terms and recursion equations (thus guarded recursive specifications) in PA voidPAPA : process algebra than in BPA voidBPABPA : basic process algebra. For example, [IMAGE ][IMAGE ] is a guarded term and the recursion equation [IMAGE ] is guarded because of axiom M2.

The semantics of PA rec voidPArecPA rec : PA with recursion can be given with a term deduction system [IMAGE ]: take for its signature the one of PA rec voidPArecPA rec : PA with recursion and for its rules the rules of PA voidPAPA : process algebra plus the rules concerning recursion; see table 6. Since bisimulation equivalence is a congruence (2.2.32), we can define the operators of PA rec voidPArecPA rec : PA with recursion on the quotient algebra of the set of closed PA rec voidPArecPA rec : PA with recursion terms with respect to bisimulation equivalence. This quotient is a model of PA rec voidPArecPA rec : PA with recursion and it satisfies RDP voidRDPRDP : recursive definition principle, ^-[IMAGE ]voidAIPmin[IMAGE ]: restricted approximation induction principle, and RSP voidRSPRSP : recursive specification principle.

#### Projection

We can extend the equational specification PA voidPAPA : process algebra\ with projections as we did for BPA voidBPABPA : basic process algebra. The equational specification +PR [IMAGE ]voidPA PR[IMAGE ]: PA with projections\ has as its signature the one of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections plus the two binary operators [IMAGE ][IMAGE ] and [IMAGE ] present in the signature of PA voidPAPA : process algebra. Its axioms are the ones of PA voidPAPA : process algebra plus the axioms concerning projections; see table 7.

The results that we obtained in subsection 2.4 translate effortlessly to the present situation.

#### Recursion and projection

Here we will extend PA voidPAPA : process algebra with both recursion and projection. This extension is obtained analogously to the extension of BPA voidBPABPA : basic process algebra with recursion and projection. The specification +PR [IMAGE ]voidPArec PR[IMAGE ]: PA rec with projections has as its signature the one of PA rec voidPArecPA rec : PA with recursion plus the unary operators [IMAGE ] that occur in the signature of +PR [IMAGE ]voidPA PR[IMAGE ]: PA with projections. Its axioms are the ones of PA rec voidPArecPA rec : PA with recursion plus the axioms concerning projection; see table 7. The results that we obtained for +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with projections in subsection 2.4.2 also hold for +PR [IMAGE ]voidPArec PR[IMAGE ]: PA rec with projections. We will not mention them here.

The semantics of +PR [IMAGE ]voidPArec PR[IMAGE ]: PA rec with projections can be given by a combination of the term deduction system of PA rec voidPArecPA rec : PA with recursion and +PR [IMAGE ]voidPA PR[IMAGE ]: PA with projections.

#### Renaming

It is not difficult to extend the equational specification PA voidPAPA : process algebra, and its extensions, with renaming operators; see subsections 2.7 and 2.7.1.

#### State operator

We can extend the theory PA voidPAPA : process algebra with either the simple or extended state operator in the same way as we did for the theory BPA voidBPABPA : basic process algebra. For details we refer to subsections 2.8 and 2.9.

#### Iteration

We can extend PA voidPAPA : process algebra with iteration by just adding the defining axioms for [IMAGE ] in table 37 to the ones for PA voidPAPA : process algebra. For this theory there is no completeness result present at the time of writing this survey.

### 3.3.1 Process creation

In this subsection, we discuss an extension of PA voidPAPA : process algebra with an operator that models process creation. This extension is not present in BPA voidBPABPA : basic process algebra\ since it is defined using the parallel composition [IMAGE ][IMAGE ]. This subsection is based on [Bergstra1990]Bergstra, J.A.. We refer to [America and Bakker1988]America, P.Bakker, J.W. de and to [Baeten and Vaandrager1992]Baeten, J.C.M.Vaandrager, F.W. for other approaches to process creation.

We refer to [Bergstra and Klint1994]Bergstra, J.A.Klint, P. for an application of process creation.

#### The theory

The equational specification +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation (process algebra with process creationprocess creation) is defined in stages. First we take the theory PA voidPAPA : process algebra where we assume that the set of atomic actions A contains some special actions: for all d in some data set D we assume that [IMAGE ]voidcrd[IMAGE ]: creation action and [IMAGE ]voidcrd[IMAGE ]: trace of [IMAGE ]. We moreover assume the existence of a function, the process creation functionprocess creation functionfunction!process creation, [IMAGE ]voidphi[IMAGE ]: process creation function on D that assigns to each [IMAGE ] a process term [IMAGE ] over PA voidPAPA : process algebra with the above set of atomic actions A. Using the function [IMAGE ] we add a unary operator [IMAGE ]voidEphi[IMAGE ]: process creation operator to the signature, thus obtaining the signature of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation. The operator [IMAGE ] is called the process creation operatorprocess creation operatoroperator!process creation.

The equations of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation are those of PA voidPAPA : process algebra plus the ones that define [IMAGE ]. We list these equations in table 45voidPCR1-5PCR1-5: process creation axioms.

[IMAGE ]
Table 45: Axioms for the process creation operator.

#### Intuition

We provide some intuition for +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation. We will compare process creation with the UNIXUNIX[+] system callsystem callcall!system forkfork; see [Ritchie and Thompson1974]Ritchie, D.M.Thompson, K.. We recall that with fork we can only create an exact copy (child processchild processprocess!child) of its so-called parent processparent processprocess!parent. We note that with the process creation operator we are able to create arbitrary processes but to provide an intuition for process creation the system call fork is illustrative.

The atomic action [IMAGE ] can be seen as a trigger for [IMAGE ]; compare [IMAGE ] to the system call fork. The operator [IMAGE ] initiates the creation of a process when a [IMAGE ] is parsed; think of it as a program that invokes the system call fork. The action [IMAGE ] indicates that a process creation has occurred; this action can be interpreted as the return value of the system call fork to the parent process (which is the unique process ID of the newly created process). Maybe this intuition is best illustrated by axiom PCR4. There we see that from [IMAGE ] a process [IMAGE ] is created that is put in parallel with the remaining process x, while leaving a trace [IMAGE ].

Next, we formulate a simple lemma that states that process creation distributes over the merge.

[IMAGE ]

#### Termination

The above example shows that the term rewriting system associated to +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation (by orienting the axioms of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation from left to right) is, in general, not terminating. For, in case of the above example, we have the following infinite sequence of rewritings:

[IMAGE ]

#### Semantics

We discuss the operational semantics of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation. It is obtained by means of a term deduction system. The signature is that of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation; the operational rules are those of PA voidPAPA : process algebra plus the rules that operationally define the process creation operator [IMAGE ]. We list them in table 46. The rules of this table originate from [Baeten and Bergstra1988b]Baeten, J.C.M.Bergstra, J.A..

[IMAGE ]
Table 46: Operational rules for the process creation operator.

The soundness of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation is easily established.

[IMAGE ]

Next, we state that +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation is a conservative extension of PA voidPAPA : process algebra.

[IMAGE ]

[IMAGE ]

From example 3.3.2 it follows that the process creation operator introduces recursion. So we do not have a completeness theorem.

### 3.3.2 Deadlock in PA

It is straightforward to add deadlock to the theory PA voidPAPA : process algebra. The equational specification _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock has as its signature the one of PA voidPAPA : process algebra plus a constant [IMAGE ]. Its axioms are the ones of PA voidPAPA : process algebra plus the axioms concerning deadlock listed in table 10. We assume for axioms M2 and M3 that a ranges over the set [IMAGE ].

#### Structural induction

We can use structural induction for _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock as before for _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock, since basic _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock terms are just basic _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock terms. This follows immediately from the fact that both merges can be eliminated from closed _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock terms. This can be shown by means of a term rewriting analysis just as in theorem 3.2.3 and the following elimination theorem.

[IMAGE ]

Also the conservativity of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock over _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock and the completeness of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock\ can be proved along the same lines as these results for PA voidPAPA : process algebra without extensions.

#### Standard concurrency

Standard concurrencyaxiom!standard concurrencystandard concurrency in _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock is dealt with completely analogously to the situation without deadlock, so we refer to theorem 3.2.5 for standard concurrency. Below, we will mention some properties about the connection of deadlock and parallel composition. The proof of these properties is elementary and therefore omitted.

[IMAGE ]

[IMAGE ]

#### Expansion

For _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with standard concurrency we have the same expansionexpansion theorem as for the theory without deadlock, so for expansion we refer to theorem 3.2.6.

#### Semantics

The semantics of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock can be given by means of a term deduction system [IMAGE ]_[IMAGE ], which is just [IMAGE ] with [IMAGE ] added to its signature. The operators of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock can be easily defined by taking representatives on the quotient of the set of closed _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock terms modulo bisimulation equivalence, since this relation is a congruence; see 2.2.32. The quotient is a model for _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock, which can be easily checked by combining the soundness proofs for _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock\ and PA voidPAPA : process algebra. Moreover, the axiom system _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock is a complete axiomatization of this quotient. This follows immediately from the completeness of PA voidPAPA : process algebra\ since we did not introduce any new transitions.

### 3.3.3 Asynchronous communication

asynchronous communicationcommunication!asynchronous  It is straightforward to extend _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with any of the features mentioned in the beginning of subsection 3.3. Here, we consider an application of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with the (simple) state operator. We describe mail through a communication channel. Let D be a finite data set and let c be a communication channel. We assume that for each [IMAGE ] we have the following special atomic actions:
• [IMAGE ]voidc d[IMAGE ]: potential send action (infix predicate)send d via c; potential actionpotential actionaction!potential
• [IMAGE ]voidc d[IMAGE ]: realized send action (infix predicate)send d via c; realized actionrealized actionaction!realized
• [IMAGE ]voidc d[IMAGE ]: potential receive action (infix predicate)receive d via c; potential action
• [IMAGE ]voidc d[IMAGE ]: realized receive action (infix predicate)receive d via c; realized action.
The state operator will turn potential, intended actions into realized actions. The state space will keep track of outstanding messages.

We consider the case where the communication channel behaves like a queue, i.e. the order of the messages is preserved. Without much trouble, descriptions for other kinds of channels can be generated (for instance, a bag-like channel). Thus, the state space is [IMAGE ], the set of words over D. Let [IMAGE ], [IMAGE ] range over [IMAGE ], and let [IMAGE ] denote the empty word. We denote the concatenation of words [IMAGE ] and [IMAGE ] simply by [IMAGE ]. Note that [IMAGE ] so [IMAGE ] is the concatenation of the words [IMAGE ] and d (for [IMAGE ]). Let [IMAGE ] be the last element of word [IMAGE ], if [IMAGE ].

We define the action and effect functions implicitly, by giving the relevant instances of axiom SO2.

[IMAGE ]

The action and effect functions are inert for all other atomic actions. Now suppose [IMAGE ]; then we can describe two communication partners:

[IMAGE ]

Some easy calculations show that

[IMAGE ]

Asynchronous communicationasynchronous communicationcommunication!asynchronous in the setting of PA voidPAPA : process algebra\ was introduced in [Bergstra et al. 1985]Bergstra, J.A.Klop, J.W.Tucker, J.V.. The present formulation is taken from [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P..

### 3.3.4 Empty process in PA

We will not discuss the combination of parallel composition and the empty processempty processprocess!empty, since this combination is not (yet) standardized. At this moment there are two possible ways to combine the merge and the empty process. These options originate from the various interpretations of the term [IMAGE ]. It may seem natural to demand that this equals x, since [IMAGE ] is only capable of terminating successfully, but this perspective leads to a non-associative merge, which is rather unnatural and therefore unwanted [Vrancken1986]Vrancken, J.L.M.. The intended interpretation of the left merge is that of the merge with the first action from the left process, so the term [IMAGE ] cannot proceed, since [IMAGE ] cannot perform an action. One of the options is that [IMAGE ] equals [IMAGE ] except if [IMAGE ]: then it equals [IMAGE ]; see [Vrancken1986]Vrancken, J.L.M. for more information. The other option drops this exception and uses a unary operator indicating whether or not a process has a termination option to axiomatize the merge [Baeten and Glabbeek1987]Baeten, J.C.M.Glabbeek, R.J. van.

## Extensions of _[IMAGE ]

In this subsection we will discuss the extensions of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with recursion, projections, renaming, and/or the encapsulation operator, the state operator, the priority operator, iteration, process creation, and discrete time.

#### Recursion and/or projection

The extensions of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with recursion, projection, or a combination of both are obtained by simply merging these extensions for _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock\ and PA voidPAPA : process algebra; see subsections 2.5 and 3.3.

#### Renaming and encapsulation

It is straightforward to extend the equational specification _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock, and its extensions, with renaming operators or the encapsulation operator; cf. subsection 2.7.3.

#### State operator

The extension of the theory _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with either the simple or extended state operator is obtained in the same way as for the theory PA voidPAPA : process algebra; see subsections 2.8 and 2.9.

#### Priority operator

We can extend the theory _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with the priority operator in the same way as the extension of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock\ with that operator. For details of that extension we refer to section 2.10.

#### Iteration

We can extend _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with iteration by just adding the defining axioms for [IMAGE ] in table 37 to the ones for _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock. Only for ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration is the completeness proved at the time of writing this survey.

#### Process creation

We can extend _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with the process creation operator [IMAGE ] in the same way as we did for PA voidPAPA : process algebra. For details we refer to subsection 3.3.1.

### 3.4.1 Discrete time

In this subsection, we extend _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with discrete time. With the interaction between the discrete time unit delay [IMAGE ] and the left merge [IMAGE ] we have to be a bit careful. We recall that [IMAGE ] is x and y in parallel but the first action stems from x. With discrete time present, the question arises if that is possible at all. For instance, [IMAGE ] equals [IMAGE ] in this system as we cannot move to the next time slice in order to let a happen, since b must occur in the current time slice. The material of this subsection is based on [Baeten and Bergstra1992a]Baeten, J.C.M.Bergstra, J.A..

#### The theory

We discuss the equational specification _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time. Its signature is the one of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock (with [IMAGE ] instead of a for [IMAGE ]) plus the discrete time unit delay operator [IMAGE ] that we first introduced in _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time. The equations of _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time are the ones of _dt[IMAGE ]voidBPAdeltadt[IMAGE ]: [IMAGE ] with discrete time plus the equations for the merge that we listed in table 42 (again with [IMAGE ] instead of a) and the equations that represent the interaction between the left merge and the discrete time unit delay; we list the latter axioms in table 47voidDTM1-4DTM1-4: discrete time/merge axioms. Incidentally, this axiomatization is new here.

[IMAGE ]
Table 47: The interaction between the left merge and the discrete time unit delay.

#### Termination

Next, we discuss the termination of a term rewriting system associated to the equational specification _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time. Since we have the left merge in our signature we use the ranked operators that we also used for the termination of PA voidPAPA : process algebra; cf. subsection 3.2.1.

[IMAGE ]

#### Elimination

With the above theorem we can obtain an elimination result for closed terms. However, we cannot obtain this result directly. This is due to the fact that we did not consider a term rewriting analysis modulo the axioms without a clear direction such as A1 and A2. We make the problems a bit more concrete with the following term rewriting modulo A1 and A2.

[IMAGE ]

So, we see that for the elimination of the left merge we need more than just the termination result above. We will solve this problem in the next theorem.

[IMAGE ]

[IMAGE ]

#### Semantics

Now we discuss the operational semantics of _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time. The semantics of the system _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time is quite straightforward. In table 48 we list the additional operational rules for the merge and the left merge. The entire semantics of _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time consists of the one of _dt[IMAGE ]voidBPAdeltadt[IMAGE ]: [IMAGE ] with discrete time plus the rules in tables 44 and 48.

[IMAGE ]
Table 48: The additional rules for the merge and the left merge.

[IMAGE ]

[IMAGE ]

[IMAGE ]

Now we have all the prerequisites to state the completeness theorem for _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time. The proof is as usual and therefore omitted.

[IMAGE ]

## 3.5 Syntax and semantics of communicating processes

In this subsection we will extend the meaning of the parallel operator [IMAGE ][IMAGE ] that we introduced in subsection 3.2. We will call the ensuing operator [IMAGE ][IMAGE ] the merge or parallel composition. We use the name free merge for the merge without communication, that is the merge of PA voidPAPA : process algebra.

We use the extended merge to model synchronous communicationcommunicationsynchronous communicationcommunication!synchronous between processes.

### 3.5.1 The theory ACP

We define the syntax of the equational specification [IMAGE ] of [Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W..

The signature [IMAGE ] consists of the one of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock\ plus a binary operator [IMAGE ]|[IMAGE ]voidA AAEmerge[IMAGE ]|[IMAGE ]: communication merge, called the communication mergecommunication mergemerge!communication and the encapsulation operator [IMAGE ] that we already discussed in subsection 2.7.3 (we recall that [IMAGE ]). Moreover, we fix a partial function [IMAGE ]voidgamma[IMAGE ]: communication function, where A is the set of atomic actions. We call [IMAGE ] the communication functioncommunication functionfunction!communication. The communication function is, like A, a parameter of the theory. It is meant to model the communication between processes. In fact, the communication merge [IMAGE ]|[IMAGE ] is the extension of the communication function to processes. We require that [IMAGE ] is both commutative and associative; that is, if [IMAGE ] is defined, it equals [IMAGE ] and if [IMAGE ] is defined it equals [IMAGE ] and vice versa. So, we can leave out the brackets in such formulas and render the latter expression as [IMAGE ].

Now we give the set of equations [IMAGE ]. This set consists of the equations for +ð[IMAGE ]voidBPAdelta deltaH[IMAGE ]: [IMAGE ] with encapsulation that we discussed in subsection 2.7.3 and the equations that we list in table 49voidCM1-9CM1-9: axioms for the mergevoidCF1-2CF1-2: communication function axioms. See table 21 for the defining axioms of the encapsulation operator. Observe that the equations CM2-4 are the same as the ones that we discussed when we introduced PA voidPAPA : process algebra. We recall them for the sake of ease.

[IMAGE ]
Table 49: Axioms for the merge with communication.

Now we discuss the axioms of ACP voidACPACP : algebra of communicating processes. The most important one is CM1 where a third possibility for the merge is added. The intended interpretation of this summand [IMAGE ]|[IMAGE ] is that it is the parallel composition of the two processes x and y but that the first step must be a communication. Both processes must be able to perform an action for which [IMAGE ] is defined.

#### Terminology

We say that two atomic actions do not communicate if the communication function is not defined for them. We say that an atomic action a is a communication actioncommunication actionaction!communication if [IMAGE ] for atomic actions b and c. A communication action [IMAGE ] is called a binary communicationbinary communicationcommunication!binary; likewise [IMAGE ] is called ternaryternary communicationcommunication!ternary if defined. However, most of the time just using binary communication is enough in applications. See also later on when we discuss so-called handshaking.

An important case of binary communication is called read/send communicationread/send communicationcommunication!read/send. The idea is that in the set of atomic actions we have read actionsread actionaction!read [IMAGE ]voidrid[IMAGE ]: read d at port i, send actionssend actionaction!send [IMAGE ]voidsid[IMAGE ]: send d at port i, and communication actions [IMAGE ]voidcid[IMAGE ]: communicate d at port i. The intended meaning of [IMAGE ] is to read datum [IMAGE ] at portport i, where the set D is some finite data set. For [IMAGE ] a similar intuition holds. Now [IMAGE ] is the result of a communication of [IMAGE ] and [IMAGE ]: it means transmit the datum d by communication at port i. The appropriate communication function is [IMAGE ] and [IMAGE ] is not defined otherwise on [IMAGE ], [IMAGE ], and [IMAGE ] (for ports i,j,k and data elements d,e,f). For other atomic actions it is permitted to have some communications defined. The above conventions are due to [Bergstra and Klop1986]Bergstra, J.A.Klop, J.W.. An example of the use of read/send communication is given in section 3.6.

#### Structural induction

As before we can use structural induction for ACP voidACPACP : algebra of communicating processes, since basic ACP voidACPACP : algebra of communicating processes terms are just basic _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock terms. This follows from theorem 3.5.5 that states that parallel composition and encapsulation can be eliminated from closed ACP voidACPACP : algebra of communicating processes terms.

### 3.5.2 Termination

As before we prove the termination of a term rewriting system associated to ACP voidACPACP : algebra of communicating processes (see table 50) with the aid of the theory of subsection 2.2.2. The proof of this fact will more or less be the same as the proof for PA voidPAPA : process algebra. There we have given some operators a weight to avoid problems with the left merge. Note that in table 50, we rewrite [IMAGE ]|[IMAGE ] to an atomic action c or [IMAGE ] in order to eliminate the communication merge.

Next, we give the definition of the weight function. It is an extension of definition 3.2.1.

[IMAGE ]

Below we give the definition of a ranked operator as defined by [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W.. And we list the new signature. This definition is an extension of definition 3.2.2.

[IMAGE ]

[IMAGE ]
Table 50: Term rewriting rules for the merge.

[IMAGE ]

[IMAGE ]
Figure 8: Partial ordering of the operators in the term rewriting system associated to ACP.

With the aid of the above termination result for ACP voidACPACP : algebra of communicating processes we can easily prove the following elimination theorem.

[IMAGE ]

#### Standard concurrency

As for PA voidPAPA : process algebra we have standard concurrency. That is, there are some properties concerning the merge, left merge, and communication merge that are not derivable for arbitrary open terms, but can be shown to be valid for closed terms (or even for solutions of guarded recursive equations). In many applications these properties are useful and thus these properties are assumed to be valid. This is why these properties are often referred to as axioms for standard concurrencyaxiom!standard concurrencystandard concurrency. In the next theorem we list them for ACP voidACPACP : algebra of communicating processes. See theorem 3.2.5 for standard concurrency in PA voidPAPA : process algebra.

[IMAGE ]

[IMAGE ]

#### Expansion

A useful application of standard concurrency in ACP voidACPACP : algebra of communicating processes is the so-called expansionexpansion theorem. This theorem states how the merge of more than two processes can be evaluated. For the expansion theorem of PA voidPAPA : process algebra we refer to theorem 3.2.6. In contrast to the PA voidPAPA : process algebra expansion theorem, we need an extra proviso for the expansion of the merge in case the communication merge is present. We need a so-called handshaking axiomhandshaking axiomaxiom!handshaking (HAvoidHAHA: handshaking axiom). We give it in table 51. It states that there is only binary communication present.

[IMAGE ]
Table 51: Handshaking axiom.

[IMAGE ]

[IMAGE ]

Next, we formulate the expansion theorem for ACP voidACPACP : algebra of communicating processes. The notation that we use in this theorem can be defined inductively in the obvious way.

[IMAGE ]

### 3.5.3 Semantics of ACP

In this subsection we give the semantics of ACP voidACPACP : algebra of communicating processes. In fact, this is now an easy job, since almost all the constructs that ACP voidACPACP : algebra of communicating processes\ contains have been discussed before. The only notion that we did not characterize operationally is the communication merge. In table 52 we present the operational rules for this concept.

The complete operational semantics for ACP voidACPACP : algebra of communicating processes is given by a term deduction system [IMAGE ] that has as its signature the one of ACP voidACPACP : algebra of communicating processes\ and the rules are the ones of table 5 (the BPA voidBPABPA : basic process algebra part), the rules of table 22 (the encapsulation part), the rules of table 44 (the PA voidPAPA : process algebra merge part), and the new rules that we list in table 52. As usual, bisimulation equivalence is a congruence; see 2.2.32. So the operators of ACP voidACPACP : algebra of communicating processes can be defined on the quotient of closed ACP voidACPACP : algebra of communicating processes terms with respect to bisimulation equivalence. The following theorem says that this quotient is a model of ACP voidACPACP : algebra of communicating processes.

[IMAGE ]
Table 52: The operational rules for the communication merge.

[IMAGE ]

At this point, we are able to prove the conservativity of ACP voidACPACP : algebra of communicating processes over _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock.

[IMAGE ]

Below we give the completeness theorem for ACP voidACPACP : algebra of communicating processes.

[IMAGE ]

## 3.6 Extensions of ACP

In this subsection we will discuss extensions of ACP voidACPACP : algebra of communicating processes with the features that we already met when we discussed extensions of both BPA voidBPABPA : basic process algebra and PA voidPAPA : process algebra. We treat the extension of ACP voidACPACP : algebra of communicating processes with recursion, projections, renaming operators, the state operator, the priority operator, iteration, process creation, and discrete time. We will also treat two examples to illustrate the use of two of the extensions. We do not discuss the extension of ACP voidACPACP : algebra of communicating processes with the empty process. We explained why in subsection 3.3.4.

#### Recursion and/or projection

The extensions of ACP voidACPACP : algebra of communicating processes with recursion, projection, or a combination of both are obtained by simply merging these extensions for _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock\ and ACP voidACPACP : algebra of communicating processes; see subsection 2.5.

#### Renaming and encapsulation

It is straightforward to extend the equational specification ACP voidACPACP : algebra of communicating processes, and its extensions, with renaming operators; cf. subsection 2.7.3.

#### State operator

The extension of the theory ACP voidACPACP : algebra of communicating processes with either the simple or extended state operator is obtained in the same way as for the theories BPA voidBPABPA : basic process algebra or PA voidPAPA : process algebra; see subsections 2.8 and 2.9.

#### Priority operator

We can extend the theory ACP voidACPACP : algebra of communicating processes with the priority operator in the same way as we extended _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with that operator. For the details we refer to subsection 2.10.

In the system _[theta][IMAGE ]voidACPtheta[IMAGE ]: ACP with the priority operator, we can describe forms of asymmetric communicationasymmetric communicationcommunication!asymmetric. Notice that ACP voidACPACP : algebra of communicating processes itself features symmetric communication: both `halves' of a communication action must be present before either one can proceed.

[IMAGE ]

#### Iteration

We can extend ACP voidACPACP : algebra of communicating processes with iteration by adding the defining axioms for [IMAGE ] in table 37 to the ones for ACP voidACPACP : algebra of communicating processes and one more axiom that gives the relation between Kleene's star and the encapsulation operator. We give this axiom in table 53voidBKS4BKS4: iteration/encapsulation axiom. We denote this system by ^*[IMAGE ]voidACPstar[IMAGE ]: ACP with iteration. Only for ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration the completeness is proved at the time of writing this survey.

[IMAGE ]
Table 53: An extra axiom for Kleene's binary star operator.

#### Process creation

We discuss the extension of ACP voidACPACP : algebra of communicating processes with the process creation operator [IMAGE ] (for the basic definitions we refer to subsection 3.3.1). We recall that the process creation operator is defined in terms of the parallel composition. So it will not be surprising that we need to impose restrictions on the communication behaviour of the special atomic actions [IMAGE ]. The restrictions are that [IMAGE ] does not communicate and is not the result of any communication ([IMAGE ] is not a communication action). In a formula: [IMAGE ]|[IMAGE ] and for all [IMAGE ]|[IMAGE ]. We note that lemma 3.3.1 only holds when the communication function is trivial; that is, for all [IMAGE ] is undefined.

Furthermore, the only difference with the discussion in subsection 3.3.1 is the restrictions on the [IMAGE ]-actions with respect to the communication. So for more details we refer to that subsection.

#### Inconsistent combinations

If we combine unguarded recursion with _[theta][IMAGE ]voidACPtheta[IMAGE ]: ACP with the priority operator we will find an inconsistency. We show this with an example that originates from [Baeten and Bergstra1988b]Baeten, J.C.M.Bergstra, J.A.. Suppose that there are three atomic actions rs, and c and [IMAGE ]|[IMAGE ]. Let c>s be the partial ordering. Now consider the following recursion equation:

[IMAGE ]

With the operational rules we can infer that [IMAGE ]a[IMAGE ]a[IMAGE ].

### 3.6.1 Discrete time

In this subsection we add relative discrete time to ACP voidACPACP : algebra of communicating processes. In subsection 3.4.1, we already extended _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with this feature. So we only need to clarify the interaction between the discrete time unit delay [IMAGE ] and the communication merge and the relation between [IMAGE ] and the encapsulation operator.

#### The theory

The equational specification _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with discrete time\ consists of the signature that is the union of the signatures of ACP voidACPACP : algebra of communicating processes (with [IMAGE ] instead of a for [IMAGE ]) and _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time. The equations of this specification are the ones of ACP voidACPACP : algebra of communicating processes (again with [IMAGE ] instead of a) plus the rules of table 47 (they represent the interaction between [IMAGE ] and the left merge) and some new axioms that we present in table 54; they express the interaction between the discrete time unit delay operator and the communication merge and the interaction between [IMAGE ] and the encapsulation operator.

[IMAGE ]
Table: The interaction between [IMAGE ] and communication and encapsulation.

#### Termination

The termination of a term rewriting system associated to _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with discrete time can be obtained with the aid of the method that we discussed in subsection 2.2.2. We can prove the termination by merging the termination proofs of ACP voidACPACP : algebra of communicating processes and _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ] with discrete time\ and a small addition.

[IMAGE ]

[IMAGE ]

With the above theorem it is easy to obtain an elimination result for closed terms.

[IMAGE ]

[IMAGE ]

#### Semantics

The semantics of _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with discrete time can be given with a term deduction system [IMAGE ]_dt[IMAGE ]. Its signature is that of _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with discrete time. The rules are those of ACP voidACPACP : algebra of communicating processes (with [IMAGE ] instead of a for [IMAGE ]), those in table 48 (they concern the merge and the left merge), and the operational rules that we present in table 55. The two rules in table 55 define what kind of [IMAGE ] transitions the communication merge and the encapsulation operator can perform.

[IMAGE ]
Table 55: The additional rules for the communication merge and the encapsulation operator.

[IMAGE ]

[IMAGE ]

[IMAGE ]

Now we have all the prerequisites to state the completeness theorem for _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with discrete time. The proof is as usual and therefore omitted.

[IMAGE ]

## 3.7 Decidability and expressiveness results in ACP

In subsection 2.14 we discussed the decidability of bisimulation equivalence for BPA rec voidBPArecBPA rec : BPA with recursion and we showed that BPA rec voidBPArecBPA rec : BPA with recursion can express non-regular processes. In this subsection we will briefly discuss decidability and expressiveness results for the PA rec voidPArecPA rec : PA with recursion and ACP rec voidACPrecACP rec : ACP with recursion\ families.

### 3.7.1 Decidability

At the time of writing this survey the results are that bisimulation equivalence is undecidabledecidabilityundecidable for ACP rec voidACPrecACP rec : ACP with recursion and the problem is open for PA rec voidPArecPA rec : PA with recursion. However, some results have been obtained in the direction of PA rec voidPArecPA rec : PA with recursion. For the so-called Basic Parallel Processes (BPP voidBPPBPP : basic parallel processes) [Christensen et al. 1993]Christensen, S.Hirschfeld, Y.Moller, F. the problem is solved: BPP voidBPPBPP : basic parallel processes is decidable. The equational theory of BPP voidBPPBPP : basic parallel processes is close to _[IMAGE ]rec voidPAdeltarec[IMAGE ]: [IMAGE ] with recursion\ with prefix sequential composition instead of sequential composition.

We will formulate these results below.

The next theorem is due to [Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W.. For the proof of this fact we refer to [Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W..

[IMAGE ]

For the decidability result on basic parallel processes we briefly introduce the syntax and semantics of this system.

#### Basic parallel processes

basic parallel processes We will introduce the syntax and semantics of BPP voidBPPBPP : basic parallel processes below using the notation that we are used to in this survey. We have a special constant [IMAGE ], alternative composition +, parallel composition [IMAGE ][IMAGE ], and a unary prefix operator [IMAGE ], called prefix sequential compositionprefix sequential compositioncomposition!prefix sequential, for all [IMAGE ], where A is some set. Now if we also add recursion we have the syntax of BPP voidBPPBPP : basic parallel processes.

The semantics of BPP voidBPPBPP : basic parallel processes is given by means of the term deduction system in table 56. For all the operators we have the usual operational rules but only the non-predicate parts. We have not seen the well-known operational characterization of prefix sequential composition before in this chapter. We give the rules for BPP voidBPPBPP : basic parallel processes in one table for the sake of ease.

We note that bisimulation equivalence in this case is just the one that we defined in definition 2.2.28 without the predicate part.

[IMAGE ]
Table 56: The operational semantics of BPP.

The next theorem is taken from [Christensen et al. 1993]Christensen, S.Hirschfeld, Y.Moller, F.. For the proof of this fact we refer to [Christensen et al. 1993]Christensen, S.Hirschfeld, Y.Moller, F..

[IMAGE ]

### 3.7.2 Expressiveness

In this subsection we discuss various expressivityexpressivity results. It turns out that ACP rec voidACPrecACP rec : ACP with recursion is more expressive than PA rec voidPArecPA rec : PA with recursion\ and that the latter is more expressive than BPA rec voidBPArecBPA rec : BPA with recursion.

#### The bag

We consider a so-called bagbag of unbounded capacity. A bag is a process able to input data elements that reappear in some arbitrary order. Let D be a finite set of such datum elements containing more than one datum. Suppose that we have atomic actions for all [IMAGE ]:
The following recursive equation formally defines the bag.

[IMAGE ]

It will be clear that B is definable over PA rec voidPArecPA rec : PA with recursion. In figure 9 we depict the deduction graph of a bag over two datum elements 0 and 1. Note that we abbreviate [IMAGE ] to d and [IMAGE ] to [IMAGE ] for d=0,1.

[IMAGE ]
Figure 9: A deduction graph of a bag over two datum elements.

Next, we state that PA rec voidPArecPA rec : PA with recursion is more expressive than BPA rec voidBPArecBPA rec : BPA with recursion. This theorem stems from [Bergstra and Klop1984a, Bergstra and Klop1995]Bergstra, J.A.Klop, J.W.. For its proof we refer to this paper.

[IMAGE ]

[IMAGE ]

Next, we consider the expressivity of ACP rec voidACPrecACP rec : ACP with recursion over PA rec voidPArecPA rec : PA with recursion. The following theorem is taken from [Bergstra and Klop1984a, Bergstra and Klop1995]Bergstra, J.A.Klop, J.W.. For more details on this result and its proof we refer to this paper.

[IMAGE ]

Next, we discuss a result that states that +RN [IMAGE ]voidACPrec RN[IMAGE ]: ACP rec \ with renaming is more expressive than ACP rec voidACPrecACP rec : ACP with recursion.

[IMAGE ]
Figure 10: A FIFO queue.

#### The queue

A queuequeue is a process that transmits incoming data while preserving their order. See also figure 10. Such a process is also called a FIFO (First In First Out) queueFIFO queuequeue!FIFO. First, we describe the queue with input port 1 and output port 2 over a finite data set D by means of an infinite linear specification. As in 3.3.3, [IMAGE ] is the set of words over D.

It is not hard to see that a queue with input port 1 and output port 2 over the data set D can be specified as follows:

[IMAGE ]

We have the last equation for all [IMAGE ] and [IMAGE ].

In figure 11 we give a deduction graph of a queue over two datum elements; note that we abbreviate [IMAGE ] by d and [IMAGE ] by [IMAGE ] for d=0,1.

[IMAGE ]
Figure 11: A deduction graph for the queue.

The next theorem states that there is no finite specification for the queue in ACP rec voidACPrecACP rec : ACP with recursion. This result is taken from [Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A.; the proof uses results from [Bergstra and Tiuryn1987]Bergstra, J.A.Tiuryn, J.. For a proof we refer to [Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A..

[IMAGE ]

In [Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A. it is shown that in +RN [IMAGE ]voidACPrec RN[IMAGE ]: ACP rec \ with renaming there exists a finite specification of the queue. For details we refer to [Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A..

[IMAGE ]

Next, we list some expressivity results for extensions of PA voidPAPA : process algebra and ACP voidACPACP : algebra of communicating processes\ with iteration. These results are taken from [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A..

[IMAGE ]
Figure 12: Expressivity results for systems with iteration.

#### Recursion versus iteration

In subsection 2.14 we devoted a small paragraph to the comparison of recursion as treated in subsection 2.3 and iteration (see subsection 2.11). We stated that the system BPA lin voidBPAlinBPA lin : BPA with finite linear recursion (BPA voidBPABPA : basic process algebra with finite linear recursion) is more expressive than ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration (see theorem 2.14.6). This result is in fact stronger: the regular system of figure 7 cannot be expressed in ^*[IMAGE ]voidACPstar[IMAGE ]: ACP with iteration.

In [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A. it is shown that the regular process depicted in figure 7 can be expressed in ^*[IMAGE ]voidACPstar[IMAGE ]: ACP with iteration with abstraction.

The next theorem is taken from [Bergstra et al. 1994a]Bergstra, J.A.Bethke, I.Ponse, A.. For the proof we refer to their paper.

[IMAGE ]

More information on the subject of expressiveness in ACP voidACPACP : algebra of communicating processes can be found in [Baeten et al. 1987]Baeten, J.C.M.Bergstra, J.A.Klop, J.W. and in [Vaandrager1993]Vaandrager, F.W.. For more information on expressiveness in systems related to ACP voidACPACP : algebra of communicating processes we refer to [Ponse1992]Ponse, A. or [Glabbeek1995]Glabbeek, R.J. van.

# 4 Further reading

For those readers who want to know more about process algebra, we give some references. First of all, we want to mention a couple of textbooks in the area. A textbook for CCS voidCCSCCS : communicating concurrent processes-style process algebra is [Milner1989]Milner, R., for CSP voidCSPCSP : communicating sequential processes style we refer to [Hoare1985]Hoare, C.A.R., and for testing theory, there is [Hennessy1988]Hennessy, M.. In ACP voidACPACP : algebra of communicating processes style, the standard reference is [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P.. The companion volume [Baeten1990]Baeten, J.C.M. discusses applications of this theory. We also want to mention the proceedings of a workshop on ACP voidACPACP : algebra of communicating processes style process algebra [Ponse et al. 1995]Ponse, A.Verhoef, C.Vlijmen, S.F.M. van.

When process algebra is applied to larger examples, the need arises to handle data structuresdata structurestructure!data also in a formal way. The combination of processes and data is treated in the theories LOTOS voidLOTOSLOTOS : Language of Temporal Ordering Specification [Brinksma1987]Brinksma, E., PSF voidPSFPSF : Process Specification Formalism\ [Mauw and Veltink1993]Mauw, S.Veltink, G.J., or CRL[IMAGE ]voidmuCRLCRL[IMAGE ]: micro Common Representation Language\ [Groote and Ponse1995]Groote, J.F.Ponse, A..

Tool supporttool support in the use of process algebra is provided by most systems; a few references are [Boudol et al. 1990]Boudol, G.Roy, V.De Simone, R.Vergamini, D., [Cleaveland et al. 1990]Cleaveland, W.R.Parrow, J.Steffen, B., [Godskesen et al. 1989]Godskesen, J.Larsen, K.G.Zeeberg, M., [Lin1992]Lin, H., and [Veltink1993]Veltink, G.J..

For an impression of the state of the art in concurrency theory we refer to the proceedings of the series of CONCUR conferences on concurrency theory: [Baeten and Klop1990]Baeten, J.C.M.Klop, J.W., [Baeten and Groote1991]Baeten, J.C.M.Groote, J.F., [Cleaveland1992]Cleaveland, W.R., [Best1993]Best, E., and [Jonsson and Parrow1994]Jonsson, B.Parrow, J..

## References

Aceto and Hennessy1992
L. Aceto and M. Hennessy. Termination, deadlock, and divergence. Journal of the ACM, 39(1):147-187, January 1992.

Aceto et al. 1994
L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOS rules into equations. Information and Computation, 111(1):1-52, 1994.

America and Bakker1988
P. America and J.W. de Bakker. Designing equivalent semantic models for process creation. Theoretical Computer Science, 60:109-176, 1988.

Austry and Boudol1984
D. Austry and G. Boudol. Algèbre de processus et synchronisations. Theoretical Computer Science, 30(1):91-131, 1984.

Baeten and Bergstra1988a
J.C.M. Baeten and J.A. Bergstra. Global renaming operators in concrete process algebra. Information and Computation, 78(3):205-245, 1988.

Baeten and Bergstra1988b
J.C.M. Baeten and J.A. Bergstra. Processen en procesexpressies. Informatie, 30(3):214-222, 1988. In Dutch.

Baeten and Bergstra1991
J.C.M. Baeten and J.A. Bergstra. Recursive process definitions with the state operator. Theoretical Computer Science, 82:285-302, 1991.

Baeten and Bergstra1992a
J.C.M. Baeten and J.A. Bergstra. Discrete time process algebra (extended abstract). In Cleaveland CONCUR92, pages 401-420. Full version, report P9208b, Programming Research Group, University of Amsterdam, 1992.

Baeten and Bergstra1992b
J.C.M. Baeten and J.A. Bergstra. Process algebra with signals and conditions. In M. Broy, editor, Programming and Mathematical Methods, Proceedings Summer School Marktoberdorf 1991, pages 273-323. Springer-Verlag, 1992. NATO ASI Series F88.

Baeten and Bergstra1993
J.C.M. Baeten and J.A. Bergstra. Real space process algebra. Formal Aspects of Computing, 5(6):481-529, 1993.

Baeten and Glabbeek1987
J.C.M. Baeten and R.J. van Glabbeek. Merge and termination in process algebra. In K.V. Nori, editor, Proceedings [IMAGE ] Conference on Foundations of Software Technology and Theoretical Computer Science, Pune, India, volume 287 of Lecture Notes in Computer Science, pages 153-172. Springer-Verlag, 1987.

Baeten and Groote1991
J.C.M. Baeten and J.F. Groote, editors. Proceedings CONCUR 91, Amsterdam, volume 527 of Lecture Notes in Computer Science. Springer-Verlag, 1991.

Baeten and Klop1990
J.C.M. Baeten and J.W. Klop, editors. Proceedings CONCUR 90, Amsterdam, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

Baeten and Vaandrager1992
J.C.M. Baeten and F.W. Vaandrager. An algebra for process creation. Acta Informatica, 29(4):303-334, 1992.

Baeten and Verhoef1993
J.C.M. Baeten and C. Verhoef. A congruence theorem for structured operational semantics with predicates. In Best CONCUR93, pages 477-492.

Baeten and Weijland1990
J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

Baeten et al. 1986
J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae, IX(2):127-168, 1986.

Baeten et al. 1987
J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. On the consistency of Koomen's fair abstraction rule. Theoretical Computer Science, 51(1/2):129-176, 1987.

Baeten et al. 1991
J.C.M. Baeten, J.A. Bergstra, S. Mauw, and G.J. Veltink. A process specification formalism based on static COLD. In J.A. Bergstra and L.M.G. Feijs, editors, Algebraic Methods II: Theory, Tools and Applications, volume 490 of Lecture Notes in Computer Science, pages 303-335. Springer-Verlag, 1991.

Baeten et al. 1992
J.C.M. Baeten, J.A. Bergstra, and S.A. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities. In Cleaveland CONCUR92, pages 472-485.

Baeten et al. 1993
J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Journal of the ACM, 40(3):653-682, July 1993.

Baeten1990
J.C.M. Baeten, editor. Applications of Process Algebra. Cambridge Tracts in Theoretical Computer Science 17. Cambridge University Press, 1990.

Bakker and Zucker1982
J.W. de Bakker and J.I. Zucker. Processes and the denotational semantics of concurrency. Information and Control, 54(1/2):70-120, 1982.

Bergstra and Klint1994
J.A. Bergstra and P. Klint. The toolbus--a component interconnection architecture. Report P9408, Programming Research Group, University of Amsterdam, 1994.

Bergstra and Klop1982
J.A. Bergstra and J.W. Klop. Fixed point semantics in process algebras. Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

Bergstra and Klop1984a
J.A. Bergstra and J.W. Klop. The algebra of recursively defined processes and the algebra of regular processes. In J. Paredaens, editor, Proceedings [IMAGE ] ICALP, Antwerpen, volume 172 of Lecture Notes in Computer Science, pages 82-95. Springer-Verlag, 1984. Extended abstract, full version appeared in [Ponse et al. 1995].

Bergstra and Klop1984b
J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60(1/3):109-137, 1984.

Bergstra and Klop1985
J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37(1):77-121, 1985.

Bergstra and Klop1986
J.A. Bergstra and J.W. Klop. Verification of an alternating bit protocol by means of process algebra. In W. Bibel and K.P. Jantke, editors, Math. Methods of Spec. and Synthesis of Software Systems '85, Math. Research 31, pages 9-23, Berlin, 1986. Akademie-Verlag.

Bergstra and Klop1995
J.A. Bergstra and J.W. Klop. The algebra of recursively defined processes and the algebra of regular processes. In Ponse et al. ACP94, pages 1-25. Full version of [Bergstra and Klop1984a].

Bergstra and Tiuryn1987
J.A. Bergstra and J. Tiuryn. Process algebra semantics for queues. Fundamenta Informaticae, X:213-224, 1987.

Bergstra and Tucker1984
J.A. Bergstra and J.V. Tucker. Top down design and the algebra of communicating processes. Science of Computer Programming, 5(2):171-199, 1984.

Bergstra et al. 1985
J.A. Bergstra, J.W. Klop, and J.V. Tucker. Process algebra with asynchronous communication mechanisms. In S.D. Brookes, A.W. Roscoe, and G. Winskel, editors, Seminar on Concurrency, volume 197 of Lecture Notes in Computer Science, pages 76-95. Springer-Verlag, 1985.

Bergstra et al. 1994a
J.A. Bergstra, I. Bethke, and A. Ponse. Process algebra with iteration and nesting. The Computer Journal, 37(4):243-258, 1994.

Bergstra et al. 1994b
J.A. Bergstra, I. Bethke, and A. Ponse. Process algebra with combinators. In E. Börger, Y. Gurevich, and K. Meinke, editors, Proceedings of CSL '93, volume 832 of Lecture Notes in Computer Science, pages 36-65. Springer-Verlag, 1994.

Bergstra et al. 1994c
J.A. Bergstra, A. Ponse, and J.J. van Wamel. Process algebra with backtracking. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Symposium ``A Decade of Concurrency: Reflections and Perspectives'', volume 803 of Lecture Notes in Computer Science, pages 46-91. Springer-Verlag, 1994.

Bergstra1985
J.A. Bergstra. Put and get, primitives for synchronous unreliable message passing. Logic Group Preprint Series Nr. 3, CIF, State University of Utrecht, 1985.

Bergstra1990
J.A. Bergstra. A process creation mechanism in process algebra. In Baeten Ba90, pages 81-88.

Best1993
E. Best, editor. Proceedings CONCUR 93, Hildesheim, Germany, volume 715 of Lecture Notes in Computer Science. Springer-Verlag, August 1993.

Bezem and Groote1994
M.A. Bezem and J.F. Groote. Invariants in process algebra with data. In Jonsson and Parrow CONCUR94, pages 401-416.

Blanco1995
J.O. Blanco. Definability with the state operator in process algebra. In Ponse et al. ACP94, pages 218-241.

Bloom et al. 1988
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.

Bol and Groote1991
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.

Boudol et al. 1990
G. Boudol, V. Roy, R. De Simone, and D. Vergamini. Process calculi, from theory to practice: verification tools. In Sifakis CAV1a, pages 1-10.

Brinksma1987
E. Brinksma. Information processing systems - open systems interconnection - LOTOS - a formal description technique based on the temporal ordering of observational behaviour ISO/TC97/SC21/N DIS8807, International Standardisation Organisation, 1987.

Brookes et al. 1984
S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3):560-599, 1984.

Caucal1990
D. Caucal. On the transition graphs of automata and grammars. Report 1318, INRIA, 1990.

Christensen et al. 1992
S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. In Cleaveland CONCUR92, pages 138-147.

Christensen et al. 1993
S. Christensen, Y. Hirschfeld, and F. Moller. Bisimulation equivalence is decidable for basic parallel processes. In Best CONCUR93, pages 143-157.

Christensen1993
S. Christensen. Decidability and decomposition in process algebra. PhD thesis, University of Edinburgh, 1993.

Cleaveland et al. 1990
R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench. In Sifakis CAV1a, pages 24-37.

Cleaveland1992
W.R. Cleaveland, editor. Proceedings CONCUR 92, Stony Brook, NY, USA, volume 630 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

Copi et al.1958
I.M. Copi, C.C. Elgot, and J.B. Wright. Realization of events by logical nets. Journal of the ACM, 5:181-196, 1958.

De Simone1985
R. De Simone. Higher-level synchronising devices in meije-SCCS. Theoretical Computer Science, 37:245-267, 1985.

Dershowitz and Jouannaud1990
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Formal Models and Semantics. Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243-320. Elsevier - MIT Press, Amsterdam, 1990.

Dershowitz1987
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69-116, 1987.

Fokkink and Zantema1994
W.J. Fokkink and H. Zantema. Basic process algebra with iteration: completeness of its equational axioms. The Computer Journal, 37(4):259-267, 1994.

Fokkink1994
W.J. Fokkink. The format reduces to tree rules. In M. Hagiya and J.C. Mitchell, editors, Proceedings 2nd International Symposium on Theoretical Aspects of Computer Software (TACS'94), Sendai, Japan, volume 789 of Lecture Notes in Computer Science, pages 440-453. Springer Verlag, 1994.

Giacalone et al. 1990
A. Giacalone, C.-C. Jou, and S.A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In M. Broy and C.B. Jones, editors, Proceedings IFIP Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel. North-Holland, 1990.

Glabbeek and Weijland1989
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.

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

Glabbeek1990
R.J. van Glabbeek. The linear time - branching time spectrum. In Baeten and Klop CONCUR90, pages 278-297.

Glabbeek1993
R.J. van Glabbeek. The linear time - branching time spectrum ii (extended abstract). In Best CONCUR93, pages 66-81.

Glabbeek1995
R.J. van Glabbeek. On the expressiveness of (extended abstract). In Ponse et al. ACP94, pages 188-217.

Godskesen et al. 1989
J. Godskesen, K.G. Larsen, and M. Zeeberg. TAV-tools for autimatic verification. Technical report R89-19, University of Aalborg, 1989.

Groote and Ponse1994
J.F. Groote and A. Ponse. Process algebra with guards: combining Hoare logic and process algebra. Formal Aspects of Computing, 6(2):115-164, 1994.

Groote and Ponse1995
J.F. Groote and A. Ponse. The syntax and semantics of [IMAGE ]CRL. In Ponse et al. ACP94, pages 26-62.

Groote and Vaandrager1992
J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, October 1992.

Groote1990a
J.F. Groote. A new strategy for proving [IMAGE ]-completeness with applications in process algebra. In Baeten and Klop CONCUR90, pages 314-331.

Groote1990b
J.F. Groote. Transition system specifications with negative premises (extended abstract). In Baeten and Klop CONCUR90, pages 332-341. Full version appeared as Technical Report CS-R8950, CWI, Amsterdam, 1989.

Hennessy1988
M. Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts, 1988.

Hoare et al. 1987
C.A.R. Hoare, I.J. Hayes, He Jifeng, C.C. Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sorensen, J.M. Spivey, and B.A. Surfin. Laws of programming. Communications of the ACM, 30(8):672-686, 1987.

Hoare1985
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, 1985.

Jonsson and Parrow1994
B. Jonsson and J. Parrow, editors. Proceedings CONCUR 94, Uppsala, Sweden, volume 836 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

Jouannaud and Kirchner1986
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15:1155-1194, 1986.

Jouannaud and Muñoz1984
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.

Kamin and Lévy1980
S. Kamin and J.-J. Lévy. Two generalizations of the recursive path ordering, 1980. Unpublished manuscript.

Kleene1956
S.C. Kleene. Representation of events in nerve nets and finite automata. In Automata Studies, pages 3-41. Princeton University Press, 1956.

Klop1992
J.W. Klop. Term rewriting systems. In Handbook of Logic in Computer Science, Volume II, pages 1-116. Oxford University Press, 1992.

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

Koymans and Vrancken1985
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.

Larsen and Skou1992
K.G. Larsen and A. Skou. Compositional verification of probabilistic processes. In Cleaveland CONCUR92, pages 456-471.

Lin1992
H. Lin. PAM: a process algebra manipulator. In K.G. Larsen and A. Skou, editors, Proceedings of the 3rd International Workshop on Computer Aided Verification, Aalborg, Denmark, July 1991, volume 575 of Lecture Notes in Computer Science, pages 176-187. Springer-Verlag, 1992.

Mauw and Veltink1993
S. Mauw and G.J. Veltink, editors. Algebraic Specification of Communication Protocols. Cambridge Tracts in Theoretical Computer Science 36. Cambridge University Press, 1993.

Milne1983
G.J. Milne. CIRCAL: a calculus for circuit description. Integration, 1:121-160, 1983.

Milner et al. 1992
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part I + II. Information and Computation, 100(1):1-77, 1992.

Milner1980
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

Milner1983
R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267-310, 1983.

Milner1989
R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

Moller and Tofts1990
F. Moller and C.M.N. Tofts. A temporal calculus of communicating systems. In Baeten and Klop CONCUR90, pages 401-415.

Moller1989
F. Moller. Axioms for concurrency. PhD thesis, Report CST-59-89, Department of Computer Science, University of Edinburgh, 1989.

Nicollin and Sifakis1994
X. Nicollin and J. Sifakis. The algebra of timed processes, ATP: theory and application. Information and Computation, 114(1):131-178, 1994.

Park1981
D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, [IMAGE ] GI Conference, volume 104 of Lecture Notes in Computer Science, pages 167-183. Springer-Verlag, 1981.

Peackock1830
G. Peackock. A treatise of algebra. Cambridge, 1830.

Plotkin1981
G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

Ponse et al. 1995
A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors. Algebra of Communicating Processes, Utrecht 1994, Workshops in Computing. Springer-Verlag, 1995.

Ponse1991
A. Ponse. Process expressions and Hoare's logic: showing an irreconcilability of context-free recursion with Scott's induction rule. Information and Computation, 95(2):192-217, 1991.

Ponse1992
A. Ponse. Computable processes and bisimulation equivalence. Report CS-R9207, CWI, Amsterdam, January 1992. To appear in Formal Aspects of Computing.

Ponse1993
A. Ponse. Personal communication, June 1993.

Ritchie and Thompson1974
D.M. Ritchie and K. Thompson. The UNIX time-sharing system. Communications of the ACM, 17(7):365-375, 1974.

Sifakis1990
J. Sifakis, editor. Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June 1989, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

Tofts1990
C.M.N. Tofts. A synchronous calculus of relative frequency. In Baeten and Klop CONCUR90, pages 467-480.

Troeger1993
D.R. Troeger. Step bisimulation is pomset equivalence on a parallel language without explicit internal choice. Mathematical Structures in Computer Science, 3:25-62, 1993.

Vaandrager1990a
F.W. Vaandrager. Process algebra semantics of POOL. In Baeten Ba90, pages 173-236.

Vaandrager1990b
F.W. Vaandrager. Two simple protocols. In Baeten Ba90, pages 23-44.

Vaandrager1993
F.W. Vaandrager. Expressiveness results for process algebras. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Proceedings REX Workshop on Semantics: Foundations and Applications, Beekbergen, The Netherlands, June 1992, volume 666 of Lecture Notes in Computer Science, pages 609-638. Springer-Verlag, 1993.

Veltink1993
G.J. Veltink. The PSF toolkit. Computer Networks and ISDN Systems, 25:875-898, 1993.

Verhoef1992
C. Verhoef. Linear Unary Operators in Process Algebra. PhD thesis, University of Amsterdam, June 1992.

Verhoef1994a
C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. In Jonsson and Parrow CONCUR94, pages 433-448.

Verhoef1994b
C. Verhoef. A general conservative extension theorem in process algebra. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi (PROCOMET '94), volume A-56 of IFIP Transactions A: Computer Science and Technology, pages 149-168. North-Holland, 1994.

Vrancken1986
J.L.M. Vrancken. The algebra of communicating processes with empty process. Report FVI 86-01, Dept. of Computer Science, University of Amsterdam, 1986.

Weijland1989
W.P. Weijland. Synchrony and asynchrony in process algebra. PhD thesis, University of Amsterdam, 1989.

## Index

...allowed
Note that each recursively specifiable process over ACP voidACPACP : algebra of communicating processes can also be specified with a possibly infinite number of linear equations. Hence the finiteness constraint.
...UNIXUNIX
UNIX is a registered trademark of UNIX System Laboratories (at least at the time of writing this survey).

X Verhoef
Fri Jun 13 12:53:07 MET DST 1997