BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1373
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Structural Operational Semantics for Weak Bisimulations
AUTHOR:: Bloom, Bard 
DATE:: August 1993
PAGES:: 50
ABSTRACT::
In this study, we present rule formats for four main notions of bisimulation 
with silent moves. Weak bisimulation is a congruence for any process algebra 
defined by WB cool rules; we have similar results for rooted weak 
bisimulation (Milner's ``observational equivalence''), branching bisimulation, 
and rooted branching bisimulation. The theorems stating that, say, 
observational equivalence is an appropriate notion of equality for CCS are 
corollaries of the results of this paper. We also give sufficient conditions 
under which equational axiom systems can be generated from operational rules. 
Indeed, many equational axiom systems appearing in the literature are 
instances of this general theory.
END:: CORNELLCS//TR93-1373
BODY::
Structural Operational Semantics for
Weak Bisimulations
Bard Bloom*
TR 93-1373
August 1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
* bard?cs.cornell.edu Supported by NSF grant (CCR-9003441).
Structural Operational Semantics for Weak
Bisimulations
Bc?d Bloom*
Cornell Vniversity
Aug?st 10,1993
Abstract
In this study, we present rule formats for four main notions of hi simulation with
silent moves. Weak bisimulation is a congruence for any process algebra defined by
WB cool rul?s; we have similar results for rooted weak bisiinulation (?lilner's `?ob-
servational equivalence"), branching bisimulation, and rooted branching bisimulation.
The theorems stating that, say, observationat equivalence is an appropriate notion of
equabty for CCS are corollaries of the results of this paper. We also give sufficient
conditions under which equational aMom systems can be generated from operational
rules. Indeed, many equationJ axiom systems appearing iii the h.terature are instances
of this general theory.
1 Introduction
Process algebras serve the same role in concurrenQy that the A-calculus does in sequential
block-structured tanguages, isolating the essential fratures of the area while abstracting away
inessential details. As there are a vast variety of frindamentally different concurrent settings
(varying process synchrony, communication mechanism, failure, and so forth), there is a
need for many process algebras. Developing the nght basic theory for the first few process
algebras was a labor of several years. This paper is part of a continuing investigation in the
metatheory of process algebra, with the goal of developing a hody of mathematics to make
the development and use of process algebras simpler.
The multiplicity of compntational models is reflected in several ways in process algebras.
Most obviously, the operations in the algebra must matcli the operations in the modA:
describing broadcasting systems requires broadcasting operations in the algebra. Somewhat
more subtly, the basic notion of p??cess equivoi?ncc --H that is, the definition of what it
means for two processes p and q to mean the same thing will also vary with the model of
concurrency. Notions of equivalence which work perft?ctly for point-to-point communication
(e.g., failures equivalence [BllR?4]) are not correct for broadcasting.
bard?cs?corneII.edu. Supported by NSF grant (CCR?9oo3441).
pi
WY
o			0
6			b
o			0
c			(1
o			0
a
0
WY
o			0
c			d
o			0
Figure 1: Linear vs. Branching Time
A wide range of process equivalences have been proposed and used [vG93]; in process
algebra, they range from strong bisimuThtion (the finest reasonable notion in this setting) to
weak partial trace equivalence (the coarsest notion, and not often applicable).
There are many ways to characterize equivalences, two of which are relevant to our
discussion. In many process algebras, there is a silent move r, an action which represents
internal computation. Some e?nvalences, called strong equivalences, treating ? as just
another action, without special status. Other equivalences, the weak equivalences, do their
best to ignore r actions that are computationally irrelevant. For example, let TT be a process
which does two T actions and then stops. Then TT and r are distinguished by most strong
equivalences, but identified by most weak ones. Some T actions cannot be ignored; the
process a +6 is able to accept either an a or a b signal, but the process Ta + Tb autonomously
chooses which it will accept, and will reject the other.
Another important charadenzation of process equivalences is linear and branching time
[G1a90]. Loosely, linear-time equivalences observe the behavior of a process as it runs along a
single execution, with very limited ability to observe possible alternate paths of computation.
Branching-time equivalences consider the whole tree of possible executions. For example,
the processes P1 and P2 of Figure 1 are hnear-time equivalent in all standard linear-time
equivalences; for example, they have the same traces, abc and abd. They are distinguished
by most branching-time equivalences; P1 makes an important decision on its first step, while
P2 delays it until its second.
Most process algebras use the notion of a transition. The relation p q says that
the process p can perform the atomic action a and thereafter behave like the process q.
Most process algebras are given by a Structural Operational Semantics (SOS), defining the
transition relation by induction on the structure of the term p.
Given the multiplidty of models of concurrency, notions of equivalence, and process
algebras, it seems worthwhile to study the metaTheory of process algebra: theorems which
apply to large families of languages, rather than merely specific ones. Such theories will
greatly facilitate the development of new process algebras. For example, [131M90, GV92,
Gro90J show that any language defined by suitable forms of structured operational rules enjoy
2
certain desirable properties: in particular, all such languages respect strong bisimulation. In
[ABV92a], we extend this theory: any language described by the USOS rules of [BIM9)]
can in fact be given an equational axiom system with a single infinitary induction principle,
which is complete for proving equalities between programs.
Nilost of these studies have treated strong equivalences. There have only been a few studies
concerning methatheory of SOSses for weak equivalences. Most of these studies have been
aimed at calculating the finest appropriate weak process equivalence. [131o90] introduced
several technical tools used in later studies, but its notion of equivalence had some ability
to count T moves and was therefore judged inappropriate as a weak process equivalence.
[Uli92J was considerably more appealing as a stuQy of equivaleuces, describing the class of
1505 rules, and precisely characterizing the notion of process equivalence they generate.
Ulidowski's notion is appealing in many ways, but misses certain important uses of process
algebras: e.g., processes with polling loops can diverge, and Ulidowski's theory doesn't place
many requirements on divergent processes.
In this study, we give SOS rule formats for important weak variants of hisimulation, weak
bisimulation, and branching bisimulation, and their (more useful) rooted versions. ?Veak
bisirnulation [Mit8l] is perhaps the niost obvious variant of bisimulation designed to ignore T
moves; its theory is not quite as clean as that of strong bisinmilation. Branching bisimulation
[vG"tITs9i is a finer notion, with better algebraic properties. Neither notion is quite right for
process algebra: they are not congruences with respect to certain operations, mainly nonde-
terministic choice +. Both can be slightly modified, to rooted weak bisimulation (Mihier's
observational equivalence [MilS9a]) and rooted bran4'ing bisimuThtion, capable of handling
+ and maintaining their other properties. ??e discuss the implications of these rule formats
on equational axiom systems.
1.1 Strong and Weak Bisimulation
Strong bisimulation [ParSi, Mil83, NIilS4] is the finest generally-accepted notion of process
equivalence in this setting. Informally, two processes are strongly bisimilar iff they make the
same decisions at the same times. 1?ormalky,
Definition 1.1 A binary relation between processes `s a strong hi simulation relation iff
whenever p p', then
o+ If p q for some action a and p ocess q, Then PI a q' for some Process q1 such
that q
o+			Vice versa; that is, if pI			a			q1 for some action a and Process q', then p			a			q for
some process q such that q			q
Processes p and PI are strongly bisimilar p ? p1, iff there is some strong bisimuThtion
relation such that p
Strong hisimulation enjoys a rich and powerfiil theory. There are complete equational
axiom systems (some requiring induction principles) for a wide variety of theories. [BNv9o,
:3
Mil89b, ABV92a]. There is an elegant equivalent logical characterization via Hennessy-
Ahiner Logic [11M85]. Definition 1.1 gives a useful method for showing two real programs
equivalent [CPS89, ?VBB92]: one guesses a relation relating the programs, and verifies
that it is indeed a strong bisimulation relation. Checking this is local, involving only one step
of computation. Despite some theoretical concerns (e.g., strong bisimulation is loo strong,
capable of distinguishing processes which ought to be identified [AhrS7, BIMSS, 13Ni9()]),
strong bisimulation is a central part of concurrency theory.
1.1.1 Weak Bisimulation
Most process algebras, including CCS and ACP, have a sdent or hidden action, T. This action
marks internal computation: for example, processes will take T steps as they compute; and
when processes communicate on a hidden channel, all that is visible outside is a T action.
The informal intent is that 7's are (mostly) irrelevant, and that processes which differ only
in the number and positioning of ?`s are equivalent. ;Ns stated before, we would like to have
T and T? identified.
Strong bisimulation, and strong equiv?ences in general, do not meet this informal intent.
T`5 are as visible as any other action, and ? +6+ 77 Accordingly, several researchers have
defined weak versions of bisimulation, which pay less attention to 7'5 but still have the
essential flavor of bisimulation. The first such relation, called simply weak bisimulation, is
based on the weak transition relation , defined by:
Definition 1.2 We define multi-step transition relations p			q by p			p, and f
p			q and q			a r then p			r. 1Y?is is extended to sets of string S in existentially:
p			q iff?s e S.p			q. Let r			f?,7,77,. .
Finally, we define ? foro C ACtT to be TaT if & c ACt, and ? Jo = 7.
Weak bisimulation is defined like strong bisin?ulation, using the relation for o ?
AdT instead of a for a E Act.
Definition 1.3 A relation between processes `s a weak bisimulation relation iff, whenever
p p' and p q for some 0 E ACtT and process q then There is a q1 such Urat p' ?
and q q', and vice versa.
Processes p and p' are weakly bisimilar, p ? p', 4. there is a weak bisimuThtion relation
with p
For example, a ? Ta. Note that a +6+ 7a, as the one can take an a-step and the other
cannot. Strong bisimulation is mathematicaily quite nice, but weak bisimulation is somewhat
less so. For example, strong bisimulation is a congruence with respect to all CCS (and a vast
range of other) operations. Weak bisimulation is a congruence with for most CCS operations,
but not for +. For example, a ? 7a, but a t b ? ra t b; the latter process can take a
7 step to the process b, which the former cannot match. The standard approach to fixing
this is to take weak bisimulation congruence, also known as rooted weak bisimulation, rooted
r-bisimulation [B'v90J, and rather anomalously as observational equivalence [NIilS4, -YIi189a].
This relation is defined as follows:
4
Definition 1.4 Processes p and PI are rooted weakly bisimilar, P ?r P1' iff whenever
p			q for some ? AdT, then p' `*??*			? q, and vice versa.
This is a direct definition of ?r ?? terms of ?; arid it differs from ? only when ?
the rooted relation insists that PI take at least one r-step. Rooted weak bisimulation works
correctly: all CCS, and indeed most other process algebra operations respect it.
1.1.2 Branching Bisirnulation
Detailed philosophical justification for branching bisimulation rnay he found in [vG?Ts9,
vG93]. Briefly, branching bisimulation is the finest weak analog of bisimulation in the testing
scenarios of [vG93], and the finest notion which admits an expansion theorem. Furthermore,
the informal description of bisimulation, ?two processes making the same decisions at the
same time," is imperfectly captured by the formal definition. Consider the weakly bisimilar
processes Pi = n(rx + y) and P2 = a(rx + g) t ax. The process P2 can, on an a-transition,
choose to forgo the chance of performing g. The process Pi cannot make the same choice
in just the a-move; discarding the y re(juires an a-move followed by a T. This conceptual
imperfection is fixed by branching bisimulation; Pi and P2 are riot branching bisimilar.
Definition 1.5 is a branching bisimuThtion reThtion if, for all actions ? C Act? and for
allp?p1 then
1.			if p			r, then either:
(a)			P = r and r			p', or
__ I			_
(b)			there are q', r' such that p' ?			q			r', p			q1, and r			r
T
p			r
P
(a)
or
a
r
T			a			r1
(6)
2. Vice versa.
As usual, p and p' are branching bisimilar, P <???b P', if ther? is a branching bisimulation
relation relating them.
Branching bisimulation suffers from the same congriience problem as weak bisimulation:
a Hb Ta, but a + b ?b ra + 6. The solution is a bit finer than for weak bisimulation.
Rooted branching bisimulation does one step of strong hi simulati on, then turns into branch-
ing bisimulation.
Definition 1.6 Two processes p anda are rooted branchiughisimilar if wWeneverp a
then p1 ? q' and q H.b q'; and vice versa.
5
The theory of Hrb is quite nice: for example, rooted branching bisimulation is a congruence
with respect to CCS, has a complete axiom system on finite processes, and SC) forth.
?1e refer to the relations of weak and branching bisimulation, rooted and otherwise,
collectively as "silent bisimulations."
6
r
a x'It!j
1.2 Structured Operational Semantics and Process Equivalences
Alost process calculi are given behavior by struct?red operational se?antics (SOS), rules
which define the behavior of composite processes in terms of the behavior of their com-
ponents. A well-designed SOS rule system has many of the advantages of denotational
semantics; e.g, structural induction is a viable proof technique, as we will see repeatedly
in this study. Furthermore, SOS rules are generalky fairly easy to read. For example, the
interleaving parallel operation p q is easily described by SOS rules: for each action a, there
are rules:
XiYi			Y2			(1)
xi			I x2			Y? I x2			Xi II r2			I Y2
The purpose of this study, like many others in this line of research, is to determine the
relation between the SOS definition of a process algebra, and the equational theory. NVe will
give some quite general rule formats which guarantee that process algebras respect the four
silent bisimulations described in Section 1.1, and a new variant which may be of some use.
The SOS definition of a process algebra or programming language describes the intended
behavior of processes. It is not intended to suggest the preferred implementation of the
language, any more than the P-rule is intended suggest the preferred implementation of
functional languages. It is often useful to specify languages using rules which appear rather
unreasonable, knowing that the implementation need not reflect the rules.
Two common categories of `unreasonable" or "unimplementable" features of rules are
copying of processes and negative tests. Both features arise quite naturally in the simplest
specifications of standard operations. Our rule formats for weak process equivalences allow
copying in a fairly general way. However, negative tests defy both implementation and weak
bisimulations, and are thus excluded from our rule forniat.
1.2.1 Copying
For example, one of the rules of the specification of a while loop is:
true
Xi			Yi
whiler1dox2 -*? (r2;whiIeyido2)
That is, if the test Xi signals "true," the loop body is executed once and the loop is re-
executed. This specification makes a copy of the loop body 2. A typical implementation
[P1o81, WBB92] does not copy 2; it simply uses a loop around the code.
A similar operation is Milner's !p, which effectively turns p into a reentrant server:
This spawns a new server x' to handle each request a. This will probably be implemented by
spawning new processes on each machine running r --H- which may, in general, be a distributed
system [BC9o, BCG9l].
Many other operations can be specified by copying rules. For example, a process impl&
menting a distributed service might produce a signal [if its load gets too high, piggybacked
on top of its normal service message. The system's response might be to bring up another
processor running the original server code, running in parallel with the original process. Such
a service could conveniently be specified by rules including:
a			a
Yi			11yll,x?Y12
a			a
server(x1,x2)			server(y1,x2)			server(x?,x2)			server(y11 r2,w2)
where a ranges over server actions, the ri argument represents the current state of the server,
and the r2 argument represents the initial state of a new server processor.
1.2.2 Negative Rules vs. Weak Bisimulation
For strong notions of process equivalence, many operations are best described using ne9ative
rules; viz., those with antecedents of the form x whiji are satisfied if r cannol perform
an a action. Consider the following ?full sequencing" operation p; q, which runs p until it
stops, then runs
a			_____			T			b
Yi			a			`Y2 V6.
a			`I			2
1 ?			Yi			a
Y2
It is impossible to define this operation without negative rules. though most process
algebras define approximations which are adequate for programming, and much easier to
implement. There are several other reasonable operations which can only be defined with
negative rules; e.g., polling operations wtiich branch on whether or not a process is ready to
communicate.
Unfortunately, negative rules seem incompatible with weak process equivalences. One
of the fundamental laws of silent bisimulations is KEAR, Koomen `s Pir???r Abstraclion Rule
[B?V90]. Intuitively, this rule 5Qy5 that that nondeterministic choice can be implemented by
a polling loop. Indeed, delay-insensitive implementations of process algebra based languages
[WBB92] implement selective communication (the main practical application of nondeter-
ministic choice in this setting) via polling loop5. As these implementations are correct up to
weak or branching bisimulation and (probably) not mudi stronger, KEAR is practically and
philosophically important.
However, KFAR seems incompatible with negative rules. A basic consequence of KEAR
is that, if we have two processes Pi and P2 such that Pi P2 then Pi and P2 ought to be
considered the same process. That is, the decision of whether or riot Pi M*> should involve
all such P2. As P2IPi P2 can be unmanageable in?nite and not even recursive ---H
testing Pi'5 ability to do an a is necessarily challenging.
7
We are not aware of any way to interpret negative tests x Th+ in a way that respects
silent hisimulations and has any chance of being implementable. Consider the weakly bisim-
ilar processes of Figure 2.
Pi
a
0
7,			7,
P2			P3			0			P4			0
7,			7,
a
o			0			0
a			a
o			0
Figure 2: Weakly Bisimilar Process
These processes must be indistinguishable in any language respecting weak hisimulation,
as they are weakly bisimilar. The most obvious interpretation of x --H? is simply to test
that x has no a transition. With this interpretation, m(Pi Th+ ) but P2 A> a rule which
can test for x			` could distinguish these equivalent processes.
A variant interpretation which has been proposed several times [Vaa9l, Uh92] is that
negative rules only be interpreted in st(?bTh states; that is, x satisfies the test 			-#+ iff
x can perform r-moves to reach a state which has neither a nor 7, transitions.			This is
implementable (by running the process until such time as it readies a stable state), and does
address the primary difficulty with KFAR; the set of processes ? to a stable process p is
just fPY For example, p? , as P4 a which is stable and cannot perform a b. This
interpretation does work for Ulidowski's weak equivalence, but it fails for weak bisimulation.
For example, Pi in this interpretation, but ?(p? ? as p? is not in a stable state,
and indeed cannot reach one by performing 7, moves.
As there seems to be no good interpretation of negative tests, we do not include them
in our languages for weak or branching hisimulation. The languages for rooted branching
bisimulation can tolerate them to a hmited degree.
1.3 Results
In this paper, we give rule formats for the four silent bisimulations of Section 1.1, as well as
a variant of rooted weak bisimulation. The basic intuition behind the classes is fairly similar
basically, we require operations to wait calmly for their operands to be ready. We call this
property coolness: we thus have WB cool languages, which respect NN'?ak Bisimulation; RBB
cool languages respecting Rooted Branching Bisimulation, and so forth. Weak bisiniulation
is discussed in Section 3, rooted weak bisimulation and a technically convenient variant called
"strongly rooted weak bisimulation" in Section 4, branching bisimulation in Section 5, and
rooted branching bisimulation in Section 6. It is worth noting that the methods used fc?r
branching bisimulation are very similar to those for weak bisimulation, though the proofs
have twice as many cases.
In Section 7, we discuss the implication of these rule formats for equational theories.
It is well-known that neither weak nor branching bisimulation has appealing (e.g., finite)
axiom systems for some basic operations like parallel composition. However, the rooted
versions generally admit equational axiom systerns. The niethod of [A13V92a] for gerierating
equational axiom systems applies to all SR\VH cool arid RBB cool languages (and preserves
their SR?VI3 cool or RHB cool character.) NVe give decidable sufficient conditions under which
R??I3 cool languages have [ABV92a]-style aMom systems. The equational axiom systems the
[ABV92a] method generates are not complete for any decent programming language.
1.3.1 Useful Corollaries: simply cool languages
In the rest of the paper, our results are quite general, and accordingly hard to apply. ?Ve
expect that the following straightforward coroliaries of our main theorems will prove useful
in most cases appearing in practice; thQy are enough to cover most CC 5-like process calculi
known to date.
Definition 1.7 A language  defined by SOS rules is simply RT3 cool if
1. All rules p for all operation symbols f of have the form:
? \yxi??y?IicJ(p)
f(:ri:rn) ? t
where I(p) is a set of numbers telling which argumenKs' off take actions under rule p.
2. For all rules p, and all i c J(p),  contains a patience rule:
Xj
T f(x1			Ti?1.,?i,r?+1xn)
3. No rules have hypotheses mentioning T `5, except the patience rules required by clause
2.
The definition for weak bisimulation differs only slight?v:
Definition 1.8 A language is simply \?\rJ3 cool iff it is simply iQB cool,. and furthermore for
every t in clause 1, Xj does not appear in t when i c J(p).
CCS without t is a simply ?V13 cool (and, a fortiori, simply RH cool) language.
Rule formats for rooted silent bisimulations are built by partitioning the rules into two
classes: tame operations, which respect the silent bisimulation from tbe previous definitions,
and wild operations, which exploit the rootedness condition for one step arid then evolve
into tame operations.
9
Definition 1.9 A GWOS language  is simply R\\713 cool $ the operations in  can be
partitioned into tame and wild operations,, such That:
1. The targets of all rules (the t `s above) only mention tame operations.
2. The sublanguage consisting only of tame opern'tions is I'VB cool.
3. Every rule fi for a wild operation has the form
\yxi a? c
f(.rD'			I
4. For each such ruTh, there are rules (possibly derived rules):
Xjy?			y? i C
f(rD T t[:r?:=yJ I ?
I A t[xj :=
`For example, CCS is a simply R?Vt3 cool language. + is a wild operation; all others are
tame. Pick one of the rules for +, say
xl			yi
xl + x2
If we choose I = x1, then we must have the 1ol1owing rules and derived rules:
xlyi			1y1			x1y1
xi + x2			y1			y1			ri			y1
Indeed, these are all valid CCS rules or derived rules and hence + is a suitable wild operation.
Rooted branching bisimulation is mud' easier, largely due to the stronger first-step con-
dition.
Definition 1.10 A c;sos language  is simply RBB cool itf ihe operation symbols can be
partitioned into tame and wild operations, such that
1. The sublanguage of consisting of only tame operations ?s s'mply 1?B cool, and
2. Let f(x? ? t be the concThsion of any rule of . Then t mentions only tame
operations.
As one would hope, we have the 1o1lowing corollary to ruost of the main theorems of this
paper.
Corollary 1.11
1. If is simply 14B coo(, then weak bisimulation is a congruence for .
10
2. ff is simply RIYB cool, then rooted weak bisimuThtion is a congruence for .
3. If is simply lIB cool, then branching bisimulation is a congruence for .
?. If is simply J?BB cool, then rooted branching bisimuThtion is a congruence for .
We also have
Corollary 1.12 If is a simplyllBB cooilangu?qe, then the methods of f4BV92atgenerate
a simply RBB cool, conservative extension of ? and a set of equations which are sound for
rooted branching bisimulation and complete for strong bKsimuThtion.
A similar fact generally holds for simply RWB cool languages, but it is harder to state in
full generality.
2 Preliminaries
In this section, we review some standard and mostly-standard definitions in process algebra.
2.1 Notation
We use fairly standard mathematical notation. though we write A rh B fc?r A n 1? = ?. If
A u B = C and A rh B, then A and iJ partition the set C'; unlike some authors, we allow A
and B to be empty.
We often introduce eccentric notations for tuples; e.g., we write write the tuple (I, a,
as t a ??, when we are interpreting it as a formula.1
We use vector notation, x? to denote a finite sequence of items named Xi, X2,..., X? for
some n. We assume that the sequences are of the correct lengths, which are always clear from
context or irrelevant. Operations and relations on vectors are to be interpreted pointwise.
For example, the equation x = y means that x and y have the same length, and that Xj =
for each i. To add to the confusion, it is occasionally treated as the set fiti, x2, . , xnt.
We denote the empty string by. If r is a symbol, T+ = fr, TT, TTT,.. .? and it = frtur+.
Similarly, if s is a set of actions or string, then 8 is the Nleene closure of 5, the set of all
finite strings of elements of 8.
2.2 Structural Operational Semantics
As we are investigating the comparative anatomy of process algebras and their definitions,
we discuss their definitions in some generality. We are concerned with ()WOS and related
classes of rules; to discuss these, we need some notation.
A process algebra language, or simply "language," includes a finite set of actions, and
a finite algebraic signature. In this study, we assume that the set of actions Actt contains
a distinguished element it, the silent action; the remaining actions Act are not required to
i?Vhen necessary, we add an extra component to the tuple; if we are using the notation t ? as
well, we assume that the representations are disjoint. This fine point is never relevant.
it
have ally significance. The definitions of signature, term, arid so forth are fairly standard. A
signature Z is a finite function from a set of openition symbols f, g, ..... to natural numbers,
their arities. Terms I are inductively built from an infinite set of variables x., y, ..... by
application of function symbols:
I ::= x f(tiIn) where V(f) n
A term is closed if it contains no van able symbols; process algebras generally contain nullary
operators, such as the stopped process 0, and thus have closed terms. This is important, as
closed terms are processes which can be executed. There are no binding operators, and in
particular no rec ? P] operator for recursive process definition a Ia CCS. Our definitionat
schema are powerful enough to include general noritermining computations, even without
recursion; and any program written with rec ? Pj over any of our calculi can be written
without rec ? ] in a suitable variant calculus.
Let Procs() be the set of closed terms of the language , and Terms() the set of all
terms. ?Vhen  is clear from context, we simply write Procs and Terms. A term is un?variate
if no variable appears in it more than once.
Actions a are elements of some finite nonempty set Act. Transition formulas describe
possible transitions. A positive transition formula is a triple, written I I', where I and
I' are terms, and a is an action symbol. A negative transition formuTh is a pair I A+ . A
formula is primitive if I and I' are variables: x a r? and j. "
A GSOS rule is a pair ??, f(i) t?, where ? is a set of primitive transition formulas,
subject to certain conditions. GSOS rules are usually written:
uifxi a? mijil ?j <n??uui\yri m4i i
f(x1.			I
The conditions are: the variables i, y are all distinct, and the variables in I are at most x,y.
In this study, we take the point of view that rules bind all variables appearing in them. In
particular, rules which differ only by a bijective renaming of variable names are equivalent.
We use the following terminology to describe parts of a CS()S rule:
o+ ante(p) ? is the set of antecedents.
o+ cons(p) = f(i.) A* I is the consequent.
o+ source(p) = f(?) is the source.
o+ target(p) = I is the tarqet.
o+ c is the action.
o+ The variables Xj are the source vaj?iables SourceVars(p).
o+ The variables Yij are the target variables Targetvars(p)
12
Symbol
a, b, c, d
a,
p, q, r, 5
1, u, v
x, y, z
Usage
Actions other than r; elements of Act
Actions or T; elenients of Act?.
Actions, T, or ?; element of Act?,
Processes
Process terms
Variables
Figure 3: Conventions
For example, the interleaving parallel operation p II q is defined by the 2 Act I rules of (1).
Niany process algebras have the operations of action prefixing and. nondeterministic choice.
For each action a, ap is a process which performs an a and thereafter behaves like p; for all
p and q, p + q may behave like either p or q. These have the rules (for each a):
________________			x1a			x2Y2			(3)
ax			x			xl + x2			y?			x1 + x2			Y2
If 1? is a rule format (that is, a set of rules), an 9? language is a finite signature ? of
operations together with a finite set of rules 1? C 9?. where all operations in R are in ? and
used with the correct arity.
Null transitions, x y, will provide great notational convenience later on: they are
intended to mean that x and y are bound to the same term. This can be trivially expressed
in the GSOS format by using x everywhere y appears: the following are equivalent.
______________			x			y
ax			ax			y
`A?e set Act?? = Act u fT,?t, use ? to range over Act??, and with a slight pun we use the
notation x y for ? ? Adm to range over x a ? and x
Definition 2.1 A rule or language which is CSOS ecept for possibly having null transitions
as antecedents is said to be in GS()S(r.) format.
Notation 2.1 In this study we work with a variety of objects including variables: terms,
transition formulas, rules, and so forth. Fo'?any such object Q, Vars(?) is the set of variables
in ?. If x Ei Vars(?) and ? is a suitable object, then ?[x := ?j is ? with ? substituted for x.
Only rules bind variables, and that at the top level only; so the definition is not subtle.
It is often convenient to work with substitulions (traditionally also called instantiations
when they refer to rules), which are partial functions a from variable names to Procs. ?Q
extend a to terms I with Vars(t) C dom(a) by:
a(f(t1t? )) = f(a(t1 ), . . . , a(tn)),
J3
and similarty to other constructs including variables.
If ? is a transition formula # C Procs x Act x Procs, and a is a substutition, and
Vars(?) C dom(a), then we may define the relation a,) ?
a,) ?			a			__ a(t))a(u)
a,)			?			t A>			?			?qCProcs.a(t)%+q
a,)			?			I			?			a(i)=a(u)
We extend ? to sets of formulae:
a,???+ I=H ? Vi'cTh(a,) w)
The GSOS theory of [I3INlss, 131o89J shows for any CSOS language , there is a unique
appropriate transition relation ); that is, one satisfjying the following properties:
1. For any process term p f(Pip?) and action a, if p) q, then there exists a rule
p which enables the transition: that is, there is an instantiation a on Vars(p) such that:
(a) a(r?) = p? for each i
(b)			a ? ante(p)
(c)			a(cons(p)) =			a
2. For each rule p and instantiation a siich that a,)K--H ante(p), thena,)Kcons(p).
This relation is denoted			L, or simpky			when  is clear from context.
2.3 R,uloid Theorems
We will frequently need to examine the behavior of processes in arbitrary contexts. Our
main technical tools for doing so are Ruloid Theorems [131M90 J31o93], whidi characterize
all possible behaviors of all terms in a language, in a form that resembles the original rule
format.
Definition 2.2 Ruloids are like rules,, except that The conclusion has the form I a ? for
some term I, rather than the simplerfonn f(x? it as required for rules.
Rules carry proscriptive force; that is, they define the behavior of all terms of the language.
Ruloids simply carry descriptive force; that is, they explain how the rules cause complex
terms to compute.
Most well-designed rule formats enjoy a RuThid Theorem. That is, for each term I and
5 c Act.?*, it is possible to calculate a set 1Z(t, s) of ruloids which precisely capture the
circumstances under which I can perform 5; and each p E 1?(t, s) is still in the same format
as the original rules, mutatis mutandis. Formally,
Definition 2.3 A set ? of ruloids is just right for a term I and a string s of actions it',
14
1. The conclusion of each p C 9? has the form I I' for some I'.
2. 9? explains all the iransitions possible for instances of I. Formally, let a : Vars(t) H Procs,
and suppose a(t) ? q. Then there ? some ruloid p c 9?, and extension a' D a to
Vars(p) such that:
(a)			a' ? ante(p)
(6)			a'(cons(p)) a'(i)			?
3. Every ruloid in 9? is valid, That is, if a : Vars(p) H Procs and a = ante(p), then
a ? cons(p).
For example, the following set of ruloids for (x I y) t are just right for that term and the
action a:
a			a			a
x			x'			yy z
?? ? ? a, (x' y)			(x y) t z a (x 1 y')			(x I y) t			a, ??
2.4 ?Presentation
In this study (and many other ones), it is convenient to use rules and ruloids in -presentation.
Definition 2.4 A ruloid p in GSOS(?) format is -presented ?j:
1. There is at least one antecedent x y for each source variable x, for some ? E
Act,,? and
2. SourceVars(p) ? TargetVars(p)
For example, the first sequencing rule (2) is not ?-presented, as no antecedent mentions
x2. Nor is the rule
x1			Yi, x2			Y2
x1 x2			y? x2
Although an antecedent mentions each argument, t,he source and target variables are not
disjoint. However, the equally useful rule
x1			y?, x2			Y2
x1 x2			y?
is r-presented. The precise definition of "`equalky useful" is equipotent:
Definition 2.5 Two ruloids p and p' (Ire equipotent if whene?'er one of them enables a
transition p a, q, then the other does as well.
Lemma 2.6 Let  be any GSOS(r) language. Then there is a GSOS(r) languQqe ` with
the same sets of actions and operations (and hence the same set o,f terms), and a biiection
p ? p' between their ruloids such that p and p' are equipotent.
15
Proof: Let p be a ruloid of . Let V be the set of variables which either don't appear in
the antecedents of p, or appear in both source and target. For each x C V, pick a variable x'
distinct from Vars(p) and all other x"s. Suppose that cons(p) t ?- u. Let i" be u with
each x E V replaced by the corresponding x'. Let p' be the ruloid:
r
which allows its argument to take r-transitions freely. (It turns out that g(q) does nol need
a patience rule, but this is a theorem.)
Not all operations have, or require, patience rules. The canonical example of an operation
that shouldn't have them is prefixing, with nih:
(n?istake)			xTx1
ax			ax'
as (1) this would destroy many essential properties of prefixing, e.g., its ability to guard
recnrsions, and (2) it isn't necessary, as pre?xing already does respect weak bisimulation
That is, if p ? PI, then ap's only possible move is an a-transition to p; clearly ap' can do
an a-transition to PI, ?4?ich is weakly bisimilar to P by hypothesis. Niore generally, if j(p)'s
Iirst step of behavior doesn't involve p's behavior, then we don't. need patience rules.
ax			x
It would be a mistake to have a patience rule:
ante(p) U ?x x'Ix E
[Art'
Then clearly p and p' are equipotent, and PI is -presented. ?
3 Rules for Weak Bisimulation
The simplest kind of operations which respect weak bisimulation are the paticnt ones. Sup-
pose that P ? p', arid that f(p) ? g(q) via a rule
x			y
j(x) A
and a transition p A q. All that we know about p' is that p1 ? A r2 T
with q ? q'. This suggests that f(x) will have to wait for its argunient to perform an a
action. So, we need a patience rule:
16
So, we only require patience rules for active ar?yurnents of functions f; that is, those
arguments which f allows to run. For example, if we have an operator with the single rule:
Yi
f(x1,x2) ? g(y1,x2)
we would expect to have a patience rule for x1 but not for x2.
However, we know from first principles that operations defined by patience rules alone
are not as powerful as possible. flisimulation equivalences, of all sorts, are branching-time
equivalences. Thus, it ought to admit branching tests: testing for the ability to do both an
a and a b simultaneously. That is, it should tolerate copying, in the style of Section 1.2.1
For example, we'd like to have an operation given by a rule of the form:
a			6
x			y?,			x			Y2
k(x)			?			0
(4)
However, this is sornewhat complicated. \Ve can't (with weak bisimulation) expect to detect
s?muttaneoustransitions. Specifically, a+bis weakly bisimilar to Pab rec ? a + T(6 + Tx)],
which alternately offers a and 6:
T
a+ 6			Pab			Pba
4
A			xc			A
_			(5)
a
0			0			0			0
Pab cannot perform an a and a 6 simultaneously, and thus k( Pab) cannot fire by rule (4).
Our solution is to require the presence of enough rules and operations so that k(Pab) will
behave right. Specifically, we insist that there be a two-argument version k of k, with one
argument to handle the test of k and the other for the ? test. The operation k
has one computational rule, giving k* the ability to do (4):
Yi,X2Y2			(6)
k*(x1,x2)			0
The basic operation k and the derived version k* are connected by a pair of rules, allowing
k's argument to take a T move in preparation for doing its two possihie behaviors separately.
These will be called bifurcation nites:
ry			ry
k(x)			T			k*(x,y)			k(x)			T			k*(y,x)
Similarly, k* has patience rules allowing its arguments to proceed independently:
XiYi			X2Y2
k?(x1,x2)			T			k?(y1,r2)			k?(x1,x2)			T			k?(x1,y2)
?Vith these rules, we see that k(Pab) 0 as desired:
k(Pa6) T k?(Pa6,P6a) 0
(7)
(8)
17
3.1 WB cool Languages
In this section, we work entirely with ?-presented languages. ?Te define a subset of the b-
presented positive GSOS(?) languages, the 147B cool languages, in which weak bisimulation is
a congruence. For example, CCS without + is a NVB cool language. The definition proceeds
in two parts. We first give an infinitary version, the fijlly ?`B cool langiiages, whidi places
restrictions on all univariate terms. Then we give necessary and sufficient finitary conditions
on the rules which guarantee the infinitary version.
Definition 3.1 The source variable x is active in fi if there is an antecedent x y of p
(where by our conventions P C ACtT and hence 3 ? &). The variable x E Vars(t) is active if
it is active in any ruloid p for t.
For example, the variable x is active in k(x) and k*(x, x'), but not in ax. Next, we need to
count how many copies of a variable we will need:
Definition 3.2 Let x ? Vars(t) for a univariate term t. 14% define barb(i,x) to be the
max?mum number of antecedents x y in any eThment of p C u?1Z(t, i3)
For exaniple, barb(k(x),x) 2, as (4) has two antecedents for x. kecall that we use
&-presented rules and ruloids; among other things, this guarantees that each variable in a
rule appears in at least one antecedent. Thus, barb(ax, x) 1.
Definition 3.3 A rule p with source f(?D is straight ifp has exactly one antecedentfor each
argument Xj. iVon-straight rules are branching.
For example, (4) is not straight; (6), (7), and (8) are straight.
Definition 3.4 A univariate term t is straight if barb(xI) 1 for each x E Vars(1). I47e
define Termssi to be the set of straight univariate terms.
For example, k?(xi, x2) is straight, and k(x) is riot. Indeed, k??(x1, x2) is a straight version
of k(x), in a sense we will make precise. To describe the correspondence between k(x) and
k*(x1,x2), we several things.
First, we need a function (.)?, taking terms to their straightened versions: we will have
= k*(xi, x2). Recall that k arid k* are simply operation symbols; the right
hand side of this equation is just a term.
o+ We need to explain that xi and x2 in k?(x?, x2) both correspond to x in k(x); we thus
have a map xX,(?) = ?xX (.) : fxi, x2J H txl, with x?X ( xi) = Q,(x2) = x. The notation
wx,(x?) is intended to be reminiscent of fractions: we nse conventions so that generally
xx,(x?) --H
o+ We need bifurcation rules, like (7), whidi Mlow k(x) to copy its argument and run it
along some T-steps.
0
?Ve need a correspondence p p between the rules for k(x) and the rules for k*(x1, x2).
For example, (4)* = (6), and the two rules of (7) correspond to the two rules of (8).
Note that this is a bijection between the rules for k(x) and those for k*(r1, x2), and
that the rules corresponding to the bifurcating rules are patience rules.
These requirements are formalized in the following defInition.
Definition 3.5 A positive GSOS(?) language  is fully \V13 cool $ there is a mapping
: Terms1 H Term?, and, for each t c Terms1, a mapp?ng xX, (?) : Vars(t*) Vars(t). Let
1? ?(x) ?r' E vars(ft)I?xx,(xl) = x?. ?`?en 4 is clear from context (which is almost all the
time), we write these as simply X (T') and \%J(x). A?te that ?xX, (?) is a ubstitution, and we
may apply it to terms and the like.
1. If t is straight, then xX,(P) =
2. If x is active in 4, then for all r1E l?l(x), there is a ruThid bj$ E lZ(t,?):
u fx1			vx,11(xx,(rit) = ri) A (x,x) $ (x1,x'1??			(9)
4 A*
where Vxl'5 are distinct fresh variables, and a(x') = v?? for each x'. bixti is the bi-
furcation rutoid of 4 for r'; if 4 is straight, it is also called the patience ruloid for
ri.2
3. The only ruloids with T `5 in the antecedent are the bfura?tion ruloids.
4. For all t and a, there is a bijection (?) : JZ(t.,&) ` 1?(t?, a) such that:
ante(p) = ?xx,(ante(p*))			(10)
target(p) = target(p*)			(11)
Note that Definition 3.5 part 4 implies that the variables appearing in p and p? are closely
related. For any ruloid p, we have
?=			ffi)			K= ______
u
Note that TargetVars(p) = TargetVars(p?). As p is straight, fi?r each r' C SourceVars(p?)
there is exactly one antecedent r' ? y of p?. There is t1ins a bijection x;(.) from
TargetVars(p?) to Sourcevars(p*), where ?x;(y) = x' iff r' ? y C ante(p).3
2Recall that the source and target variables of a GSOS(c) ruloid must be disjoint Thus, we must introduce
new variables v?i, to avoid possible name clashes,
3Note that p is an implicit parameter of these functions.
19
Similarly, for each y, there is a unique a E SourceVars(p) with an antecedent a
let 7x(.) : Ta rgetvars(p) H SourceVars(p) be the flinction associating a's with y's. It is
not in general a bijection (though it is by definition a bijection for straight ruloids); let
: SourceVars(p) H ?(TargetVars(p)) be given by ?(a) ?yIyX(y)
Note also that if p is a bifurcation ruloid, then so is p arid vice versa.
3.2 Weak Bisimulation is a Congruence for fully WB cool Lan-
guages
In this section, we show that weak bisimulation is a congruence for fully ?VB cool languages.
In Section 3.2.1 we develop a more local equivalent definition of weak bisiniulation; which
we use in Section 3.2.2 to prove the main theorem.
3.2.1 Local Weak Bisimulation Relations
It is convenient to use an alternate version of weak bisimulation, with a niuch more local
character.
Definition 3.6 P Ao q iff a			T and P			or a $ T and P			q. A relation
?s a local weak bisimulation relation J, whenever p p' and P q for some a then
p1 Mo q1 and q q'; and vice versa.
Lemma 3.7 Every local weak bThirnuThtion reThtion ? a weak bisimulation relation.
Proof: Suppose that p p' for a local weak bisimulation relation , and that P
There are two cases: a $ ? and a = T. We onlv present the a $ T case. In this case, we
have p q for some m, n. We may then fill in the following diagram from the left,
using the definition of local weak bisimulation relation repeatedly:
T			T			T			a			r			T
P			=			Po			Pi			Pm			qi			.			____			=			q
I			I			T			I			T			T			I ________ I			T			T			I			I
P			= Po -0 Pi -0 ...			Pm			?i			0??? ---0			= q
It is straightforward from this that p1 ? q1 and q q1 as desired. ?
3.2.2 Weak bisimulation is a congruence
We use standard bisimulation methodology to show that P ? P1 implies f(P) ? f(P1). We
construct a relation which includes ? arid is closed under application of operations. The
diacritical conventions used in this proof are sumnianzed in Figure 4.
Definition 3.8 We define P			P0 to hold ij)
20
t*, p* Straight versions of t and p
x Source variable of p
Source variable of p*
y Target variables of p and p?
p?, a0 Things on the right-hand side of `?.
a1 Components after one r-step of computation.
a Components after all their T-steps.
a Components after one a' of computation.
Figure 4: Di acritical Conventions
1. p?p0, or
2. There Is a un?variate ternn I, and substitutions a and a0 011 Vars(!), such that for all
x ? Vars(t), a(x)			a0(x) and p a(t) and p0			a0(t).
3,. There 15 a un?variate term t, and substitutions a on Vars(t) and a0 on Vars(t?) such
that p = a(t) and p0 = a0(t*), and Vx' c vars(i?).a(xx,(x?)) a0(x').
?.			p?			p by 3.
Note that			is symmetric.
Theorem 3.9 If  is a fully lVB cool language, then weak b%simuThtiou is a congruence
for.
Proof: By Lemma 3.10, is a weak bisimulation relation. Suppose that p? ? Pt' for
1 = 1,2It suffices to show that f(p? ? f(j7) fi?r all operation symbols f of . Let
I = f(x?, and define a(r?) = pi and a0(r?) = p;; then we have f(p7) = a(!) a0(t) =
by clause 2. Hence f(p? ? f(p?) as desired.
Lemma 3.10			is a weak bisimulation relation.
Proof: It suffices to show that, if p ?` p0 arid p a q, then there is some q0 such that
p0 a q0 and q			q0. There are four cases? depending on the reason that p			p0.
1: This case is trivial.
2: In this case, p = a(t) and p0 = a0(t), where Vx c Vars(t).a(x) ` a0(r). Let p be the
ruloid enabling p a q, and u = target(p). There is an instantiation a of Vars(t),
such that q = ?(u) and for each antecedent .r y of p we have
A* ?(y)			(12)
21
By (12) and the induction l?ypothesis, for each  y, there are teri?s a'0(r') and
&0(y) (where x' = yX'(y)) such that,
--H			a0(?)			=			je(j4)			=			a0(y)
4 = T			a?(x)			?			a"(W)			=			u?(y)			&(y)			(t:3)
Else			a?(r)			M?			&?(`)			?			a?(y)
?Nte have two cases, depending on whether fi was an action rule or a bifurcation rule.
2.action: In this case, no 4 is T. ?Ve have two subcases, depending on whether or not
any a0(x) takes a T-step in (13)
2.action.no: In this case, we have a0(r) ? a0(y) for each antecedentr ? y
of p. 1-lence, p applies to p? =
p			a0(u) =
and q = a(u)			a0(u) =			as desired.
2.action.yes: In this case, there is an antecedent ?o Yo in ante (p) such
that a0(ro) 4% a'0(x0,). Let x01 = yXI(y0). In this case, there is a bifurcation
ruloid (except for variable names) bIx?01 which is
T v4,(r r'I?(r') = x A (x $ x0 V r' $ x01)?
I I?[xo :=
?\?\J? know that
a?(xo)			4% a'?(i?) Co u?(y0)
Let a1? be the substitution on Vars(i*) given by:
ai?(x') =			a??(?xx (x')) r' =
otherwise
By the bifurcation rule (14)
p a?(t)=p?1
(14)
Now, we will run P'i with patience ruloids until it is ready to execute p the
right way. For each r' 4% y in ante (p?) , we have u1'(x') 4% a'?(x') and
for all x1			?			y, we have 6?(x') = at(x') --H aO(xX,( r')). Hence, we have
transitions:
= p?2
Now, for each antecedent r' 4% y of K we have a'0 (x') 4% a0(y), and
for each antecedent y' y, we have a'0(x') = a'0(y). Hence p* applies to
Tho:
P2			a0(n) = q
q			q0 by part 3 of the definition.
22
2.bifurcation: In this case, /? bIxtt for some x0,. Let x0 ?xX,(xlo) Let a(x'0) be the
T-child of a(x0) that caused the transition, and a(x') = a(yx(I))?for other x"s.
Then q = &(1*). By the induction hypothesis, there is a process a (x01) a(x'0)
with a?(?) ffi% a0(x01). For each r' ? r?', let J?(x') = aO(Xy(I)) There are two
cases: n = 0 and n > 0.
2.bifurcation.(n = 0): NVe have a?(vo) a(r'0). Furthermore, for each x' ?
a0(x') --H a0 x (r')) a(x'). hence
q = p0 = a0([)			&(!?) = q
as desired.
2.bifurcation.(n > 0): This is basically the sanie as case 2.action.yes.
3: In this case, wehavep = a(t), pi = a?(!?), and for all x' C Vars(t*) we havea(xx,(xi)) a0(x').
Let p be the ruloid and a the substitution for target variables enabling the transition
p q. That is, for all antecedents x y of p, we have a(x) ? a(y); and
also p = a(t) and q = a(u) where it = target(p).
By the induction hypothesis, we have for each antecedent ` y of p?, a process
&0(y) such that
=			?			a0(x)			=			a"(x')			=			a0(;q)
= r			?			a0(x)			?			a'0(W)			=			a0(y)			(15)
Else			a0(x)			?			a'0(x')			?			a0(y)
3.action: Unlike most other cases, we don't need to apply a bifurcation ruloid to p0;
it's already bifurcated. By repeated uses of patience ruloids for p*, we have
p0=a0([) M
And by K? we have
p2			a0(u) = q0
Now, we have q = a(u) &0(u) = as desired.
3.bifurcation: Otherwise, p is a hifurcation rule, p = Let j0 = ?xX,(xoI) Then
q = a(t?), where a(x) T a(x'0) is the instantiation of the (unique) non-
antecedent of p, and a(x') = a(xx,(xI)) for x' ? x01.
By induction, we have a0(r01) T a0(01?) a(x01). Let a0(x') = a0(r') f:?r
x #xol.
By repeated use of the rol patience rule for [?, we have
p = a0(!?) A a0(t*)
and q = a(1*)			a0(1*) = q0 as desired.
23
4: In this case, we have p = a(t?), p0 = a0(t), and Vr' c Vars([*).a(x') JO(?xX,(Xt)) Let p?
enable the transition p			q. As usual we have
=			=			=
?			=			a0(y')			(16)
Else			?`(r)			?			u'?(?')			?			&?(:q)
There are two cases, depending on			whether fi is			an action or bifurcation rule.
4.action: ?Ve have two subsubcases, depending on whether there are any T-moves or
not:
4.action.no: In tUs case, for all r y C ante(p). we have a0(r) ? a' (y).
So, p apphes to p.' = a'(t), giving us the transition
p			? a'(u) =			q = a(11)
as desired.
4.action.yes: Let Yo be a y such that a'(x) 4% a'(r'), where x01 = X?(y0), and
xo = yX (yo) Clearly, x0 is active in p, arid hence there is a bifurcation ruloid
by?0i N?V?e have
a'(ro) T at(xo') 4% a"(ro') ? a'(yo)
Let a;(?,1) = ae(xx,(xi)) for all Xi # r'0. The bifurcation ruloid bitxo? enables
the transition
p			a1,(P)=p'1.
??e have, for all active X1, a?(?') 4% a''(?'); so repeated uses of the patience
rules for l? gives us
PI
Now, p* applies to p20, giving
p20			a			a `(it) = q0			q = a(it)
as desired.
4.bifurcation: In this case, p is a hifurcation ruloid bit?0 Let p* he the bifurcation
ruloid bir0. \Ve have a(?0,) A a(X'o), and let a(?') = a(x') for all x' $ r?'. Let
x
xo = x,(Xo') By the induction hypothesis, we have a'(r0) 4% a'(r01)
Let a'(?') --H a' (x (TI)) for all x' $ X0,. ??\Te have two subs'ibcases, depending on
4.bifurcation.(n = 0): In this case, we have a'(x0) = &`(X01) &(X01). For all
X? $ r?', we have a?(xx,(r?)) a(x') = a(?'). Hence,
= a'(t) a(ID = q
as desired.
24
4.bifurcation.(n $ 0): In this case, we have
fl--Hi
o?(ro) T			T			a'(?')
The bifurcation rutoid bi$6 applies to 00:
p			a10(t?)
where a10(x') = aO(xX,(x/)) for all x' $ 0'. ?? now use ii --H 1 patience ruloids
on ?0(ft):
M? a0(t?) q0
Then q = a(t?) a0(t*) q? as desired.
3.3 Finitary Characterization: WB cool Languages
As we have seen, fully ?VI3 cool languages respect weak bisimulation. Unlortunately, the def-
inition of fully ?VB cool is infinitary. In this section, we present finitary, decidable necessary
and sufficient conditions.
Definition 3.11 A language is PVB cool if the temns f(') where f is a function symbol and
x are distinct variables satisfy the fully ?7B cool condition.
The proof that ?VB cool languages are fully NVB cool proceeds by constructing the rutoid
sets 1Z(t, ?) for each I and &, and then checking that they satisfjy Definition 3.5. The ruloid
theorem will be presented as what amounts to a functional program, in which we construct
the set of ruloids for each term by induction.
Tbeorem 3.12 Let  be a l?B cool language. Then  is fully lVB cool.
Proof: We first construct sets 1Z(t, a) f:)r all ternis I and actions a E ACtT?, and then show
that are fully WB cool. The constructions for are easy:
= frevyixcVars(t)?
where o(x) = Vx. The constructions for variables are equiy easy:
25
Uij ante(p??)
I u [y'ij :--H--H uij]
Suppose, then, that t f(i) is a univariate terin. Consider a rule p for f:
Cij
Xj			Y'ij
A
Choose ruloids Pij E ?(t?, ??). These ruloids give conditions under which tj . They
have the form:
= ?zA?lAcante(p?5)?
Ii ? `Uij
Rename the target variables as necessary in sonie fixed way so that Vars(ii?5) are all disjoint.
Let the ruloid p be:
Uij ante(p?5)
t			zi[qij :--H--H ujj]
Note that by hypothesis the ruloids for (f(?)) are in the right conespondence with those
for f(i). That is, corresponding to p there is a ruloid:
= fJij?iyijlwxl(r%))X?,,Xj4?jCante(p)?
u
and by induction to each Pij there is a valid ruloid K5:
--H fz'A?A?ante(pii).7xx(f)
Jr C?j
?tj5
Thus, there is a vahd niloid
where
I			(f(A )?[Z'j := 17]
Furthermore, we define xXj (z) for I to be the union of the ?xX, (?) functions for the J?.
That is, if z E Vars(t), then z E Vars(J?) for precisely one i. Let xX, (z) be xX, (z). \??? now
check the parts of Definition 3.5.
Part 1: If I is straight, then each t? is also straight Hence xX,(I7) I., and furthermore f(.i?
is straight; hence (f(x?)* = f(x?., arid so xX,(I?) = I
Part 2: Suppose that is active in I, and z' c \TX'J(z). ?e know that E Vars(I?) for some
i, and r? is active in f(?).4 ?ifurcation ruloids for I niay be built from the bihircation
ruloids for f and i?.
4Note that the ruloid for an transition has only `s as antecedents
26
Part 3: Suppose that p has a r in an antecedent w. Then by construction, some Pid
also has z w as an antecedent. Hence pij is a bifurcation ruloid for Ij. As it proves
a conclusion of the form I? T u?5, the rule p must have an antecedent Xj
hence p is a bifurcation rule as well. Hy construction, fi is also a bifurcation ruloid.
Part 4: Straightforward from the definitions.
4 Rooted Weak Bisimulation
?Veak bisimulation is not a congruence for most process algebras Indeed such basic opera-
tions as nondeterministic choice and selective communication are not \?\7B cool and do not
respect weak bisimulation. For example, the CCS rules for + are
a			a
x			yy
? + ? a			? + ;q a
for all a. In particular, there are no patience rules. \?\?`? have a ? Ta, hut a + b ? ?a + b. For
this reason, some researchers [Hen88] introduce patent versions of +, with the above rules
for all a r, and two patience rules:
x
? +HY			X'+H Y			X+H Y			Y' +H `4
?Vith this notion of choice, one may build a ??I3 cool version of CCS, for which weak
bisimulation will be a congruence.
Themorestandard solutionistouseaslightlydifferentnotion ofequivalence: ?oo?edweak
bisimulation, called ?ootedr bisimuThtion in [I3\V9O]: iNlilneroriginally calledit observalional
congruenee [MilSO]. The definition is given in t)efinition 1.4.
The characterization of R?N?VB cool languages is rather complicated. ?ather ?han do it
immediately, we start with a related, slightly stronger notion, .stivng[y rooted weak bisinin-
lation, which is quite reminiscent of rooted branJ?ing bisinmlation. Sk\N113 cool languages
are much like RWB cool and RHB cool languages, but the definitions and proofs are much
simpler. ?Ve deal with rooted weak bisimulation proper in the next subsection.
4.1 Strongly Rooted Weak Bisimulation
For expository convenience, we introduce a slightly strengthened version of rooted weak
bisimulation. The rule format for rooted weak bisinnilation is based on the ideas used in
much simpler form here.
Strongly rooted weak bisimulation i% a congruence for a wider class of languages than
ordinary rooted weak bisimulation. It probably roughly as useful for actual verification as
the ordinary relation. The canonical difference is, a + ?? ?r ?? but a + Ta #sr ra. The
27
theory of strongly rooted weak bisimulation remains to he developed. Perhaps it will turn
out to be good for something.
Definition 4.1 Processes p and p' are strongly rooted weakly bisimilar, p ?sr q, iff when-
ever p			q for some ? E Act?, then p' ?			? q and v?ce versa.
This is a direct definition of ?sr in terms of ?.
?Ve introduce a rule format which guarantees that all operations respect strongly rooted
weak bisimulation. Note that ?sr is an extremeky powerful relation on its first move; it has
the full power of strong bisimulation on that move. It is not surprising that it respects a
rule format which has the full power of GSOS rules available on its first move. After the
first move, ??? is simply ?; so we use the NVB cool rule format.
A SR?V?I3 cool language, like CCS, then, has two kinds of operations. First, it includes a
NVB cool sublanguage of tame operations for CCS, all the operations except t. Second,
it includes some wild operations defined by arbitrary CSOS rules like + - which are
required to yield terms in the ?JB cool sublanguage after the first step of computation.
Formally:
Definition 4.2 A (not necessarily positive) GSOS(?) language  is SP?i? cool iff the fune-
lion symbols can be partitioned into two sets, of wild and tame operations, suJ? that
1. The targets of all rules in  are univariate terms mentioning only tame operations.
2. The sublanguage of  given by just the tame operations and all their rules is I?B cool.
Tbeorem 4.3 Let  be a Sll?B cool language. Then ?sr is a congruence for .
Pro of: Clearly, if a(x) ? a'(x) for all r C dom(a), and I is a univariate term mentioning
only tame operations, then a(t) ?
Now, suppose that Pi ?sr Pt' for each i. It suffices to show that f(p? ?sr f(P?) Suppose
that some rule p enables a transition f(j?) M* q a(t) where p a(source(p)) and
I = target(p) and a ?= ante(p). For each positive antecedent Xj y of p, we have
pi a(y). flence, p' ? a'(y) for some a'(y) ? a(y). Furthermore, if Pi ? then
P'i as well. In particular, p applies to f(p?), giving a transition f(p?) ? a'(target(p)).
By the first paragraph of this proof, we have a(target(p)) ? a'(target(p)). As this holds for
all transitions from f(p?, and (by symmetry) from f(p?), we have shown that f(P) ?sr f(P?)
4.2 Rooted Weak Bisimulation
"Ve now adapt the tame/wild idea to rooted weak hisimulation proper. First, we give a more
local definition of rooted weak bisimulation; then, exploiting that definition, a rule format
respecting it.
2S
Definition 4.4 A symmetric relation			is a local rooted weak bisimulation it', whenever
P PI and p			q, then there is a q'			such that p1 T*?T; q' ? q. Two proc%9es are locally
rootedly weakly bisimilar,, P ?1r PI iff there is a local rooted weak bisimuThtion relating them.
As with ordinary ?r? this is a direct definition in terms of ?. Local and ordinary rooted
weak bisimulation differ formally in that the local relation only looks at a single step of one
process, whilst the ordinary relation allows any number of T steps of the other.
Lemma 4.5 Local rooted weak bisimulation coincides with rooted weak bisi?nulation,' that is,,
P ?Lr PI iff p ?r P1'
Proof: Suppose that p W?r P?, and that p r. \Ve must show that there is a r' such
that p' ??? r1 ? r. If n 0, then p a q r for somf*a(k* l3y p ?? p', we have
?1 ?*??* q1 ? q. As q ? q', we have q' T r1 ? r. hence, p1 r1 ? r as desired.
Otherwise, n > 0, and we have p* q r. i'rom p ?i? pI we have p' *TT* q1 ?
and from weak bisimulation q' T r' ? r. Again, putting these together gives us
?? T*a?: r1 ? r as desired.
`For the other direction, suppose that P ?r P?? and p a q. N?\e thus have p
with both r?'s being empty; hence, the rooted weak hi simulation condition applies, and
?1 T*aT; q1 ? q as desired. 4
NVe can use the characterization as local rooted weak hi simulation to deduce a rule format
which respects ?r' Some operations, the tame ones, will respect ?; in C(?S, this is all
operations except +. The remaining operations, the wild ones, like t need not respect weak
bisimulation; but they must have ruloids which force them to respect local rooted weak
bisimulation.
For example, suppose that for each rule
r?y
f(x,z)			t
that there are ruloids of the form:
r?y
f(x,z)			T
y?z			_________
I A t[y :--H--H			1			T			t[y :=
(17)
where I is some tame term. For example, if f were +, I would be y.
Suppose P J?r P1 Intuitively, the first rule allows f(p', r) to take a r-transition to an
instance of t, handling the first T moves of p'. The second ruloid lets t do the transition that
f did; the third ruloid handles the final T n?ves of p'. Suppose we have transitions:
a
p			a
T			a			I			T
P			P1			q1			q
29
T			T			(1			T			T			C
Pi			P2			P3			P4			P5			P6			0
WY
a			c
p			u
`i23
TyT\\a
Pi23,
Y6
Pli5 A; 0
0			0
Figure 5: Rooted NVeakl v I3isimil ar Processes
The above rules give (roughly)
6
J kP, T)			tI--H
y .--H
__________			6
f(p', r)			T l[y := P'il			i[y :--H--H q'1] ? i[y :=
In general, though, we need some more structure. Suppose that we have the operation
f, whose rules include
x?y			_______
f(x) ? dy'			f(i) ? x
where d.y is prefixing, (3). For example, f(a.c) `-` 6.d.c t d.a.c. Consider the processes
p = rra(b + r(b + Tc)) and p' = a(b + ?c) + ac + T.T.p'; see Figure 5, where the names
of the states show the correspondence between the processes. NVe have p ?? p1. (These
processes are chosen to illustrate all the difficulties that arise in the general case.) We will
have f(P) ?r f(P1)? but this will require several new operations and a new rule for f.
Let us try to match the transition J(p') ? d.c with some computation from f(p). We
have to do several things. First of all, ?? need to absorb the transition Pi P2. ?Vhen
we do this, we lose the option of performing the ci action that is available to f(p); we have
T*bT*
committed to the transition f(...) , though it is not yet available. Thus we must have
a transition f(p) T 9(P2) for some new function g.
g will wait patiently for its argument to perform an a, with a transition g(p2) T g(p3),
and when it does, will perform something like f's a transition: g(p3) ? 1?(P4) Note that
we cannot simply have g(??) move to d.P4, as the latter has the option of eventually doing
the string cib, but f(P')'s child d.c cannot.
The function A intuitively means that we have performed the f(. . T?bT* and are trying
to get into a state in which it is appropriate to get to its target d.c. It will discard T actions,
in a transition A(P4) T h(Ps). When the process is about to get to the right state, A will
become the target of f's original transition: A(P?) T d.P6 H d.c.
30
Thus, in general, to match a transition from f, we need two intermediate states -? 9
and h in this example -? which represent the intent to do that transition, with g being the
state before the transition has happened, and h the state afterwards. This rather compli-
cated example inspires the following equally complicated definition. Given the top transition
f ? tin this diagram, we insist that the rest be possible as well (where there are T loops
at 11 and 12):
a
T			T
c t'
Definition 4.6 A positive USOS Thnguage is lIJYB cool if U?e operations can be partitioned
into tame and wild operations, such that:
1. The target of every rule contains only tame operations.
2. The sublanguage of lame operations is PVY? cool.
3. For every rule p with target f(,) ? 1 for a ?l)iid operationymbol f,, the following
exist:
(a,) Terms 11 and 12, such that Vars(1), t?'t, vars(t1) and Vars(t2) are mutually
disjoint.
(b)			Bijections ?(?) : Vars(11) H Vars(1) and x2(?) : vars(t2)			Vars(1). (Let ???.?
and --Hf(.) be the inverses, and let A (1)
(c)			The following ruloids for each 0 which is active in f(Y),			each oi such that
0 = q?X (ol), and each o2 such that ro yo E ante(p) and ? (o2) = y0
0?ol,f`I-=;`(1)A($0v1$ol)A\			(18)
A Ii
?2$?y)cante(p)Ay=4xG2)A\ (19)
A 12
I			T			-r1			r1
A 1lI1 $
11			``0			(20)
T 111
31
where 111 = t1[?1
fri ? x2Ir ? i?cante(p).=q;(ri),?=??.2)?
11?I2
\yxi ? yjx ? y?antqp)x=??1)?
1t?t
2			?			21			2
X0?t2			x211r2 # x0
?21
where 121 --H 12[x? . TW21]
(21)
(22)
(23)
2			T			2			______			2
YO			X			y y			?			$ yo			(24)
t2?t
In most cases, 11 and 12 will simply be renamirigs of I; for t. where I is a target variable
rl? 11 and 12 are other variables y' and z'.
Theorem 4.7 J?ooted weak bis?rnulation L? (1 congruence with respect to all 1??B cool tan-
guages.
Pro of: Let  be a R?V??B cool language. It is clear that if I is a univariate term containing
only tame operations, and a(x) ? a'(x) for each x, then
a(t) ? a0([)			(25)
Let p? <=>r Pt? be vectors of ck?se4 terms of . It suffices to show that p J(P) ?tr
= p?. Suppose that p q, and let p be the rule fcw f enabling this transition. Let
= pj and a0(xi) = p?. J?or each antecedent r y of f, we have a(x) ? a(y) for
some a. By local weak bisimulation let ;r = Xl(y) and x2 = __
y			y
ffiM? a60?1) ? a?(x2) D%Y
where a(y) ? a?(g) for each y. \N?hat happens next depends on whether or not there are 7
actions.
Vy.my = fly = 0: In this case, we have a?(x) a?(y) for each antecedent r y of p.
Hence p applies to p?, giving a transition p? ? = a`(1), and q ? q' by (25).
Vy.rny = 0, and Bgo.ny0 > 0: In this case, use (19) to get a transition
`3
32
Now, apply the rules (23) (?? n?) --H I times, giving us transitions
? adO(t2)			(26)
fl?O --H?
where a??(?02)			Jd'(Wo2)			T			&(yo), and Jd0(X2)			u0(?(x2)) for all other x2.
Then, apply the rule (24), giving a transition
?d0(12) T a?(t) =			(27)
From (25), we have q ? q?. That is, p? ? as desired.
?Yo fl?y0 > 0: For this case, we use (18) to get a transition
p
where a'(x0) o+r a:(Xyl(yo)) ,rmao -1 a:()??o) Let Ja?(') = a'?(i) for all
other r1. We then use (20) (z? rn:?) --H 1 times, giving us transitions
aa?(I1) ?
We are now ready to use one of the ruloids giving t2 a a-action. There are two subcases,
depending on whether or not ay1.m?1 > 0. If no such Yi exists, then a?(x2) = a0(y)
for each y = and so we use (22) to give a transition
a:(11) a a?(i) = q0 ? q
which proves the theorem in this case.
Otherwise, such a y1 does exist. In this case, we use (21), giving a transition
a a?(l2)
We then proceed as for (26) arid (27), giving a?([2) ? ?
Thus, rooted weak bisimulation is a congruence
4.3 Discussion
The SItWB cool and It\vB cool ft?rmats provide an amazing degree of programming power
for a language respecting silent bisimulation. They allo'v operations like t, and even some
operations which require negative rules: e.g., a one-step priority operator, whidi gives the
action a priority over
a			? r,, x
Ol(x) a			01(x) ?
33
Note that the full priority operator,
x?x'
0(x) a
6			a
x			x , x
0(x) ?
which is not cool. The negative rule forces 0 to be wild, but the targets of both rules use 0
and thus it must be tame. However, this operation does not respect ? Recall the process
P6a of (5), which alternately offered a 6 and an a transition; recall that P6a ? a + 6, though
they are not strongly rooted weakly hisirriilar. ?Ve have 0(P6a) ? 0(0), hut 0(a + 6) M+
and 0(a + 6) A+ hence 0 does not respect weak hisimulation. As P6a ? a + 6, we have
aP?a ?sr a(a + 6). But 0(aP6a) a 0(P6a) and O(a(a + 6)) a 0(a + 6), and hence the
two are not strongly rooted weak bisimilar.
5 SOSses for branching bisimulation
Branching bisirnulation is a finer relation than weak hisimulation. Not surprisingly, a wider
class of operations respect it. Here, for example, is an operation which respects branching
bisi-mulation but not weak bisimulation:
a			6 x1
x			x
h(x) a			h(x) ? x			h(x) ?
Note that this is almost a NVB cool operation, with h- = h. However, the target of the 6-rule
is x rather than x'; the rule is not -presented, arid if it were it would not be straight, and
thus we would not be allowed to have h = 6.
Let p = a + r6 and q = p + 6. It is easy to verify that p ? q, but p </4-?-6 q. \Ve have
a			ba
h(p) H a + r66, and h(q) ? q 0. In particular, h(q) , but h(p) cannot take
these actions even with r's interspersed. The two are thus distinguishabie by h.
?Ve define fully RB cool languages and related terms in much the same way that we
defined fully `A7B cool languages. Indeed the definition differs only in two places from Def-
inition 3.5:  is a GSOS language (without -transitions) rather than a GSOS(r) language
(requiring r-transitions.), and the matching between targets, part 4 is slightly different than
for Definition 3.5. barb(t, x) must be redefined: barb(t, x) must be defined as 1 if no rule for
I has x as an antecedent.
Definition 5.1 A CSOS language  is Fully RB cool if there is a mapping (?)? : Terms1 TermsSi,
and, for each I E Terms1, a mapping x% (?) : Vars(t?) Vars(t). I?e mse the`ame auxiliary
functions as in Section 3.
1. If I is straight, then xX,(I*) = I
2.			If x is active in I, then for all x'0 ? (x;l(x), ?here is a ruloid			E
x			v
I A
(28)
34
where v is a fresh variable, and
r' $ 4
--H $,i(r') ? =
bixto, is the bifurcation ruloid of I- for r?'; f t is straight, it is also called the patience
ruioidfor 0,.
3, The only ruloids wiTh. T'5 in the antecedent are the bifurcation ruThids,
4, For all I and a, there is a bijedion (?) : 9Z(t, a) H 9Z(t?, a) such that:
ante(p)			?xx,(ante(p?))			(29)
target(p)			?x,(target(p?))			(30)
The functions tx??(x), xyl(y), and xy(y), are defii)ed as I?efore,
Definition 5.2 If 1 is not a univariate term, we define 1 as foUows. For each variable x,
choose an ?nflnite nu?nber of variables 1, 2 , distinct for alland i, and Ystr'ip the
function sending each Xj back to x. Let t be I with the i `Th. occurrence of each variable ,r
replaced by j. IYe define I to be i?, and ? (r') --H Ystnp (xx ?(xl))
Definition 5.3 147e define p p' to hold if:
1. p H? p', or
2. There is a term I, and substitutions a and a' on Vars(t), suJ' that Vr E Vars(t).a(x)
a'(r) and p = a(t) and p' =
3, There is a term 1, and substitutions a on Vars(t) and a' on Vars(t?) such that p = a(I)
and p' = a'(t?), and Vx' E vars(!?),a(?xx,(:rt)) a'(').
4, PO			p by 3.
Note that			is symmetric.
Theorem 5.4 Branching bisimuThtion is a congruence for every R13 cool language.
Proof: As with Theorem 3.9, it suffices to show that is a branching bisimulation relation;
that is, whenever p r, that either
a = r and r			p0:
T
p			r
or
35
there are q0, ?? such that p0 ? q0			r0, and p			q0 and r			r0:
&
v
r
T			&
p			q			r
The proof that is a branching bisimulation relation is by induction on the reason that
p p0, plus an extensive case analysis. Suppose that p p0 and that p r. NVe use
some more diacritical marks beyond Figure 4:
a+ The substitution which will prove the theorem
?t The target of p*, which in this setting is different from that of p.
1: This case is trivial.
2: Suppose that p = a(i) a'(i) = p?, where &(r) ?0(x) for each x E Vars(i). Now,
i need not be univariate. However, by definition, there is a univariate term I and
substitution 4) : Vars(I) Vars(i) sudi that 4)(!) = 1. Let a = a o 4) and a0 = a0 0 4)
Let p be the ruloid for I and a D a be the instantiation giving p a ?? Let
u = target(p); note that r = ?(u). There are two cases, depending on the kind of
ruloid p is.
2.bifurcation: In this case, for some `ro E Vars(I) and x'0 E Vars(I?), we have
Yo
I			T
As a(xo) a0(ro) and a(ro) T ?(y0), the induction hypothesis shows that
a0(xo) matches a(r0)'s move. There are two cases, depending on how a0(ro)
matches a(x0)'s transition.
2.bifurcation.flr: In this case, we have ?(y0) a0(r0). Leta+(x') =
?Ve have a+(r') aO(?xx,(xl)) for all x' C Vars([?). hence ? =
a0(t) = p by part 4 of the definition of
2.bifurcation.[ffiA: This case is like 2.action below, where % = T, and there is
only one antecedent of the rule.
2.action: in this case, p is any non-bifurcation ruloid. Let target(p). For each
antecedent x			y of p, we have:
`3
a0(x) A a'0(r?) Affi
36
where x' yXJ(y). There are two subcases, depending on whether or not there are
any T-steps in any transition a0(x) ?
2.action.no: If there are no r-steps in any transition a0(x) ? a'?(r'), then
we have a0(x) ?ffi* a?(y) for each antecedent ? y of p. So, p applies
directly to a?(t), giving us a transition p? ? a?(u) r?. Let q? =
then we have as desired.
2.action.yes: Otherwise, for some antecedent Xo Yo of p, we have a?(ro) A
ai'(xo') ? a'' (x'o) ? a''(yo). Let a1,(x') = a?(wx,(xl)) for all x' C
Vars(t*) --H fx'?. We apply the biflircation ruloid bit4, which gives a tran-
sition
a0(t)			ai'(t?)			(31)
We now apply patience ruloids for I to move all the a-t(r1)'s to a"(r')'s:
24 a"([?)			(32)
Note that p = a(t) &`(I?) = q0 by 1)efinition 5.3 part 3.
The ruloid p applies to a"([?), and we have the transition:
a a' `(ii).			(33)
where tt = target(p?). Recall that xA (it) = ?J. I?t r' = a"(u). Let a+(y) =
a'(y) for each y, and a+(r') --H a( xX (x')) for each `; then a+(it) = a'(u) =
We have a+(z) &`(z) for each c ?W'uj, and hence r r'. This completes
the [4 diagram as desired.
3: In this case, we have p = a(i) and p' = a.'(i?) for some term 1. As before, we uniquify
variables, giving us a univariate term I arid substitutions a and a' such that p = a(t)
and p' = a0(t*). Let p be the ruloid fc?r I and a ? a the instantiation giving p a
Let u = target(p), and note that r = a'(u). There are two cases, depending on whether
p is a bifurcation or an action rutoid.
3.bifurcation: In this case, p has the form
xo
0=
I -*`?
We have
and			r = a'(y4(I?))
xot ? Yo
I			T
There are two snbsnbcases, depending on how a'(r01) matches a(x0)'s move.
37
3.bifurcation.?: In this case, a(yo) a0(x0,). Let a+ a 0 Y4 Then for all
Ei Vars(1*), we have a+(x') a0(x'). Hence r a+(i?) ao(I*) = p by
De?nition 5.3 part 2.
3.bifurcation.?: This case is about the same as 3.action below.
3.action: For each antecedent r y of p, we have a diagram:
6(r)			6
kY)
a?(')			a'0(r') 3
where x' = yXI(y). Unlike 2, we do not need any snbcases, as p? is already bi-
furcated. For each antecedent r' y of p?., there is a patience ruloid for t?,
giving us transitions
p0 = a?(t?) ? a'?(t?) =			(34)
As j(xX,(x?)) a'?(x') for each x', we bave p q?. Furthermore, the ruloid p
applies to a0(1*), giving a transition
q0 = J0(t?) LL a0(i?) = r0
where zt = target(p?).
?7e have 6(y) a0(y) for each target variable y, and &(xX,(xl)) a0(r') for each
r'. Let a+(y) = a(y) and a+(x') --H a( xx,(r1)); then a+(u?) = r. hence, r f0 as
desired.
4: In this case, we have p = &(i?) and p0 = a0(1) for some term 1. As before, we uniquify
variables, giving us a univariate term I and substitutions a and a0 such that p =
and p0 = a0(1).
Let p* be the ruloid for 1 and a D a the instantiation giving p r. Let u --H
target(p) and it = target(p*), and note that r = a(it).
NVe have two cases, depending on whether p is an action or bifurcation rule.
4.bifurcation: If p is the bifurcation rule for X1jo+ then we must do cases on how
a0(x?), where of course ri=?xX,(rto+)
4.bifurcation.Lr: NVe have a(x?) a+(r?') a0(xi). Let a+(4-) = a(r,') for
all j $ i. ?Ve have q = a+(it.') a0('u) = q0 as desired.
4.bifurcation.[ffiA: This case is much like case `l.adion below.
4.action: For each antecedent r' ? y of K. we have
?1
a0(.r) 44 a'o+(r') `3
3S
where x = x (r1) Ns usual, there are two cases, depending on whether or not
there are any T moves.
4.action.yes: In this case, for some x0,, we have o"(?o) AT a"(r0,)
Let a10 (r') = ae(?xx,(xl)) for r' ? x'0. Apply the biflircation ruloid for x'0 to
a0(t), giving us the transition:
A ai?(l?)
and then use patience ruloids for I to give transitions
aio([*) A a0(1*) = q0
It is easily seen that p = a(t?) a'0(t?) = q0. As usual, p* applies to a0(1*),
and we have a transition
q = a'0(i?) A a0(:?) =
As a(y) a0(y) and a(x') a'0(x') for each y and r', we have r r0 as
desired.
4.action.no: In this case, p applies directly to p?. XVe have a'0(x') = a0( xX (x'))
for each x', and a transition
p0 = q0 = a0(I) A a0(u) = r0.
Let a+0(y) = a0(y) and a+0(x') = a0(?%(x')); then a+0(it) = &0(tt) = r0. NVe
thus have r = &(it) a+0(it) = r0 as desired.
This completes the proof. ?
5.1 Finitary Characterization: RB cool Languages
As in Section 3.1, we present a finitary characterization of i?ulky kI3 cool languages; indeed,
we show that requiring the operation symbols to satis% the Fully RB cool requirement
suffices to guarantee that the whole language is Fully k!3 cool.
Definition 5.5 A language  is PB cool iff the tertns f(xW) satisfy the Fully JIB cool condi-
lion.
As before, we inductively construct 7?(t, ci') and I for all terms I, and show that they
work properly.
Theorem 5.6 Let  be a JIB cool language. Then  is fully 1?B cool.
39
Proof: Let
?(x,?=			4;
Suppose, then, that t = f(ft) is a univariate term. Consider a rule p for f:
Xj
f(x? A ?
Choose ruloids Oji Ei ?(l?, ??). These ruloids give conditions under which It ffi%'? ThQY
have the form:
flij = fz?wwEante(p?5)?
Ii ffiA?- ?t'j
Rename the variables as necessary in some fixed way so that Vars(u??) are all disjoint, and
the variables in Pjj'S are disiolut from those in p Let the ruloid p be:
I			?Ui(;l:)t)(?iyi?j := uij]
Note that, by induction, the ruloids for (f(i))* are in the right correspondence with those
for f(r?. That is, corresponding to p there is a ruloid:
= frt'i?Yijx?Xi(x?ij)=X?,Xj??yqEante(p)
u
with ?xXi (u?) = u and to each flij there is a rujoid
with xXt(u't?) = ?tij. Let
Pij =			fw?wj?z?wCante(Pij).xx,(zl)=
I?Th??
Vt'j
=			:= 17]
Thus, there is a ruloid
=			Ujiante(p?i5)
1*			ii[Xt' := 17.Ytj :=
Furthermore, we define xXt (z) to be the union of the ?xXt (?) flinctions. That is, if c Vars(1),
then z Ei Vars(I?) for precisely one we define ?xXi (z) for I to be xXt (z).
40
1.
If I is straight, then so are all the t%?5.' and f. Hence xX,(t7) = tj, and x?Xi(f(TW)*)
That is, f(x?* f(x?). Hence I f(1?), whence Q,(t?) = f(x%(t?)) = f(i) as desired.
2. Just as for this case of Theorern 3.12.
3. Just as for this case of Theorem 3.12.
4. ?Vehaveante(p?) = uante(o?) uxx,(ante(pij)) = xx,(ante(p)). Vurtheunore?dom(x% t??) ??
i by construction So,
t
as desired.
?x,(target(p?)) =
?xX (i5[X?)			17., Yij := it?i)
X
u[x?4 :--H , y?5 := xX?(i?i5)]
n[?j			t?.,y?
6 Rooted Branching Bisimulation
Branching bisirnulation suffers from the same kind of problem as weak Usirnulation: some
operations, t in particular, do not respect it. The solution is to use rooted branching bisirn-
ulation, Definition 1.6, which is adequate for all of (?CS and most related languages. As
with strongly rooted weak bisimulation, a rooted weak bisirnulation relation gives us the full
power of bisimulation on the first step of computation, arid hence we may nse the full power
of GSOS rules.
Definition 6.1 A USOS language  is 1?BB cool iff the fanction symbols can be partitioned
into tame and wild operations, such that
1. The sublanguage of given by just the tame operations and all their rules is RB cool.
2. The targets of all rules in  are univariate terms mention only tame operations.
Theorem 6.2 Let  be a 1t.BB cool language. Then *7>-rb is a coagruence for .
Proof: Just like Theorem 4.3. t
41
MT Equational Theories
In [ABV92a], we gave a general procedure for taking a GSOS language , and building an
extension ` of  and an equational axiom system which, witb the addition of one induction
principle, is complete for proving strong bisimulations of processes.
[ABV92a] comprises a collection of methods for computing equations and, wh&e neces-
sary, auxiliary operations from the rules of . The central example is interleaving composi-
tion, (1). Interleaving is smooth but not distinctive the full definitions are riot relevant
yet and the method of [A13v92aj introduces the au?'bary operation of Thflmc'rge [BlKS2J,
with rules
and the equation
x
xtLy ? xl Ill?
(35)
xII			y--Hx[Ly+y[Lx			(36)
Leftmerge is a very tractable operation, being both smooth and distinctive. The method of
[ABV92a] gives us essentially the axiom system of [13KS2]:
(x + y)ttz			(r[kz) + (ylz)			(37)
(ax)Iy'			a(x y)			(38)
O[Lx			0			(39)
which is complete for strong bisimulation.
7.1 Equations Fail for Unrooted Weak Bisimulations
However, tt is not WB cool or ItH cool, as it doesn't have a patience riile. Not surprisingly,
it does not respect either weak or branching bisimulation. l?etting stand for either weak
or branching bisimutation, we have
a Ta
However, a L 6 $ (ra) L 6 they're not even weakly trace equivalent:
aW6
a
016
6
0
Ta[L6
r
alib
WY
Ob			ajO
WA
0
42
Xj			Yij
A
7
x?r
r[Ly ? r'[Ly
where t? is a term mentioning only tame operations.
If ` is the [AHV92aJ extension of , then all the targets of new rules are (up to renaming
of variables) equal to some targets of rules of . Pbr example, the target of (35) is the same
as that of (1). Hence, the targets of ` are all tarne terms. Lei us declare that all the new
operations are wild. The tame sublanguage of ` is the same as that ?f 1, and hence `vH
cool or RH cool as appropriate. Thus, 1 is SR\VH cool or RHB cool.
Making [L patient, by adding the rule
(mistake)
will, of course, make it respect both weak arid branching bisimulation. This doesn't help.
While the patient it still enjoys (37), (39), and a suitably modified version of (38), we have
lost the all-important (36). Indeed, consider Ta Tb and (?aLrb) t (?bLra). The ?-children
of the former are:
However,
y
a Tb
y
raIll?b
A
alib
?a ? b
y
(mistake)			(?a?rb) t (?b[tra)			a??b
which is committed to doing the a first; and ra ?? rb cannot evolve via T steps to any state
which is committed to doing a first. Thus the two are not even weakly bisimilar.
Conjecture 7.1 J4'e conjecture that this is not fixable in gene cal; that no non-distinctive
operation can be given a finite axiomization, even with auritiary operators with respect to
weak or branching bisimulation.
7.2 Equations for Strongly Rooted Equivalences
The situation for strongly rooted weak bisimulation and rooted branching bisimulation is
much better: the auxiliary operations created by [AHV99a] can he added as wild operations,
and hence those methods give a sound axiomatization.
Suppose that  is a SRWB cool or RHB cool language. Recall that each rule p of  has
the form:
43
In particular, the new operations all respect ?sr or Hrb. The equations generated by
[ABV92a] are valid under strong bisimulation, and remain valid under coarser relations,
including ?sr and ?rb Thus, the aMorn system is sound.
Completeness is more of a problem, for familiar reasons. ?\?`e must add axioms describing
the equivalence as a quotient of strong hi simulation. This is a (probably easy) open problem
for strongly rooted weak bisirnulation. For rooted branching Usimulation, this is the equation
[BW90]:
a(r(x + y) + x) = a(x + y).
However, for general processes, this wifl not be complete. [ABV92aJ achieve completeness
by using the facts that (1) two finitely-branching synchronization trees are strongly bisimilar
iff they are bisimilar when truncated to all finite depths, and (2) GSOS languages only
generate finitely-branching trees. Any decent process algebra can define a process p which
is infinitely br*anching up to that is, there are an infinite number of distinct processes
p? with p p?. The best approach we are aware of is the use of auxiliary predicates to
test for boundedness, and take a bounded version of the Approximation Induction Principle;
for details, see [I3'A/90J.
7.3 Equations for Rooted Weak Bisimulation
As always, we need to have equations characterizing rooted weak bisimulation as a quotient
of strong bisimulation. For rooted weak bisimulation, these are the familiar
a.r.x			cix
NVe need to extend [ABV92aJ slightly; operations in RNVB cool languages are frequently
non-distinctive. The intuition behind distinctive operations is that at most one rule can
apply to any term of the form f(aipia?p?). However, this is frequently not true in
RWB cool languages. For exarriple, in Definition 4.6, if 12 and t are different, the rules (21)
and (22) give t1 two transitions with the same cause. However, the full force of distindiveness
isn t required for [ABV92a], nor is it here.
Definition 7.2 Let f be a straight operation in a positive GSOS(r) language, and p a rule
for f. The trigger off by fi is the vector (?i,. ???, where ? is O?e action on the antecedent
-* yi.
The trigger of a rule describes when it can fire. N?"e are interested in when seyeral rules can
apply to a term. Clearly, two rules with the same trigger fire or don't fire together. However,
rules with different triggers can also apply; e.g. both niles of (1) both apply to ci Ici, with
triggers (a,?) and (?,ci?. The two rules overlap:
Definition 7.3 Two triggers ? and ? overlap if for all i, if ? 6), then eiTher ? or ? is
e. Two rules overlap if their triggers do.
44
It is impossible in general to a?omatize operations with overlapping rules directly; e.g.,
there is no finite axiomatization of [NIol90]. The definition of distinctiveness in [ABV92a]
simply forbade overlapping triggers. For our setting, we need a looser notion:
Definition 7.4 A straight positive GSOS(?) operation f is instinctive if,
1. whenever two rules have overlapping triggers, the triggers are equal; and
2. the rules for f use the same target variables; that 5, if r y is an antecedent of
one rule for p, then x y is an antecedent of every nile p for some a??; and
3. For any argument Xj? either all rules have a non-& antecedent for Xj or none do.
A set of rules is instinctive if the operation defined by only those rules is instinctive.
(Thus, we may speak of a subset QJ an ope"a.tion's rules being instinctive.)
Lemma 7.5 Let f be an instinctive operation, and let ? be a trigger of the right length for
f. Let R be the set of all rules for f with ? as trigger. Let a? be the aclion and t? be the
target of nile p. Let ??			$`.yj $; ?			. Then ? f(AW) = ZpER c?.t?.
Proof: Each of the rules in R applies to f(X); each p E R causes an (yP transition to tP. As
the triggers of rules of f which are not in 11 do not overlap ?, no such rule applies to f(X).
t
Note that if there are no rules with ? as their trigger, this gives an equation of the form
f(X) 0. The language is positive, so the tricks of [ABV92a] for negative rules are not
necessary.
Lemma 7.6 Let f be an instinctive operation. 7hen f is distHbuti?'e over its active arqu-
ments. Specifically, suppose that Xj is active in f(x). P'or convenience, let C[v] (f(:r))[xj := v]
Then
?C[r+y] ??C[r]+C[y].
Proof: This is a consecjuence of [ABV92h]'s Lemnia 4.3, which essentially says that the
third part of the definition of "instinctive" guarantees distributivity.?
Definition 7.7 A R?VB cool language is classy if, for each rule p for a wdd operation, the
rule p together with all instances of (18) and (19) for it are instinctive.
An equational axiom system E is said to be head-normafizing if, whenever p is a process,
there is a theorem of the form E F p Zi a?q?. Head normalization is the essential property
of [ABV92a]-like theories.
Theorem 7.8 Let  be a classy 1?tYB cool Thnguage Then there is a J?lVB cool extension
` of with a sound and head-normalizing axiom system for strong bisimuThtion.
45
Proof: The method of [ABV92aj proceeds in steps. The first step introduces straight
versions of atl non-straight operations in . If f is not straight, its straightened version j+
has the same rules as f*; the main difference is that [AHlV92aj does not introduce bifurcation
rules taking f to f+.
Thus, if f is non-straight but tame, then  already has a straightened version of f(D
Indeed, the equation
H
is valid, as the rules for the two sides are in such close correspondence. So, we need not
introduce f+ in this case.
If f is non-straight arid wild, then we must introduce f+ The targets of the rules for f+
are the same as the targets of the rules for f:
Yi, 			Y2
f(x) ? g(y1,y2)
a			b
1			Yi, 2			Y2
f+(l 2)			g(y1,y2)
In particular, f has rules (iS) and (19), giving f r-transitions to 11 and j2 f+ has corre-
sponding rules, giving f+ transitions to 11 and 12. ()f course, ?1 and t2 are the same terms
for f+ as they were for j, so the remaining rules (which govern 11 and t2 transitions and
do not mention f) show that f+ has the required auxiliary ruloids. Hence, by declaring the
new f+ operations to be wild, the ? extended by the straightening auxiliary operations is
RWB cool.
The remaining steps of the [ABV92a] method are straightforward given our assumptions.
Straight, instinctive operations can be axiomatized directly as described above. Suppose
that f is straight and not instinctive. ?Ve will introduce some auxiliary, wild, instinctive
operations which jointly describe f. ibr each rule p for j, we define the operation f?, which
just has rules corresponding to p, and the rules (15) and (J9): the rules for f? are identical
to those for f, except that f? replaces J in the sources. The condition of classiness ensures
that f? is instinctive, and hence can be a?omatized. Using the f?, we can axiomatize f:
8 Conclusion
f(r? &- ?fp(Q#)
p
We have given fairly general rule formats for four popular notions of silent bisimulation,
and one new formal as well. In many cases, the rule formats for the rooted equivalences
admit the extension giving equationat axiom systems of [AHV92a]. These axiom systems
are as close to complete as can be expected, given the degree of undecidahility of the silent
bisimulations.
46
8.1 Open Problems
A number of questions remain to be answered.
1. Conjecture 7.1, that nondistinctive operations cannot be finitely axiomatized with
respect to weak or branching hisimulation.
2.
Rooted weak bisimulation might able tolerate negative rules to some (probably very
small) extent, under some interpretation. Can this actually be done? Is the resulting
extension useful?
3. Almost all of the rules used in this study have been positive GSOS. It seems likely that
similar constructions would work for the tyft rules of [CV92j.
4. What is the theory and practice of strongly rooted weak hisin?ilation? Is it adually
good for anything, or does it just have a clean rule lormat?
5. Are the conditions given ill this paper sufficient? That is, are there GS()S operations
which do respect, say, weak bisininlation, but are not \vH cool? We exclude junk
operations; for example, if f has only one rule
6.
r y,x
f(x) a
then f does respect weak bisimulation indeed, f is semanticaily constant, with
f(r) H 0 but this is uninteresting.
As with GSOS languages, we mQy define the congruence generated by a rule format:
two processes are, say, RB cool congruent iff they have the same set of completed
weak traces (viz., without T) in all RB cool languages. (Actually, there are a number
of choices to be made here: e.g., one may use weak partial traces instead of weak
completed ones, or take divergence into account.) DC) the congruences generated by
these rule formats have any good characterization or properties?
9 Acknowledgements
Thanks are due to:
o+ Frits Vaandrager and Rob van Glabbeek for technical and historical advice.
o+ Vicki Borah, F?. Niarten, and the summer heat for terininological assistance.
o+ Paul Taylor for his diagrams package, which let me produce the trickiest diagrains in
this document in half of no time.
47
References
[Abr87] Samson Abramsky. Observation equivalence as a testing equivalence. 7?eoreiiea[
Computer Sci., 53(2/3):225 241, 1987.
[ABV92aj Luca Aceto, Bard Bloom, and i?its Vaandrager. Turning SOS rules into equa-
tions. In Proceedings of LICS `92, pages 113--H124. lEEF Computer Society Press,
1992.
[ABV92b] Luca Aceto, Bard Bloom, and Frits Vaandrager. Turning SOS mies into equa-
tions. Technical Report CS-R9218, C\?\?I, 1992.
[BC90] Kenneth Birman and Robert Cooper. Tbe Isis project: Real experience with a
fault tolerant programming system. Technical Report 90-1138, Department of
Computer Science, Cornell University, July 1990.
[BCG91] Kenneth P. Birman, Robert Cooper, and Barry Gleeson. Programming with
process groups: Group and multicast semantics Tedinical Report 91-1185, De-
partment of Computer Science, Cornell University, January 1991.
[B11R84] 5. D. Brookes, C. A. R. Boare, and A. w. Roscoe. A theory of commumcating
sequential processes. J. ACM, 31 (3):560 599, i984.
[B1M88]
Bard Bloom, Sorin Istrail, and Albert R. N4eyer. Bisimulation can't be traced
(preliminary report). In Confrrence Record of Ihe F?fleenih Annual ACAJ Syrn-
posium on Principles of Programming Langu?qes, pages 229--H239, 1988. Also
appears as MIT Technical Memo MIT/LCS/TM-345.
[BIM90j Bard Bloom, Sorin Istrail, arid Albert R. N1?vcr. Bisimulation can't be traced.
Technical Report TR 90-1150, Cornell, August 1990. (To appear in JACM).
[BK82]
J. A. Bergstra and A. ??V. Klop. Fixed point semantics iri process algebras. Techni-
cal Report INV 206/82, Department of Computer Science, Mathematisch Centrum,
Amsterdam, The Netherlands, 1982.
[Blo89j Bard Bloom. Ready Simulation, BisimuThtion, and The Semantics of CCS-Like
Languages. PhD thesis, Massachusetts Institute of Technology, August 1989.
[B1o90] Bard Bloom. Strong process equivalence in the presence of hidden moves (pre-
liminary report). (Unpublished), July 1990.
[B1o93] Bard Bloom. Ready, set, go: Strudural operational sem??tics for
linear-time process algebras. Technical Report 00000, Cornell, 1993. (to appear).
[BM90] Bard Bloom and Albert R. M?yer. Experimenting with process equivalence.
In Dr. Marta Kwiatkowska, editor, Proceedings of the International BCS-F4CS
I'Vorkshop on Semantics for Concurrency, pages 189--H201, Leicester, U.K., July
1990.
48
[BW9O] J. C. M. flaeten and NV. P. NVeijland. Process Algebra. Cambridge Tracts in
Theoretical Computer Science is. Cambridge University Press, 1990.
[CPS59j
[Gla9O]
Rance Cleaveland, Joachim Parrow, and B. Steffen. The Concurrency NVorkbend?.
In Proceedings of the Workshop on Automated Verification iWethods for Finite
State Systems. Springer-Verlag, 1959. LNCS 407; to appear in ACM TOPLAS.
R.J. van Glabbeek. The linear time branching time spectrum. In J.C.M.
Baeten and J.W. Klop, editors, Proceedings CONCUl? 9(), Amsterdam, volume
455 of Lect. Atotes in Computer Sci., pages 27&--?297. Springer?Verlag, 1990.
[Gro90] Jan Friso Groote. Transition system specifications with negative premises. Tech
nical Report CNVI report R-CS5950, CNN?1, 1990.
[GV92] Jan Friso Groote and Frits Vaandrager. Structured operational semantics and
bisimulation as a congruence. Information and Computation, 100(2):202 260,
October 1992.
[Hen55] Matthew fiennessy. Algebraic Theory of Processes. MIT Press Series in the
Foundations of Computing. MIT Press, Cambridge, Massachusetts, 1955.
[11M55] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism arid
concurrency. J. ACM, 32(1):137--H16i, 1955.
[MilSO] Robin Milner. A Calculus of Communicating Systems, volunie 92 of Lect. ATotes
?n Computer Sci. Springer-Verlag, 1950.
[Mil5lj
Robin Milner. A modal characterisation of observable ruachine-behaviour. In
E. Astesiano and C. B5hm, editors, CAAP `81: Trees in Algebra and Program-
ming, 6th Colloquium, volunw 112 of Lect. Votes in Computer Sci., pages 25--H34.
Springer-V&lag, 1951.
[Mil53j Robin Milner. Calculi for synchrony and asynclirony. 1?eoretical Computer Sci.,
25(3):267--H310, 1953.
[Mi154]
Robin Milner. Lectures on a calculus ft? communicating systems. in 5. D.
Uwokes, A. NV. Roscoe, and G. NVinskel, editors, Seminar on Concurrency: CAIU,
July 9-11, 1984, volunie 197 of Lect. iVotes in Computer Sci., pages 197--H220.
Springer-Veri ag, 1954.
[Mii59a] Robin Milner. Communication and Concurrency. Prentice Hall International
Series in Computer Science. Prentice Hall, New York, 1959.
[Mil59b] Robin Milner. A complete axiomatisation for observational congruence of finite-
state behaviours. Information and Computation, 51(2):227 247, May 1959.
Faron Moller. The importance of tlie left merge operator in process algebras. In
M. Paterson, editor, Automata, Languages and Pmgmmming: 17th International
Colloqium, volume 443 of Lect. Notes in Computer Sci., pages 752 764. Springer-
Verlag, July 1990.
[Mol90]
49
[Par81]
[Plo81]
[Uli92]
D. Park. Concurrency and automata on in?nite sequences. In P. Deussen, editor,
Theoretical Computer Science, Lect. Notes in Computer Sci., page 261. Springer-
Veriag, 1981.
Gordon Plotkin. A structural approach to operational semantics. Technical Re-
port DAINIl FN-19, Aarhus University, Computer Science Department, Denmark,
1981.
Irek Ulidowski. Equivalences on observable processes. In Proceedings of the Sev-
enth Annual JEEE Symposium on Logic in Computer Science, pages 148-161.
IEEE, 1992.
[Vaa91] Frits Vaandrager. private communication. (email discussions), June 1991.
[vG93] Rob van Glabbeek. The linear time - branching time spectrum ii: The semantics
of sequential processes with silent moves (preliminary version). Available by
anonymous ftp from Boole.stan:'ord.edu, April 1993.
[vGW89j
Rob van Glabbeek and W. P. Weijland. Branching time and abstraction in bisim-
ulation semantics. In G. X. Ritter, editor, Jnformation Processing 89: Proceedings
of the IFIP 11th ?Vorid Computer Congress, pages 613 618. North-Holland, Au-
gust 1989. TUNI report 19052 (= SFB-Bericht Nr. 342/29/90 A) and CNVI report
CS-R91 20.
Sam Weber, Bard Bloom, and Geoffrey Brown. Compiling Joy to silicon: A
verified silicon compilation scheme. In Tom knight and John Savage, editors,
Proceedings of the Advanced Research in VESI and Parallel Systems Conference,
pages 79--H98. 1992.
50
[WBB92]
