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.
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.
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.
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.
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..
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 ]
Table 1: BPA.
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.
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:
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.
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.
A useful property for a term reduction system is that there are no infinite reductions possible. Below we define some more notions.
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 ]
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.
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).
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 ]
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.
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.
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.
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.
In this subsection we will add recursion to the theory BPA voidBPABPA : basic process algebra.
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 ].
The next two definitions are taken from [Bergstra and Klop1986]Bergstra, J.A.Klop, J.W..
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.
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 ]
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.
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.
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 ].
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
converges to the term s itself. It is a nice example of the use of structural induction.
[IMAGE ]
Table 9: Derivation rules for projections.
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.
First we formalize how we can join two given signatures.
Next, we define how to ``add'' two operational semantics.
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.
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..
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..
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.
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.
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.
Next, we define the notion of equational conservativity.
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.
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.
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.
The following corollary is called the projection theorem.
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 5, 6, 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.
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.
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 ]
Table 10: Deadlock.
In this subsection we will discuss the extensions of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with recursion and/or projections.
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.
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 1, 7, 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.
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).
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.
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.
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.
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 ].
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:
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.
In this subsection we will discuss the extensions of _()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] with recursion and/or projections.
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.
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.
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.
[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.
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.
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.
With the aid of the above termination result, we can show the elimination theorem for basic process algebra with renaming operators.
[IMAGE ]
Table: A term rewriting system for +RN [IMAGE ].
[IMAGE ]
Table 20: Derivation rules concerning renaming operators.
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.
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.
In this subsection we will discuss the extensions of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming with recursion and/or projections.
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.
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.
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.
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
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.
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 ]).
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.
Note that proposition 2.7.3 also holds for +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]: [IMAGE ] with renaming.
[IMAGE ]
Table 23: Derivation rules for renaming operators and empty process.
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 ].
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.
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
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.
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. M, S, 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
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.
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.
Now, we can state the elimination theorem for basic process algebra with the state operator.
[IMAGE ]
Table: Derivation rules of [IMAGE ]_[IMAGE ].
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
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..
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. M, S, 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
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.
[IMAGE ]
Table 30: The rewrite rules for the extended state operator.
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
As before, we have [IMAGE ].
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
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 ]
Table 32: The axioms defining the priority operator.
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.
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.
Next, we formulate the elimination theorem for 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.
Next, we formalize the notion when a formula holds in a term deduction system with negative premises.
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.
[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.
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.
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..
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.
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..
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..
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.
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.
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.
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.
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.
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..
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.
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.
In this case, the operational rule takes the form
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:
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.
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.
Now it can be shown that
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.
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.
[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:
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 ]
Table 38: Operational rules for Kleene's binary star operator.
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
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
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.
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.
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..
[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.
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.
Next, we formulate some facts from [Baeten and Bergstra1992a]Baeten, J.C.M.Bergstra, J.A.. They can be easily proved.
[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.
Next, we formulate a conservativity result for _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with discrete time.
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.
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.
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.
For more information on the extension of BPA voidBPABPA : basic process algebra with conditional constructs we refer to the above papers.
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).
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.
In this subsection we briefly mention decidability and expressiveness issues for the family of process algebras that we have introduced thus far.
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.
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.
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.
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.
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..
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.
In this subsection we will describe the syntax and semantics of concrete concurrent processes.
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.
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.
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.
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.
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.
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 ].
Next, we take care of the conservativity of PA voidPAPA : process algebra over BPA voidBPABPA : basic process algebra.
Below we give the completeness theorem for PA voidPAPA : process algebra.
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.
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.
The results that we obtained in subsection 2.4 translate effortlessly to the present situation.
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.
We refer to [Bergstra and Klint1994]Bergstra, J.A.Klint, P. for an application of 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.
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 ]
Table 46: Operational rules for the process creation operator.
The soundness of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation is easily established.
Next, we state that +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process creation is a conservative extension of PA voidPAPA : process algebra.
From example 3.3.2 it follows that the process creation operator introduces recursion. So we do not have a completeness theorem.
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 ].
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.
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 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.
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.
The action and effect functions are inert for all other atomic actions. Now suppose [IMAGE ]; then we can describe two communication partners:
Some easy calculations show that
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..
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.
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.
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..
[IMAGE ]
Table 47: The interaction between the left merge and the discrete time unit
delay.
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.
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.
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.
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.
We use the extended merge to model synchronous communicationcommunicationsynchronous communicationcommunication!synchronous between processes.
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.
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.
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 ]
Table 50: Term rewriting rules for the merge.
[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 ]
Table 51: Handshaking axiom.
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.
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.
At this point, we are able to prove the conservativity of ACP voidACPACP : algebra of communicating processes over _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock.
Below we give the completeness theorem for ACP voidACPACP : algebra of communicating processes.
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.
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.
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 ]
Table 53: An extra axiom for Kleene's binary star operator.
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.
With the operational rules we can infer that [IMAGE ]a[IMAGE ]a[IMAGE ].
[IMAGE ]
Table: The interaction between [IMAGE ] and communication and
encapsulation.
With the above theorem it is easy to obtain an elimination result for closed terms.
[IMAGE ]
Table 55: The additional rules for the communication merge and the encapsulation
operator.
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.
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.
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..
For the decidability result on basic parallel processes we briefly introduce the syntax and semantics of this system.
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..
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.
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.
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.
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.
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:
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..
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..
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.
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.
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.
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..