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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
[IMAGE ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
With the aid of the above termination result, we can show the elimination
theorem for basic process algebra with renaming operators.
[IMAGE ]
[IMAGE ]
At this point we have all the ingredients necessary to state and prove that
+RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming is a conservative extension of BPA voidBPABPA : basic process algebra.
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 ]
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 ]
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 ]
We will give an example. Suppose that [IMAGE ] and f(b)=b.
Then we can derive [IMAGE ], for
each [IMAGE ].
[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 ]
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 ]
Now, we can state the elimination theorem for basic process algebra with
the state operator.
[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 ]
[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 ]
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 ]
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 ]
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 ]
[IMAGE ]
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 ]
[IMAGE ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
[IMAGE ]
With the aid of the above termination result for ACP voidACPACP : algebra of communicating processes we can easily
prove the following elimination theorem.
[IMAGE ]
Next, we formulate the expansion theorem for ACP voidACPACP : algebra of communicating processes. The notation that we
use in this theorem can be defined inductively in the obvious way.
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 ]
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 ]
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 ]
With the above theorem it is easy to obtain an elimination result for
closed terms.
[IMAGE ]
Now we have all the prerequisites to state the completeness theorem for
_dt[IMAGE ]voidACPdt[IMAGE ]: ACP with
discrete time. The proof is as usual and therefore omitted.
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 ]
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 ]
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 ]
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 ]
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 ]
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..
Acknowledgements
We thank the proof readers, Jan Bergstra
(University of Amsterdam and Utrecht University) and Jan Willem Klop (CWI
and Free University Amsterdam) for their useful comments. Also comments
by Twan Basten (Eindhoven University of Technology), Kees Middelburg
(PTT Research and Utrecht University), Alban Ponse (University of
Amsterdam), and Michel Reniers (Eindhoven University of Technology)
were appreciated. Special thanks go to Joris Hillebrand (University of
Amsterdam) for his essential help in the final stages of the preparation
of the document.
2 Concrete sequential processes
In this section we will introduce some basic concepts that can be found
in process algebra. We will do this in a modular way. That is, first
we treat a basic theory that is the kernel for all the other theories
that we will discuss subsequently. The basic theory describes finite,
concrete, sequential non-deterministic processes. Then we add features
to this kernel that are known to be important in process algebra: for
instance, deadlock or recursion to mention a few. Such features make
the kernel more powerful for both theoretical and practical purposes.
We also show that each feature is a so-called conservative extension of
the original theory; thus, we may argue that our approach is modular.
2.1 Introduction
2.2 Basic process algebra
2.2.1 The theory Basic Process Algebra
Table 1: BPA.
Intuition
Full distributivity
Figure: Two deduction graphs with the same execution
paths ab and ac but with different choice moments.
Structural induction
Structural inductionstructural
inductioninduction!structural is a basic proof technique in
process algebra when closed terms are involved. We will inductively
define the class of basic terms. It will turn out that every closed
term can be written as a basic term.
2.2.2 Term rewriting systems
In this subsection we will introduce a result from the field of term
rewriting systems that is a powerful tool in process algebra. We will
do this by means of an example: we will prove the essential step of
proposition 2.2.6 using the result. General references
to this theory are [Dershowitz and Jouannaud1990]Dershowitz, N.Jouannaud,
J.-P. and [Klop1992]Klop, J.W..
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.
2.2.3 Semantics of basic process algebra
Table: Derivation rules of [IMAGE ].
Figure 2: A proof
2.3 Recursion in BPA
Semantics
The semantics of BPA rec voidBPArecBPA rec : BPA with recursion can be given
completely analogously to the semantics for BPA voidBPABPA : basic process algebra that we gave in
subsection 2.3.
Table 6: Derivation rules for recursion ([IMAGE ]).
Figure: Two deduction graphs of the processes X
and Y that can be found in example 2.3.2.
2.4 Projection in BPA
Table 7: Projection.
Proof rule
We will discuss a proof rule expressing that a
process is determined by its finite projections. This rule is due to
[Bergstra and Klop1986]Bergstra, J.A.Klop, J.W..
Table: A term rewriting system for +PR [IMAGE ].
Table 9: Derivation rules for projections.
Semantics
The semantics of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections can be given in the same
way as the semantics for BPA voidBPABPA : basic process algebra.
2.4.1 Conservativity
Here, we will explain how to prove the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over
BPA voidBPABPA : basic process algebra without using theorem 2.4.5. We recall that
the main application of theorem 2.4.5 is that we can
prove that adding the projection operators does not yield new identities
between BPA voidBPABPA : basic process algebra terms. This important property is called conservativity.
We did not give a proof of theorem 2.4.5, but
instead we will provide an alternative powerful method for proving the
conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over BPA voidBPABPA : basic process algebra (and all the other conservativity
theorems in this chapter). This method is based on the format of
the operational rules of both systems rather than on a term rewriting
analysis. So, we will make a second expedition into the area of general
theory on structured operational semantics and we will illustrate the
theory with a running example. This example will yield, of course,
the conservativity of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections over BPA voidBPABPA : basic process algebra. We will base ourselves
on [Verhoef1994b]Verhoef, C..
2.4.2 Recursion and projection
Proof rule
We will discuss a proof rule expressing that a
process that can be specified with the aid of a guarded recursive
specification is determined by its finite projections. This rule is a
restricted version of the rule that is defined in
definition 2.4.1 and is also due to
[Bergstra and Klop1986]Bergstra, J.A.Klop, J.W..
Semantics
2.5 Deadlock
Table 10: Deadlock.
Structural induction
In _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock we can use the technique of
structural induction just like in BPA voidBPABPA : basic process algebra (compare
page [*]). We will adjust the definition of a
basic term (see definition 2.2.4) and we will mention
the result that every closed term over _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock can be written as a
basic term.
Semantics
As usual, we give the semantics by means
of a term deduction system. Take for the signature of [IMAGE ]_[IMAGE ]
the signature of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock and for the set of rules just the ones
of BPA voidBPABPA : basic process algebra of table 5. Since bisimulation equivalence is a
congruence (2.2.32), the quotient of closed _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock terms
modulo bisimulation equivalence is well-defined so the operators of
_[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock can be defined on this quotient using representatives.
This quotient is a model of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock.
Extensions of _[IMAGE ]
Recursion
Projection
Recursion and projection
2.6 Empty process
Table 11: Empty process.
Structural induction
Semantics
Table: Derivation rules of [IMAGE ]_()[IMAGE ].
2.6.1 Conservativity
In this subsection we will explain how to prove that _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty
process is a
conservative extension of BPA voidBPABPA : basic process algebra. We cannot immediately use the theory
of subsection 2.4.1, since the operational semantics of _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty
process\
presented in table 12 is not an operationally
conservative extension of the operational semantics of BPA voidBPABPA : basic process algebra that we
listed in table 5. For we can prove in the extended
system that [IMAGE ], whereas in the subsystem we can prove
that [IMAGE ]a[IMAGE ]. So we can ``reach'' a new term if we start with
an original term. A possible solution for this problem is to give
an alternative operational semantics for _[IMAGE ]voidBPAepsilon[IMAGE ]: BPA with empty
process than the one that we
present in table 12.
Extensions of _()[IMAGE ]
Recursion
Table 13: Derivation rules for recursion and empty process.
Projection
Table 14: Derivation rules for projections with empty process.
Recursion and projection
2.6.3 CCS termination
A variant of the empty process is given by the CCS voidCCSCCS : communicating concurrent processes process NIL voidNILNIL : a CCS constant\
[Milner1980]Milner, R.. We can extend the signature of BPA voidBPABPA : basic process algebra by the
constant NIL voidNILNIL : a CCS constant, and formulate the operational rules in table
15. These rules are taken from
[Aceto and Hennessy1992]Aceto, L.Hennessy, M..
Table: Derivation rules of [IMAGE ]_NIL[IMAGE ].
Table 17: [IMAGE ] in the presence of NIL.
2.7 Renaming in BPA
Table 18: Renaming.
Structural induction
In +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming we can use structural
induction just as in BPA voidBPABPA : basic process algebra, since closed +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming terms can be rewritten
into basic BPA voidBPABPA : basic process algebra terms. To that end, we will first prove that the term
rewriting system associated to +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming is strongly normalizing.
We display the rewrite rules concerning the renaming operators
in table 19. Note that, in rule RRN1, f(a) stands for
the atomic action that a is renamed into.
Table: A term rewriting system for +RN [IMAGE ].
Semantics
We give the semantics for +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming\
by means of a term deduction system [IMAGE ]+RN [IMAGE ], whose
signature is the one of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming and whose rules are the rules of
tables 5 and 20. Bisimulation equivalence
is a congruence, so the quotient of closed +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming terms modulo bisimulation
equivalence is well-defined. This means that the
operators of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming can be defined on this quotient,
which is a model of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming.
Table 20: Derivation rules concerning renaming operators.
Extensions of +RN [IMAGE ]
Recursion
We can add recursion to +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming in the same way as
we added recursion to BPA voidBPABPA : basic process algebra. The equational specification +RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming has as
its signature the signature of BPA rec voidBPArecBPA rec : BPA with recursion plus for all functions f from A
to A a renaming operator [IMAGE ]. The equations of +RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming are the
axioms of BPA rec voidBPArecBPA rec : BPA with recursion plus the axioms concerning renaming; see
table 18. We can turn the set of closed
+RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming terms into a model of +RN [IMAGE ]voidBPArec RN[IMAGE ]: BPA rec with renaming that
satisfies RDP voidRDPRDP : recursive definition principle and RSP voidRSPRSP : recursive specification principle as usual.
Projection
Projections can be added in an obvious way
to +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming: just add the projection functions and their axioms to the equational
specification +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming to obtain +PR [IMAGE ]voidBPA RN PR[IMAGE ]: +RN [IMAGE ] with
projections. The standard facts that hold
for +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections also hold for +PR [IMAGE ]voidBPA RN PR[IMAGE ]: +RN [IMAGE ] with
projections. As we did for +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections we can infer
that +PR [IMAGE ]voidBPA RN PR[IMAGE ]: +RN [IMAGE ] with
projections is sound and complete, and that AIP voidAIPAIP : approximation induction principle is valid.
Recursion and projection
The extension with both recursion and
projection of +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming, called +PR [IMAGE ]voidBPArec RN PR[IMAGE ]: +RN [IMAGE ]\
with projections, can be obtained just like in the
case of BPA voidBPABPA : basic process algebra.
2.7.2 Renaming in basic process algebra with deadlock
Structural induction
We can use structural induction as
before, since closed _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ]
with renaming terms can be rewritten into basic
_[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock terms. This follows from the next elimination theorem.
Semantics
The semantics for _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ]
with renaming can be given
just like the semantics for +RN [IMAGE ]voidBPA RN[IMAGE ]: BPA with renaming. Let [IMAGE ]_+RN [IMAGE ] be the term
deduction system with the signature of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ]
with renaming and with the rules
of tables 5 and 20. In the latter
table we further assume that [IMAGE ]. Since bisimulation equivalence
is a congruence, the quotient of the set of closed _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ]
with renaming terms with respect
to bisimulation equivalence is well-defined. This quotient is a model
of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ]
with renaming; from this, the completeness of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock, and the elimination result,
the completeness of _+RN [IMAGE ]voidBPAdelta RN[IMAGE ]: [IMAGE ]
with renaming follows.
Extensions of _+RN [IMAGE ] and _[IMAGE ]
Recursion and/or projection
Encapsulation
In most concurrency theories in which a
form of deadlock is present there usually is the notion of an
encapsulation or restriction operatorrestriction
operatoroperator!restriction; this is a renaming operator that
renames certain atomic actions into [IMAGE ]. The notion of encapsulation
and the notation [IMAGE ]voiddeltaH[IMAGE ]: encapsulation operator stem from
[Bergstra and Klop1984b]Bergstra, J.A.Klop, J.W.. The notion named
restriction is due to [Milner1980]Milner, R..
Table 21: The encapsulation operator.
Table 22: Derivation rules for the encapsulation operator.
2.7.4 Renaming in basic process algebra with empty process
Abstraction
Structural induction
We can use structural induction as
before, since closed +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]:
[IMAGE ] with renaming terms can be rewritten into basic
_()[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: [IMAGE ] or [IMAGE ] terms. This can be shown along the same lines as the elimination
theorem for the theory without the empty process; see, for
instance, theorem 2.7.2.
Semantics
The semantics of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]:
[IMAGE ] with renaming will be given by means
of a term deduction system. Let [IMAGE ]+RN [IMAGE ] be the term deduction
system with +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]:
[IMAGE ] with renaming as its signature and with rules displayed in
tables 12 and 23. Bisimulation
equivalence
is a congruence, so we can define the operators of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]:
[IMAGE ] with renaming\
on the quotient of closed +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]:
[IMAGE ] with renaming terms modulo bisimulation equivalence.
It is straightforward to prove that this is a model of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]:
[IMAGE ] with renaming.
The completeness of +RN [IMAGE ]voidBPAdeltaepsilon RN[IMAGE ]:
[IMAGE ] with renaming is also standard to prove.
Table 23: Derivation rules for renaming operators and empty process.
Look-ahead
If we allow renaming into the empty
process, we need two more derivation rules that concern renaming;
they introduce a look-aheadlook-ahead as can be seen
in table 24. The operational rules
that we list in this table are due to [Baeten and Glabbeek1987]Baeten,
J.C.M.Glabbeek, R.J. van.
Table: Extra rules when we allow renaming into [IMAGE ].
Extensions of +RN [IMAGE ] and _()[IMAGE ]
Recursion and/or projection
Encapsulation
The extension of _[IMAGE ]voidBPAdeltaepsilon[IMAGE ]: BPA \
with deadlock and empty process with the
encapsulation operator can be obtained in the same way as in the case without
the empty process; see subsection 2.7.3.
2.8 The state operator
In this subsection we extend BPA voidBPABPA : basic process algebra with the (simple) state operator, which
is a generalization of a renaming operator. It is a renaming operator
with a memory to describe processes with an independent global state.
We denote the state operator by [IMAGE ]; the subscript is the
memory cell containing the current state s. This subsection is based on
[Baeten and Bergstra1988a]Baeten, J.C.M.Bergstra, J.A.. Another treatment
of state operators can be found in [Verhoef1992]Verhoef, C..
Table 25: The axioms defining the state operator.
2.8.1 Termination and elimination
Next, it is our aim to show that the state operator can be eliminated.
Therefore, we will use that the term rewriting system associated to
_[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator is strongly normalizing. We will prove the latter fact with
the aid of the method of the recursive path ordering. However, we cannot
apply this method immediately. This is due to the fact that we cannot
hope to find a strict partial ordering on the signature of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator\
that does the job. The problematical rule is the rewrite rule RSO2 (see
table 26).
Suppose that we have one atomic action a. Let us have two different
states, which shall remain nameless. Take an inert action function,
that is it does nothing, and let the effect function act as a switch.
This yields the following instantiation for the rewrite rule RSO2:
Table 26: The rewrite rules for the simple state operator.
Semantics
We give the semantics for _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator\
by means of a term deduction system [IMAGE ]_[IMAGE ]. Its
signature is that of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator and its rules are the rules of
tables 5 and 27. According to
theorem 2.2.32 bisimulation equivalence is a
congruence so the operators of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator can be defined on the quotient
of the closed _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator terms modulo bisimulation equivalence. Moreover,
it is a model of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator. With the aid of the method explained
in subsection 2.4.1, it is not hard to see that _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator\
is a conservative extension of BPA voidBPABPA : basic process algebra. Then it easily follows with
theorem 2.4.26 that the axioms in tables 1
and 25 constitute a complete axiomatization of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator.
Table: Derivation rules of [IMAGE ]_[IMAGE ].
Extensions
2.9 The extended state operator
In the following, we will discuss BPA voidBPABPA : basic process algebra with the extended state operator,
which is
a generalization of the simple state operator. We denote the extended
state operator by [IMAGE ]. The difference with the (simple)
state operator is that we can rename an atomic action into a closed term of
a particular form, namely a finite sum of atomic actions. With this extra
feature it is possible to translate an instruction like read(x)
into process algebra.
Table 28: The axioms defining the generalized state operator.
Table: Derivation rules of [IMAGE ]_[IMAGE ].
Termination
In the previous subsection
(2.8) we mentioned that we cannot use the method of
the recursive path ordering immediately. The same phenomenon occurs with
the extended state operator. Fortunately, the solution of the problems
is the same as for the simple state operator. We have to define ranked
extended state operators and prove the termination of this system.
We omit the details and refer to subsection 2.8 for
more information. We only mention the main result.
Table 30: The rewrite rules for the extended state operator.
Semantics
We give the semantics for _[IMAGE ]voidBPALambda[IMAGE ]: BPA
with the extended state operator\
by means of a term deduction system [IMAGE ]_[IMAGE ].
Its signature is that of _[IMAGE ]voidBPALambda[IMAGE ]: BPA
with the extended state operator and its rules are the
rules of tables 5 and 29.
According to 2.2.32 bisimulation equivalence is
a congruence so the quotient of the closed _[IMAGE ]voidBPALambda[IMAGE ]: BPA
with the extended state operator terms modulo
bisimulation equivalence is well-defined. Moreover, it is easily
seen that the quotient is a model of _[IMAGE ]voidBPALambda[IMAGE ]: BPA
with the extended state operator. With the theory of
section 2.4.1, we find that _[IMAGE ]voidBPALambda[IMAGE ]: BPA
with the extended state operator is a conservative
extension of BPA voidBPABPA : basic process algebra. With the termination theorem 2.9.1
and an elimination result, similar to 2.8.4,
we find using theorem 2.4.26 that the axioms of
tables 1 and 28 constitute a complete
axiomatization of _[IMAGE ]voidBPALambda[IMAGE ]: BPA
with the extended state operator.
Extensions
2.10 The priority operator
In this subsection we introduce _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with the priority operator that
originates from [Baeten et al.
1986]Baeten, J.C.M.Bergstra,
J.A.Klop, J.W..
Table 31: The axioms defining the unless operator.
Table 32: The axioms defining the priority operator.
Intuition
The partial order < is used in order to describe
which actions have priority over other actions. If for instance a<b
and b and c are not related we want to have that [IMAGE ]
and [IMAGE ]. The priority operator thus respects the
alternative composition for actions without priority but gives the
alternative with the highest priority, in the < hierarchy, if the sum
contains prioritized actions. A typical example of a low priority action
is an atomic action expressing time-out behaviour: as long as there are
alternatives with a higher priority no time-out will be performed within
the scope of the priority operator. The priority operator has been used
to specify and verify time critical protocols in an untimed setting;
see, for instance, [Vaandrager1990b]Vaandrager, F.W..
Table 33: Rewrite rules for the unless operator.
Table 34: The rewrite rules for the priority operator.
2.10.1 Semantics of basic process algebra with priorities
Table 35: Derivation rules for the priority operator.
Table 36: Derivation rules for the unless operator.
2.10.2 Conservativity
Extensions of _[theta][IMAGE ]
In this subsection we discuss extensions of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator with the notions
of recursion, projections, renaming, and/or the encapsulation operator, and
the state operator. In fact, all extensions but the one with recursion
can be obtained just as for the BPA voidBPABPA : basic process algebra or _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock case.
Recursion
The problem with the extension of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\
with recursion is purely technical. Since there are negative premises in
the operational characterization of the priority and unless operators,
we introduced the notion of a stratification to ensure that the
semantical rules indeed define a transition relation. We recall that in
example 2.10.10 we give a stratification for the operational
semantics of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator. The map defined there counts the total number of
occurrences of [IMAGE ] and [IMAGE ]. This approach no longer works in
the presence of the operational rules for recursion that we presented in
table 6. We illustrate this with a simple example.
Suppose that we have the following recursive specification:
Projection
Renaming and encapsulation
It is straightforward to extend
the equational specification _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator with renaming operators or the
encapsulation operator; cf. subsection 2.7.3.
State operator
The extension of the theory _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\
with either the simple or extended state operator is obtained in the
same way as for the theory BPA voidBPABPA : basic process algebra; see subsections 2.8
and 2.9.
Inconsistent combinations
Remarkably, if we combine recursion
with the equational specification _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator plus renaming operators
we will find an inconsistency. [Groote1990b]Groote, J.F. gives
the following example. Take a renaming function f such that
Consider the recursive equation
2.11 Basic process algebra with iteration
In this subsection we extend basic process algebra with an iterative
construct. This construct is, in fact, Kleene's star operator, a binary
infix operator denoted *. We will call this operator Kleene's
binary star operator, since there are two versions of Kleene's star
operator: one unary and one binary. The binary construct originates from
[Kleene1956]Kleene, S.C. and its more commonly known unary version
is due to [Copi et al.1958]Copi, I.M.Elgot, C.C.Wright,
J.B.. This subsection is based on the papers [Bergstra et al.
1994a]Bergstra,
J.A.Bethke, I.Ponse, A. and [Fokkink and Zantema1994]Fokkink,
W.J.Zantema, H..
The theory
The equational specification ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration consists
of the signature of BPA voidBPABPA : basic process algebra and a binary infix operator *voidA AAG*:
Kleene's binary star operator, called Kleene's binary star
operatorKleene's binary star operatoroperator!Kleene's
binary star. Its equations are the ones of BPA voidBPABPA : basic process algebra plus the axioms in
table 37voidBKS!-3BKS1-3: iteration axioms.
Table 37: The axioms defining Kleene's binary star operator.
Semantics
We give the semantics of the equational
specification ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration by means of a term deduction
system [IMAGE ]^*[IMAGE ]. Its signature is the signature of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration.
Its deduction rules are the rules for BPA voidBPABPA : basic process algebra that we met many times
before (see table 5) plus the rules that characterize
Kleene's binary star operator. We list them in table 38.
Table 38: Operational rules for Kleene's binary star operator.
Extensions of ^*[IMAGE ]
The extension of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration with
deadlock (^*[IMAGE ]voidBPAdeltastar[IMAGE ]: [IMAGE ]
with iteration) is as usual. This system is obtained by
taking the syntax of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock plus Kleene's binary operator *. The axioms
of ^*[IMAGE ]voidBPAdeltastar[IMAGE ]: [IMAGE ]
with iteration are the ones of ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration plus those for deadlock.
2.12 Basic process algebra with discrete relative time
Theory
The equational specification _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time has as its
signature the one of BPA voidBPABPA : basic process algebra and a unary function called discrete time
unit delaydiscrete time unit delaytime!discrete,
which is denoted [IMAGE ]voidsigmad[IMAGE ]: discrete time unit
delay. The [IMAGE ] is some fixed symbol, which is a measure for the
delay. The axioms of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time are the ones of BPA voidBPABPA : basic process algebra that we listed in
table 1 plus the equations defining the discrete time unit
delay; see table 39voidDT1-2DT1-2: [IMAGE ] axioms.
Table 39: The axioms defining the discrete time unit delay.
Table 40: The rewrite rules for the discrete time unit delay.
Semantics
Next, we formally define the semantics by way of a
term deduction system for _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time. The signature of this system consists
of the one for the equational specification _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time. The deduction
rules are those for + and [IMAGE ] of BPA voidBPABPA : basic process algebra in table 1,
and the rules for constants and the discrete time unit delay in
table 41.
Table 41: The operational semantics for the discrete time unit delay.
Extensions of _dt[IMAGE ]
Deadlock
We can extend _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time with deadlock in the
usual way. We abbreviate this equational specification as _dt[IMAGE ]voidBPAdeltadt[IMAGE ]:
[IMAGE ] with discrete time.
The axioms for [IMAGE ] are the usual ones for deadlock; see
table 10. The termination proof is a combination
of these proofs for _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time and _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock. The notion of a basic term
needs a little modification: [IMAGE ] is an A-basic term. The
operational semantics is the same as the one for _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time. The soundness
and completeness are proved along the same lines as the case _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time.
The conservativity of _dt[IMAGE ]voidBPAdeltadt[IMAGE ]:
[IMAGE ] with discrete time over _()[IMAGE ]voidBPAdelta[IMAGE ]: BPA or
[IMAGE ] is obtained as usual.
Recursion
The extension of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time with recursion has the
same technical problem as the extension of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator with recursion.
We recall that the problem is that we need to define a new stratification
on the operational rules of _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time with recursion in order to guarantee
that the transition relation is well-defined. For a solution we refer
to subsection 2.10.3 where extensions of _[theta][IMAGE ]voidBPAdeltatheta[IMAGE ]: [IMAGE ] with the priority operator\
are discussed.
2.13 Basic process algebra with other features
Abstraction
In this survey we only treat concrete process
algebra, hence any extension of the systems that we discuss with some
notion of abstractionabstraction will not be covered by this
survey. For more information on process algebras that incorporate
abstraction we mention [Bergstra and Klop1985]Bergstra, J.A.Klop,
J.W. that treats an extension of BPA voidBPABPA : basic process algebra with abstraction. Other systems
that feature abstraction are CCS voidCCSCCS : communicating concurrent processes [Milner1980, Milner1989]Milner,
R., Hennessy's system [Hennessy1988]Hennessy, M., and CSP voidCSPCSP : communicating sequential processes\
[Hoare1985]Hoare, C.A.R.. We note that the latter two systems
are not extensions of BPA voidBPABPA : basic process algebra but treat basic notions in a different way.
But also CCS voidCCSCCS : communicating concurrent processes is not an extension of BPA voidBPABPA : basic process algebra because there is no sequential
composition in CCS voidCCSCCS : communicating concurrent processes.
Backtracking
A well-known notion in logic programming
is backtrackingbacktracking. [Bergstra et al.
1994c]Baeten,
J.C.M.Ponse, A.Wamel, J.J. van extended process algebra
with this notion. They discuss an algebraic description of backtracking
by means of a binary operator. For more details on this extension we
refer to [Bergstra et al.
1994c]Baeten, J.C.M.Ponse, A.Wamel,
J.J. van.
Combinatory logic
In [Bergstra et al.
1994b]Bergstra,
J.A.Bethke, I.Ponse, A., process algebra is extended
with combinatory logiccombinatory logic. An interesting point of
this combination is the possibility to verify the well-known alternating
bit protocol without any conditional axiom, that is, the verification
is purely equational. For more information on this combination and
the equational verification we refer to [Bergstra et al.
1994b]Bergstra,
J.A.Bethke, I.Ponse, A..
Real-time
In recent years, much effort has been spent on the
extension of several process algebras with a notion of time. We discuss
in this survey just one such extension: process algebra with relative
discrete time. However, there are many more (concrete) extensions
present in the literature. We mention the distinction between relative
and absolute time, and the choice of the time domain: discrete or dense.
We refer to [Klusener1993]Klusener, A.S. for more information on
real timereal timetime!real process algebra in many
and diverse forms.
Real-space
In [Baeten and Bergstra1993]Baeten,
J.C.M.Bergstra, J.A. a form of real time process algebra
is extended with real spacereal space. The paper surveys
material from former reports on this topic. We refer the interested
reader to [Baeten and Bergstra1993]Baeten, J.C.M.Bergstra, J.A.
for more information.
Nesting
In this survey, we discuss the extension of process
algebra with iteration, or Kleene's binary star. An extension that we
do not discuss is one with an operator called the nestingnesting
operatoroperator!nesting operator. Like Kleene's binary star
operator, the nesting operator also is a recursive operator (though it
defines irregular recursion). We refer to [Bergstra et al.
1994a]Bergstra,
J.A.Bethke, I.Ponse, A. for more information on this
topic.
Signals
In [Baeten and Bergstra1992b]Baeten, J.C.M.Bergstra,
J.A. process algebra is extended with stable signalsstable
signalsignal!stable. These are attributes of states of
a process. They introduce a signal insertionsignal insertion
operatoroperator!signal insertion and a signal termination
operatorsignal termination operatoroperator!signal
termination to be able to describe signals with a certain duration.
A typical example that can be described with this theory is a traffic
light system. For more information on the extension with signals we
refer to [Baeten and Bergstra1992b]Baeten, J.C.M.Bergstra, J.A..
Conditionals
An extension with conditionals or
guards can be found in the just mentioned paper [Baeten and Bergstra1992b]Baeten,
J.C.M.Bergstra, J.A.. They introduce an
if-then-elseif-then-else operator operator in the notation of
[Hoare et al.
1987]Hoare, C.A.R.Hayes, I.J.He,
JifengMorgan, C.C.Roscoe, A.W.Sanders,
J.W.Sorensen, I.H.Spivey, J.M.Surfin, B.A..
[Baeten and Bergstra1992b]Baeten, J.C.M.Bergstra, J.A. also
introduce a variant of this conditional operator, called the guarded
commandguarded commandcommand!guarded that originates
from [Baeten et al.
1991]Baeten, J.C.M.Bergstra, J.A.Mauw,
S.Veltink, G.J.. [Groote and Ponse1994]Groote, J.F.Ponse,
A. developed a substantial amount of theory for a similar conditional
construct called a guardguard.
Invariants and assertions
Probabilities
2.14 Decidability and expressiveness results in BPA
2.14.1 Decidability
2.14.2 Expressiveness
Figure: The deduction graph of the counter C.
Recursion versus iteration
In subsection 2.3
we discussed the extension of BPA voidBPABPA : basic process algebra with recursion. In subsection
2.11 we discussed a similar construct: iteration.
We can compare both approaches in the following sense: ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration is
less expressive than BPA lin voidBPAlinBPA lin : BPA with finite linear recursion. BPA lin voidBPAlinBPA lin : BPA with finite linear recursion is BPA rec voidBPArecBPA rec : BPA with recursion where only finite
linear specifications are allowed[+].
In other words, ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration does not contain non-regular processes.
In [Bergstra et al.
1994a]Bergstra, J.A.Bethke, I.Ponse, A.
a simple example is given that shows the strictness of the inclusion.
Consider the following regular process:
Figure 7: The deduction graph of a regular process.
3 Concrete concurrent processes
Up to now, we have discussed the language BPA voidBPABPA : basic process algebra with many of its
extensions. Next, we want to discuss an extension of such significance
that we devote a new section to it. It is the notion of parallelism or
concurrency that we add to our family of basic systems that we treated in
the previous section. We will restrict ourselves to concrete concurrency;
that is, we do not consider abstraction.
3.1 Introduction
3.2 Syntax and semantics of parallel processes
3.2.1 The theory PA
We will discuss the equational theory [IMAGE ]. This
section is based on [Bergstra and Klop1982]Bergstra, J.A.Klop, J.W..
Intuition
Table 42: Axioms for the free merge.
Structural induction
Table: A term rewriting system for PA.
Termination
Next, it is our aim to prove that the term
rewriting system associated to the equational specification PA voidPAPA : process algebra is
strongly normalizing. In subsection 2.2.2 we already
discussed the powerful method of the recursive path ordering. Indeed,
we will use this method to prove the desired result but we cannot
apply it immediately. We recall that the termination problem more
or less reduces to finding the appropriate strict partial ordering
on some operators in the signature. The problem that we have with
this particular system is that we cannot define a consistent partial
ordering on the elements of the signature. First, we will explain
this problem and then we will see that a possible solution can be
obtained in the same way as for the termination of _[IMAGE ]voidBPAlambda[IMAGE ]: BPA with
the simple state operator; see
section 2.8.1. The problematical pair
consists of the rules [IMAGE ]. Analysing this pair we find that if
we take the rule RM1 on the one hand, the ordering that does the job
is [IMAGE ][IMAGE ]. On the other hand, if we look at RM3,
the right choice is the other way around: [IMAGE ][IMAGE ].
This particular problem is tackled by [Bergstra and Klop1985]Bergstra,
J.A.Klop, J.W.. More detailed information on this problem
can be found in a survey on term rewriting that appeared in this
series [Klop1992, remark 4.11,16ex(ii,16ex),]Klop, J.W..
The idea of [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W.
was to equip the operators [IMAGE ][IMAGE ] and [IMAGE ] with a rank.
Thus yielding a ranked signature for which it is possible to define the
desired strict partial ordering. To formalize the ranked signature
we first need a notion termed ``weight''. Its definition stems
from [Bergstra and Klop1985]Bergstra, J.A.Klop, J.W.. Note that we
already defined this notion in the case of BPA voidBPABPA : basic process algebra with the state operator;
see definition 2.8.1.
Standard concurrency
Some properties concerning both
merges cannot be derived from PA voidPAPA : process algebra, but can only be proved for closed
PA voidPAPA : process algebra terms, for instance the associativity of the merge. In many
applications these properties are useful and thus assumed to hold.
Hence, following [Bergstra and Tucker1984]Bergstra, J.A.Tucker, J.V.,
they are often referred to as axioms for standard
concurrencyaxiom!standard concurrencystandard
concurrency. In the next theorem we will treat two such equalities.
Expansion
An important result in PA voidPAPA : process algebra with standard
concurrency is the so-called expansionexpansion theorem, which
is a generalization of axiom M1 ,16ex(see
[Bergstra and Tucker1984]Bergstra, J.A.Tucker, J.V.,16ex). It tells us how
the merge of more
than two processes can be evaluated. For instance, the merge of three
processes x,y, and z yields
Semantics of PA
Table: Derivation rules of [IMAGE ].
Extensions of PA
Recursion
Here we will add recursion to PA voidPAPA : process algebra. This is done in
the same way as we did for BPA voidBPABPA : basic process algebra.
Projection
We can extend the equational specification PA voidPAPA : process algebra\
with projections as we did for BPA voidBPABPA : basic process algebra. The equational specification +PR [IMAGE ]voidPA PR[IMAGE ]: PA with projections\
has as its signature the one of +PR [IMAGE ]voidBPA PR[IMAGE ]: BPA with projections plus the two binary
operators [IMAGE ][IMAGE ] and [IMAGE ] present in the signature of PA voidPAPA : process algebra.
Its axioms are the ones of PA voidPAPA : process algebra plus the axioms concerning projections;
see table 7.
Recursion and projection
Here we will extend PA voidPAPA : process algebra with both
recursion and projection. This extension is obtained analogously to the
extension of BPA voidBPABPA : basic process algebra with recursion and projection. The
specification +PR [IMAGE ]voidPArec PR[IMAGE ]: PA rec with
projections has as its signature the one of PA rec voidPArecPA rec : PA with recursion plus
the unary operators [IMAGE ] that occur in the signature of +PR [IMAGE ]voidPA PR[IMAGE ]: PA with projections. Its
axioms are the ones of PA rec voidPArecPA rec : PA with recursion plus the axioms concerning projection;
see table 7. The results that we obtained
for +PR [IMAGE ]voidBPArec PR[IMAGE ]: [IMAGE ] with
projections in subsection 2.4.2 also hold
for +PR [IMAGE ]voidPArec PR[IMAGE ]: PA rec with
projections. We will not mention them here.
Renaming
It is not difficult to extend the equational
specification PA voidPAPA : process algebra, and its extensions, with renaming operators; see
subsections 2.7 and 2.7.1.
State operator
We can extend the theory PA voidPAPA : process algebra with either
the simple or extended state operator in the same way as we did for the
theory BPA voidBPABPA : basic process algebra. For details we refer to subsections 2.8
and 2.9.
Iteration
We can extend PA voidPAPA : process algebra with iteration by just adding the
defining axioms for [IMAGE ] in table 37 to the ones for PA voidPAPA : process algebra.
For this theory there is no completeness result present at the time of
writing this survey.
3.3.1 Process creation
In this subsection, we discuss an extension of PA voidPAPA : process algebra with an operator
that models process creation. This extension is not present in BPA voidBPABPA : basic process algebra\
since it is defined using the parallel composition [IMAGE ][IMAGE ].
This subsection is based on [Bergstra1990]Bergstra, J.A.. We refer
to [America and Bakker1988]America, P.Bakker, J.W. de and to
[Baeten and Vaandrager1992]Baeten, J.C.M.Vaandrager, F.W. for other
approaches to process creation.
The theory
The equational specification +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process
creation (process
algebra with process creationprocess creation) is defined
in stages. First we take the theory PA voidPAPA : process algebra where we assume that the
set of atomic actions A contains some special actions: for all d
in some data set D we assume that [IMAGE ]voidcrd[IMAGE ]: creation
action and [IMAGE ]voidcrd[IMAGE ]:
trace of [IMAGE ]. We moreover assume the existence of a
function, the process creation functionprocess creation
functionfunction!process creation, [IMAGE ]voidphi[IMAGE ]:
process creation function on D that assigns to each [IMAGE ] a process
term [IMAGE ] over PA voidPAPA : process algebra with the above set of atomic actions A. Using
the function [IMAGE ] we add a unary operator [IMAGE ]voidEphi[IMAGE ]:
process creation operator to the signature, thus obtaining the signature
of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process
creation. The operator [IMAGE ] is called the process creation
operatorprocess creation operatoroperator!process
creation.
Table 45: Axioms for the process creation operator.
Intuition
We provide some intuition for +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process
creation. We will
compare process creation with the UNIXUNIX[+] system callsystem
callcall!system forkfork; see
[Ritchie and Thompson1974]Ritchie, D.M.Thompson, K.. We recall
that with fork we can only create an exact copy (child
processchild processprocess!child) of its so-called
parent processparent processprocess!parent. We note
that with the process creation operator we are able to create arbitrary
processes but to provide an intuition for process creation the system
call fork is illustrative.
Termination
The above example shows that the term rewriting
system associated to +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process
creation (by orienting the axioms of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process
creation from left
to right) is, in general, not terminating. For, in case of the above
example, we have the following infinite sequence of rewritings:
Semantics
We discuss the operational semantics of +PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process
creation. It
is obtained by means of a term deduction system. The signature is that of
+PCR [IMAGE ]voidPA PCR[IMAGE ]: PA with process
creation; the operational rules are those of PA voidPAPA : process algebra plus the rules that
operationally define the process creation operator [IMAGE ]. We list them
in table 46. The rules of this table originate from
[Baeten and Bergstra1988b]Baeten, J.C.M.Bergstra, J.A..
Table 46: Operational rules for the process creation operator.
3.3.2 Deadlock in PA
Structural induction
Standard concurrency
Expansion
For _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with standard concurrency we have
the same expansionexpansion theorem as for the theory without
deadlock, so for expansion we refer to theorem 3.2.6.
Semantics
The semantics of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock can be given by means of
a term deduction system [IMAGE ]_[IMAGE ], which is just [IMAGE ] with [IMAGE ]
added to its signature. The operators of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock can be easily defined by
taking representatives on the quotient of the set of closed _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock terms
modulo bisimulation equivalence, since this relation is a congruence;
see 2.2.32. The quotient is a model for _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock,
which can be easily checked by combining the soundness proofs for _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock\
and PA voidPAPA : process algebra. Moreover, the axiom system _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock is a complete axiomatization
of this quotient. This follows immediately from the completeness of PA voidPAPA : process algebra\
since we did not introduce any new transitions.
3.3.3 Asynchronous communication
asynchronous
communicationcommunication!asynchronous
It is straightforward to extend _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with any of the features mentioned in
the beginning of subsection 3.3. Here, we consider an
application of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with the (simple) state operator. We describe mail
through a communication channel. Let D be a finite data set and let c
be a communication channel. We assume that for each [IMAGE ] we have the
following special atomic actions:
The state operator will turn potential, intended actions into realized
actions. The state space will keep track of outstanding messages.
3.3.4 Empty process in PA
We
will not discuss the combination of parallel composition and the
empty processempty processprocess!empty, since
this combination is not (yet) standardized. At this moment there
are two possible ways to combine the merge and the empty process.
These options originate from the various interpretations of the
term [IMAGE ]. It may seem natural to demand that
this equals x, since [IMAGE ] is only capable of terminating
successfully, but this perspective leads to a non-associative merge, which
is rather unnatural and therefore unwanted [Vrancken1986]Vrancken,
J.L.M.. The intended interpretation of the left merge is that
of the merge with the first action from the left process, so the
term [IMAGE ] cannot proceed, since [IMAGE ] cannot
perform an action. One of the options is that [IMAGE ]
equals [IMAGE ] except if [IMAGE ]: then it equals [IMAGE ];
see [Vrancken1986]Vrancken, J.L.M. for more information. The other
option drops this exception and uses a unary operator indicating
whether or not a process has a termination option to axiomatize the
merge [Baeten and Glabbeek1987]Baeten, J.C.M.Glabbeek, R.J. van.
Extensions of _[IMAGE ]
Recursion and/or projection
Renaming and encapsulation
It is straightforward to extend
the equational specification _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock, and its extensions, with renaming
operators or the encapsulation operator;
cf. subsection 2.7.3.
State operator
The extension of the theory _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with
either the simple or extended state operator is obtained in the
same way as for the theory PA voidPAPA : process algebra; see subsections 2.8
and 2.9.
Priority operator
We can extend the theory _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with
the priority operator in the same way as the extension of _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock\
with that operator. For details of that extension we refer to
section 2.10.
Iteration
We can extend _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with iteration by just adding the
defining axioms for [IMAGE ] in table 37 to the ones for _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock.
Only for ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration is the completeness proved at the time of writing this
survey.
Process creation
We can extend _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with the process creation
operator [IMAGE ] in the same way as we did for PA voidPAPA : process algebra. For details we refer
to subsection 3.3.1.
3.4.1 Discrete time
The theory
We discuss the equational specification _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ]
with discrete time.
Its signature is the one of _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock (with [IMAGE ] instead of a
for [IMAGE ]) plus the discrete time unit delay operator [IMAGE ]
that we first introduced in _dt[IMAGE ]voidBPAdt[IMAGE ]: BPA with
discrete time. The equations of _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ]
with discrete time are
the ones of _dt[IMAGE ]voidBPAdeltadt[IMAGE ]:
[IMAGE ] with discrete time plus the equations for the merge that we listed
in table 42 (again with [IMAGE ] instead of a)
and the equations that represent the interaction between the left
merge and the discrete time unit delay; we list the latter axioms in
table 47voidDTM1-4DTM1-4: discrete time/merge axioms.
Incidentally, this axiomatization is new here.
Table 47: The interaction between the left merge and the discrete time unit
delay.
Termination
Next, we discuss the
termination of a term rewriting system associated to the equational
specification _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ]
with discrete time. Since we have the left merge in our signature we
use the ranked operators that we also used for the
termination of PA voidPAPA : process algebra; cf. subsection 3.2.1.
Elimination
Semantics
Table 48: The additional rules for the merge and the left merge.
3.5 Syntax and semantics of communicating processes
In this subsection we will extend the meaning of the parallel
operator [IMAGE ][IMAGE ] that we introduced in subsection 3.2.
We will call the ensuing operator [IMAGE ][IMAGE ] the
merge or parallel composition. We use the name free merge
for the merge without communication, that is the merge of PA voidPAPA : process algebra.
3.5.1 The theory ACP
Table 49: Axioms for the merge with communication.
Terminology
We say that two atomic actions do not communicate
if the communication function is not defined for them. We say that an
atomic action a is a communication
actioncommunication actionaction!communication
if [IMAGE ] for atomic actions b and c. A communication
action [IMAGE ] is called a binary communicationbinary
communicationcommunication!binary; likewise [IMAGE ] is
called ternaryternary communicationcommunication!ternary
if defined. However, most of the time just using binary communication is
enough in applications. See also later on when we discuss so-called
handshaking.
Read/send communication
An important case of binary
communication is called read/send communicationread/send
communicationcommunication!read/send. The idea is that
in the set of atomic actions we have read actionsread
actionaction!read [IMAGE ]voidrid[IMAGE ]:
read d at port i, send actionssend
actionaction!send [IMAGE ]voidsid[IMAGE ]: send d at port
i, and communication actions [IMAGE ]voidcid[IMAGE ]: communicate d
at port i. The intended meaning of [IMAGE ] is to read datum [IMAGE ] at portport i, where the set D is some finite data set.
For [IMAGE ] a similar intuition holds. Now [IMAGE ] is the result of a
communication of [IMAGE ] and [IMAGE ]: it means transmit the datum d
by communication at port i. The appropriate communication function
is [IMAGE ]
and [IMAGE ] is not defined otherwise on [IMAGE ], [IMAGE ], and [IMAGE ]
(for ports i,j,k and data elements d,e,f). For other atomic
actions it is permitted to have some communications defined. The above
conventions are due to [Bergstra and Klop1986]Bergstra, J.A.Klop,
J.W.. An example of the use of read/send communication is given in
section 3.6.
Structural induction
As before we can use structural induction
for ACP voidACPACP : algebra of communicating processes, since basic ACP voidACPACP : algebra of communicating processes terms are just basic _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock terms.
This follows from theorem 3.5.5 that states that
parallel composition and encapsulation can be eliminated from closed
ACP voidACPACP : algebra of communicating processes terms.
3.5.2 Termination
Table 50: Term rewriting rules for the merge.
Figure 8: Partial ordering of the operators in the term rewriting
system associated to ACP.
Standard concurrency
As for PA voidPAPA : process algebra we have standard
concurrency. That is, there are some properties concerning the
merge, left merge, and communication merge that are not derivable for
arbitrary open terms, but can be shown to be valid for closed terms
(or even for solutions of guarded recursive equations). In many
applications these properties are useful and thus these properties are
assumed to be valid. This is why these properties are often
referred to as axioms for standard concurrencyaxiom!standard
concurrencystandard concurrency. In the next theorem we list
them for ACP voidACPACP : algebra of communicating processes. See theorem 3.2.5 for standard concurrency in PA voidPAPA : process algebra.
Expansion
A useful application of standard concurrency in
ACP voidACPACP : algebra of communicating processes is the so-called
expansionexpansion theorem. This theorem states how the merge
of more than two processes can be evaluated. For the expansion theorem
of PA voidPAPA : process algebra we refer to theorem 3.2.6. In contrast to the
PA voidPAPA : process algebra expansion theorem, we need an extra proviso for the expansion of the
merge in case the communication merge is present. We need a so-called
handshaking axiomhandshaking axiomaxiom!handshaking
(HAvoidHAHA: handshaking axiom). We give it in table 51.
It states that there is only binary communication present.
Table 51: Handshaking axiom.
3.5.3 Semantics of ACP
Table 52: The operational rules for the communication merge.
3.6 Extensions of ACP
Recursion and/or projection
Renaming and encapsulation
It is straightforward to extend
the equational specification ACP voidACPACP : algebra of communicating processes, and its extensions, with renaming
operators; cf. subsection 2.7.3.
State operator
The extension of the theory ACP voidACPACP : algebra of communicating processes with
either the simple or extended state operator is obtained in the
same way as for the theories BPA voidBPABPA : basic process algebra or PA voidPAPA : process algebra; see
subsections 2.8 and 2.9.
Priority operator
We can extend the theory ACP voidACPACP : algebra of communicating processes with
the priority operator in the same way as we extended _[IMAGE ]voidBPAdelta[IMAGE ]: BPA with deadlock with that
operator. For the details we refer to subsection 2.10.
Iteration
We can extend ACP voidACPACP : algebra of communicating processes with iteration by adding
the defining axioms for [IMAGE ] in table 37 to the
ones for ACP voidACPACP : algebra of communicating processes and one more axiom that gives the relation between
Kleene's star and the encapsulation operator. We give this axiom in
table 53voidBKS4BKS4: iteration/encapsulation axiom.
We denote this system by ^*[IMAGE ]voidACPstar[IMAGE ]: ACP with iteration. Only for ^*[IMAGE ]voidBPAstar[IMAGE ]: BPA with iteration the completeness
is proved at the time of writing this survey.
Table 53: An extra axiom for Kleene's binary star operator.
Process creation
We discuss the extension of ACP voidACPACP : algebra of communicating processes with
the process creation operator [IMAGE ] (for the basic definitions we
refer to subsection 3.3.1). We recall that the process
creation operator is defined in terms of the parallel composition.
So it will not be surprising that we need to impose restrictions on
the communication behaviour of the special atomic actions [IMAGE ].
The restrictions are that [IMAGE ] does not communicate and is not the
result of any communication ([IMAGE ] is not a communication action).
In a formula: [IMAGE ]|[IMAGE ] and for all [IMAGE ]|[IMAGE ]. We note that lemma 3.3.1 only holds when the
communication function is trivial; that is, for all [IMAGE ]
is undefined.
Inconsistent combinations
If we combine unguarded
recursion with _[theta][IMAGE ]voidACPtheta[IMAGE ]: ACP with the
priority operator we will find
an inconsistency. We show this with an example that originates from
[Baeten and Bergstra1988b]Baeten, J.C.M.Bergstra, J.A.. Suppose that
there are three atomic actions r, s, and c and [IMAGE ]|[IMAGE ].
Let c>s be the partial ordering. Now consider the following recursion
equation: 3.6.1 Discrete time
In this subsection we add relative discrete time to ACP voidACPACP : algebra of communicating processes.
In subsection 3.4.1, we already extended _[IMAGE ]voidPA delta[IMAGE ]: PA with deadlock with
this feature. So we only need to clarify the interaction between the
discrete time unit delay [IMAGE ] and the communication merge and the
relation between [IMAGE ] and the encapsulation operator.
The theory
The equational specification _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with
discrete time\
consists of the signature that is the union of the signatures
of ACP voidACPACP : algebra of communicating processes (with [IMAGE ] instead of a for [IMAGE ])
and _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ]
with discrete time. The equations of this specification are the ones
of ACP voidACPACP : algebra of communicating processes (again with [IMAGE ] instead of a) plus the rules
of table 47 (they represent the interaction
between [IMAGE ] and the left merge) and some new axioms that we present
in table 54; they express the interaction between
the discrete time unit delay operator and the communication merge and
the interaction between [IMAGE ] and the encapsulation operator.
Table: The interaction between [IMAGE ] and communication and
encapsulation.
Termination
The termination of a term rewriting system
associated to _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with
discrete time can be obtained with the aid of the method
that we discussed in subsection 2.2.2. We can prove the
termination by merging the termination proofs of ACP voidACPACP : algebra of communicating processes and _dt[IMAGE ]voidPAdeltadt[IMAGE ]: [IMAGE ]
with discrete time\
and a small addition.
Semantics
The semantics of _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with
discrete time can be given with a
term deduction system [IMAGE ]_dt[IMAGE ]. Its signature is that of _dt[IMAGE ]voidACPdt[IMAGE ]: ACP with
discrete time.
The rules are those of ACP voidACPACP : algebra of communicating processes (with [IMAGE ] instead of a for [IMAGE ]), those in table 48 (they concern the
merge and the left merge), and the operational rules that we present in
table 55. The two rules in table 55
define what kind of [IMAGE ] transitions the communication merge and
the encapsulation operator can perform.
Table 55: The additional rules for the communication merge and the encapsulation
operator.
3.7 Decidability and expressiveness results in ACP
3.7.1 Decidability
Basic parallel processes
basic parallel processes
We will introduce the syntax and semantics of BPP voidBPPBPP : basic parallel processes below using
the notation that we are used to in this survey. We have
a special constant [IMAGE ], alternative composition +,
parallel composition [IMAGE ][IMAGE ], and a unary prefix operator [IMAGE ],
called prefix sequential compositionprefix sequential
compositioncomposition!prefix sequential, for all [IMAGE ],
where A is some set. Now if we also add recursion we have the syntax
of BPP voidBPPBPP : basic parallel processes.
Table 56: The operational semantics of BPP.
3.7.2 Expressiveness
The bag
We consider a so-called bagbag of unbounded
capacity. A bag is a process able to input data elements that reappear
in some arbitrary order. Let D be a finite set of such datum elements
containing more than one datum. Suppose that we have atomic actions
for all [IMAGE ]:
The following recursive equation formally defines the bag.
Figure 9: A deduction graph of a bag over two datum elements.
Figure 10: A FIFO queue.
The queue
A queuequeue is a process that
transmits incoming data while preserving their order. See also
figure 10. Such a process is also called a FIFO
(First In First Out) queueFIFO queuequeue!FIFO.
First, we describe the queue with input port 1 and output port 2 over
a finite data set D by means of an infinite linear specification.
As in 3.3.3, [IMAGE ] is the set of words over D.
Figure 11: A deduction graph for the queue.
Figure 12: Expressivity results for systems with iteration.
Recursion versus iteration
4 Further reading
For those readers who want to know more about process algebra, we
give some references. First of all, we want to mention a couple of
textbooks in the area. A textbook for CCS voidCCSCCS : communicating concurrent processes-style process algebra
is [Milner1989]Milner, R., for CSP voidCSPCSP : communicating sequential processes style we refer to
[Hoare1985]Hoare, C.A.R., and for testing theory, there
is [Hennessy1988]Hennessy, M.. In ACP voidACPACP : algebra of communicating processes style, the standard
reference is [Baeten and Weijland1990]Baeten, J.C.M.Weijland, W.P..
The companion volume [Baeten1990]Baeten, J.C.M. discusses
applications of this theory. We also want to mention the proceedings
of a workshop on ACP voidACPACP : algebra of communicating processes style process algebra [Ponse et al.
1995]Ponse,
A.Verhoef, C.Vlijmen, S.F.M. van.
Index
Index
X Verhoef
Fri Jun 13 12:53:07 MET DST 1997
![[IMAGE ]](img20.gif){kind=link}
![[IMAGE ]](img21.gif){kind=link}
![[IMAGE ]](img22.gif){kind=link}
![[IMAGE ]](img13.gif){kind=link}
![[IMAGE ]](img23.gif){kind=link}
![[IMAGE ]](img24.gif){kind=link}
![[IMAGE ]](img25.gif){kind=link}
![[IMAGE ]](img26.gif){kind=link}
![[IMAGE ]](img27.gif){kind=link}
![[IMAGE ]](img28.gif){kind=link}
![[IMAGE ]](img29.gif){kind=link}
![[IMAGE ]](img30.gif){kind=link}
![[IMAGE ]](img31.gif){kind=link}
![[IMAGE ]](img32.gif){kind=link}
![[IMAGE ]](img33.gif){kind=link}
![[IMAGE ]](img34.gif){kind=link}
![[IMAGE ]](img35.gif){kind=link}
![[IMAGE ]](img36.gif){kind=link}
![[IMAGE ]](img37.gif){kind=link}
![[IMAGE ]](img38.gif){kind=link}
![[IMAGE ]](img39.gif){kind=link}
![[IMAGE ]](img44.gif){kind=link}
![[IMAGE ]](img41.gif){kind=link}
![[IMAGE ]](img42.gif){kind=link}
![[IMAGE ]](img43.gif){kind=link}
![[IMAGE ]](img45.gif){kind=link}
![[IMAGE ]](img46.gif){kind=link}
![[IMAGE ]](img47.gif){kind=link}
![[IMAGE ]](img48.gif){kind=link}
![[IMAGE ]](img49.gif){kind=link}
![[IMAGE ]](img50.gif){kind=link}
![[IMAGE ]](img51.gif){kind=link}
![[IMAGE ]](img52.gif){kind=link}
![[IMAGE ]](img53.gif){kind=link}
![[IMAGE ]](img54.gif){kind=link}
![[IMAGE ]](img55.gif){kind=link}
![[IMAGE ]](img56.gif){kind=link}
![[IMAGE ]](img57.gif){kind=link}
![[IMAGE ]](img58.gif){kind=link}
![[IMAGE ]](img59.gif){kind=link}
![[IMAGE ]](img60.gif){kind=link}
![[IMAGE ]](img61.gif){kind=link}
![[IMAGE ]](img62.gif){kind=link}
![[IMAGE ]](img63.gif){kind=link}
![[IMAGE ]](img64.gif){kind=link}
![[IMAGE ]](img65.gif){kind=link}
![[IMAGE ]](img66.gif){kind=link}
![[IMAGE ]](img67.gif){kind=link}
![[IMAGE ]](img68.gif){kind=link}
![[IMAGE ]](img69.gif){kind=link}
![[IMAGE ]](img70.gif){kind=link}
![[IMAGE ]](img71.gif){kind=link}
![[IMAGE ]](img72.gif){kind=link}
![[IMAGE ]](img73.gif){kind=link}
![[IMAGE ]](img74.gif){kind=link}
![[IMAGE ]](img75.gif){kind=link}
![[IMAGE ]](img76.gif){kind=link}
![[IMAGE ]](img77.gif){kind=link}
![[IMAGE ]](img78.gif){kind=link}
![[IMAGE ]](img79.gif){kind=link}
![[IMAGE ]](img81.gif){kind=link}
![[IMAGE ]](img80.gif){kind=link}
![[IMAGE ]](img82.gif){kind=link}
![[IMAGE ]](img83.gif){kind=link}
![[IMAGE ]](img84.gif){kind=link}
![[IMAGE ]](img85.gif){kind=link}
![[IMAGE ]](img86.gif){kind=link}
![[IMAGE ]](img87.gif){kind=link}
![[IMAGE ]](img88.gif){kind=link}
![[IMAGE ]](img89.gif){kind=link}
![[IMAGE ]](img90.gif){kind=link}
![[IMAGE ]](img91.gif){kind=link}
![[IMAGE ]](img92.gif){kind=link}
![[IMAGE ]](img93.gif){kind=link}
![[IMAGE ]](img94.gif){kind=link}
![[IMAGE ]](img95.gif){kind=link}
![[IMAGE ]](img96.gif){kind=link}
![[IMAGE ]](img97.gif){kind=link}
![[IMAGE ]](img98.gif){kind=link}
![[IMAGE ]](img99.gif){kind=link}
![[IMAGE ]](img100.gif){kind=link}
![[IMAGE ]](img101.gif){kind=link}
![[IMAGE ]](img102.gif){kind=link}
![[IMAGE ]](img103.gif){kind=link}
![[IMAGE ]](img104.gif){kind=link}
![[IMAGE ]](img105.gif){kind=link}
![[IMAGE ]](img106.gif){kind=link}
![[IMAGE ]](img107.gif){kind=link}
![[IMAGE ]](img108.gif){kind=link}
![[IMAGE ]](img109.gif){kind=link}
![[IMAGE ]](img110.gif){kind=link}
![[IMAGE ]](img111.gif){kind=link}
![[IMAGE ]](img112.gif){kind=link}
![[IMAGE ]](img113.gif){kind=link}
![[IMAGE ]](img114.gif){kind=link}
![[IMAGE ]](img115.gif){kind=link}
![[IMAGE ]](img116.gif){kind=link}
![[IMAGE ]](img117.gif){kind=link}
![[IMAGE ]](img118.gif){kind=link}
![[IMAGE ]](img119.gif){kind=link}
![[IMAGE ]](img120.gif){kind=link}
![[IMAGE ]](img121.gif){kind=link}
![[IMAGE ]](img122.gif){kind=link}
![[IMAGE ]](img123.gif){kind=link}
![[IMAGE ]](img124.gif){kind=link}
![[IMAGE ]](img125.gif){kind=link}
![[IMAGE ]](img126.gif){kind=link}
![[IMAGE ]](img2.gif){kind=link}
![[IMAGE ]](img127.gif){kind=link}
![[IMAGE ]](img128.gif){kind=link}
![[IMAGE ]](img129.gif){kind=link}
![[IMAGE ]](img130.gif){kind=link}
![[IMAGE ]](img131.gif){kind=link}
![[IMAGE ]](img132.gif){kind=link}
![[IMAGE ]](img133.gif){kind=link}
![[IMAGE ]](img134.gif){kind=link}
![[IMAGE ]](img135.gif){kind=link}
![[IMAGE ]](img136.gif){kind=link}
![[IMAGE ]](img137.gif){kind=link}
![[IMAGE ]](img138.gif){kind=link}
![[IMAGE ]](img139.gif){kind=link}
![[IMAGE ]](img140.gif){kind=link}
![[IMAGE ]](img141.gif){kind=link}
![[IMAGE ]](img142.gif){kind=link}
![[IMAGE ]](img143.gif){kind=link}
![[IMAGE ]](img144.gif){kind=link}
![[IMAGE ]](img145.gif){kind=link}
![[IMAGE ]](img146.gif){kind=link}
![[IMAGE ]](img147.gif){kind=link}
![[IMAGE ]](img148.gif){kind=link}
![[IMAGE ]](img149.gif){kind=link}
![[IMAGE ]](img150.gif){kind=link}
![[IMAGE ]](img151.gif){kind=link}
![[IMAGE ]](img152.gif){kind=link}
![[IMAGE ]](img153.gif){kind=link}
![[IMAGE ]](img154.gif){kind=link}
![[IMAGE ]](img155.gif){kind=link}
![[IMAGE ]](img156.gif){kind=link}
![[IMAGE ]](img157.gif){kind=link}
![[IMAGE ]](img158.gif){kind=link}
![[IMAGE ]](img159.gif){kind=link}
![[IMAGE ]](img160.gif){kind=link}
![[IMAGE ]](img161.gif){kind=link}
![[IMAGE ]](img162.gif){kind=link}
![[IMAGE ]](img163.gif){kind=link}
![[IMAGE ]](img164.gif){kind=link}
![[IMAGE ]](img165.gif){kind=link}
![[IMAGE ]](img166.gif){kind=link}
![[IMAGE ]](img167.gif){kind=link}
![[IMAGE ]](img168.gif){kind=link}
![[IMAGE ]](img169.gif){kind=link}
![[IMAGE ]](img170.gif){kind=link}
![[IMAGE ]](img171.gif){kind=link}
![[IMAGE ]](img172.gif){kind=link}
![[IMAGE ]](img173.gif){kind=link}
![[IMAGE ]](img174.gif){kind=link}
![[IMAGE ]](img175.gif){kind=link}
![[IMAGE ]](img176.gif){kind=link}
![[IMAGE ]](img177.gif){kind=link}
![[IMAGE ]](img178.gif){kind=link}
![[IMAGE ]](img179.gif){kind=link}
![[IMAGE ]](img613.gif){kind=link}
![[IMAGE ]](img8.gif){kind=link}
![[IMAGE ]](img19.gif){kind=link}