BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1372
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Ready, Set, Go: Structural Operational Semantics for Linear-Time 
        Process Algebras
AUTHOR:: Bloom, Bard 
DATE:: August 1993
PAGES:: 37
ABSTRACT::
We investigate the relationship between operational semantics, equational 
semantics, and ready equivalence (a well-known relative of failure equivalence 
and testing equivalence) in process algebra. We give a class of structural 
operational semantic rules, called winterized rules, which define 
operations respecting ready equivalence. The class of winterized rules is 
surprisingly broad; it includes some copying operations which would seem 
to violate ready equivalence. Membership in this class is decidable in 
$O(n^{2})$ time. We show that for any process algebra defined by such rules 
has complete equational axiom system. These methods - winterizability in 
particular - apply mutatis mutandis to other linear-time process equivalences.
END:: CORNELLCS//TR93-1372
BODY::
Ready, Set, Go:
Structural Operational Semantics for
Linear-Time Process Algebras
Bard Bloom*
TR 93-1372
August 1993
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
+ bard?cs.cornell.edu Supported by NSF grant (CCR-9003441).
Ready, Set, Go
Struct?ral Operational Semantics for
Linear-Time Process Algebras
Bard Bioon? *
Coriieii U?ivcrsity
Aiigiist 10,1993
Abstract
We investigate the relationship between operational semantics, equational seman-
tics, and ready equivalence (a well-known relative of failure equivalence and testing
equivalence) in process algebra. We give a class of structural operational semantic
rules, called wintenzed rules, which define operations respecting ready equivalence.
The class of winterized rules is surprisingly broad; it includes some copying operations
which would seem to violate ready equivJence. Membership in this class is decid-
able in 0(n2) time. We show that for any process algebra defined by snch rules has
complete equational axiom system. These methods wintenzability in particular
apply mutatis mutandis to other linear-time process equivalences.
1			Introduction
Process algebras serve the same role in concurrency that the A-calculus does in sequential
block-structured languages, isolating the essential leatures 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, arid so forth), there is a
need for many process algebras. Developing the right 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 body of mathematics to make
the development and use of process algebras simpler.
Most process algebras give a notion of process transitions: p 4 p' meaning that the
process p can perform the action a and thereafter behave like p'. This relation is gener-
ally defined by structural operational semantics (SOS). This notion of process behavior is
straightforward to define and useful for many purposes, but by itself it is too detailed for
* bard?cs?corneII edu Supported by NSF grant (CCR-900344?)
a semantic theory. The major schools of process algebra introduce more abstract seman-
tic models, generally based on process equivalences. These equivalences induce algebraic
theories and are hetpful understanding and verifying programs.
CSP, one of the major schools of process algebra, uses semantics built on the notion
of failure equivalence (or testing equivalence) [to, 11,14]. Failure equivalence is (using the
word loosely) a linear-time semantics; that is, the meaning of a process is given by a set
of suitably annotated linear executions of the process. Failure equivalence is precisely the
right equivalence for CSP, in the sense that it is conipositional (if two processes are failure
equivalent, they remain failure equivalent in all (?SP contexts) and fully abstract for most
notions of observation (processes are failure equivalent iff they produce the same observations
--H e.g., completed traces in all CSP contexts)
CCS and ACP, two other main schools of process algebra, use a considerably finer bisimu-
lation semantics; indeed bisimulation is generally regarded as the finest reasonable notion of
process equivalence in this area of process algebra. Risimulation is a branching-time equiv-
alence; p H q iff, roughly, p and q make the same decisions at the same time. Bisimulation
semantics are compositional but not frilly abstract for most notions of observation.
A typical example of a process whid? is correct up to failures (that is. up to visible
behavior) but not correct up to bisimulation is a lossy delay link, which models certain
communication media: a process which accepts data at one port, pauses, and either produces
the input data at its output port or loses it. There are several kinds of l(?ssy delay links up
to bisimulation: e.g., the link which loses data upon receipt (the CCS process abc + abd) is
not bisimilar to the one which loses it during the delay (a(6c + bd)). However, those links
are indistinguishable in failures equivalence, and hence equivalent in CSP.
1.1 Structural Operational Semantics and Process Equivalence
In previous work [8, 13, 2], we and others have developed the connection between structural
operational semantics and hisimulation. This work allows us to recreate (?CS-ACP style
theory in a wide variety of settings. Given a specification of a process algebra by suitably
structured rules, the theory shows that bisimulation is compositional, and shows how to
derive a complete equational axiom system for it. Thus, simply by writing down the SOS
definition for the algebra, one automatically gets a theory along the same lines as CCS and
ACP for it. The automatically-generated theory is coniparable in style and power of theories
of CCS and ACP, and indeed identical to it in many standard cases.
In this study, we show similar results for the ready semantics [4,12, 18] a shghtly refined
version of failure semantics. NVe give a large class of structured operational rules for whidi
ready semantics are always compositional, and show how to derive a complete equational
axiom system for such rules. The results are surprising in a few ways; in particular, copying
operations generally require branching-time semantics, but we give a large subset of copying
operations (including all the ones appearing in practice) which respect linear-time semantics.
Our rule formats are decidable in O(n2) time.
Similar results hold for many other linear-time semantics. hi [6], we give a similar story
for partial trace semantics. In fact, similar results hold for most other strong linear-tinie
semantic models; the details will be presented in due course. One notable omission from
2
this list is failure equivalence itself; the most general classes of SOS formats we know are
unsatisfactory.
Section 2.1 is for notation. Section 2.2 gives basic definitions of structural operational
semantics (SOS). Section 2.3 gives the definitions for ready simulation. Section 3 shows how
SOS-definable operations can violate ready semantics, using copying and polling. Section 4
introduces the class of straightforward ready rulcs, SOS systems without copying or polling,
and shows that such systems respect ready semantics. Section 5 shows that a suitably re-
stricted form of copying, winterizable copying, is compatible with ready semantics. Section 6
shows how to derive a complete equational axiom system from a set of rules. Section 7 gives
a (contrived) straightforward ready language for which ready semantics are fully abstract.
Section S gives conclusions and open problems. The appendix gives an 0(n2) algorithm for
deciding winterizabili ty.
2 Preliminaries
2.1 Notation
W'e use fairly standard notation, though we write A it B for A n I? = e. ?Ve often introduce
eccentric notations for tuples; e.g., we write write the tuple (I, a, t? as t 4 1', when we are
interpreting it as a formula.
NVe are frequently concerned with actions a and strings of actions s. NVe denote the empty
string by ?.
We use vector notation, Xffi to denote a sequence of items named ?I, ?2We assume
that the sequences are of the correct lengths, which are always clear from context. Operations
and relations on vectors are to be interpreted pointwise. For example, the equation :i' = y
means that i and j have the same length. arid that Xj = y? for each i.
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. ?Ve are concerned witti C1SOS and related
classes of rules; to discuss these, we need some notation.
A process algebra language, or simply "language," includes a finite algebraic signature.
The definitions of signature, term, and so f:?rth an fairly standard. A signature "` is a finite
function from a set of operation symbols f, g,h.... 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(t1/?)			where ?(f) = n
A term is closed if it coritains rio variable symbols; process algebras generally contain nullary
operators and thus have closed terms. This is important, as closed terms are processes
which can be executed. There are no bindirig operators, arid in particular no rec ? Pj
operator for recursive process definition a Ia CC 5. Our definitional schema are powerful
enough to include general nontermining computations, even without recursion; and any
3
program written with rec ? over any of our caiculi 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. When  is clear from context, we simply write Procs and Terms. A term is un?variate
if no variable appears in it more than once; Termsi(') or simply Terms1 is the set of univariate
terms.
Actions a are elements of some finite nonempty set Act. Transition formulas describe
possible transitions. A positive transition formula is a triple, written I 4 I', where t and 1'
are terms, and a is an action symbol. A negative transition formula is a pair I 4. A forniula
is primitive if I and I' are variables: x 4 ` and r 4.
A USOS rule is a pair (ii, f(i) 4 t?, where ? is a set of primitive transition formulas,
subject to certain conditions. GSOS rules are usnally written:
u?fxi?yi5i?j?m??uui?xi%?3 1
n) 4 I
The conditions are: the variables rffl g are all distinct, and the variables in I are at most x,g.
We use the following terminology to describe parts of a GSOS rule:
o+ ante(p) = Ii is the set of antecedents.
o+ cons(p) = f(i) 4 I is the consequent.
o+ f(x? is the source.
o+ I is the target.
o+ c is the action.
For example, the interleaving parallel operation p q and full sequencing operation p; q
are GSOS: for each action a, there are rules:1
a			a			a
X1HYi			X2HY2			xl H
xi			II x2 4 Yi I x2			x1 x2 4 x1 I Y2			xl ; x2 4 Yi x2
_______________			X24Y2,V6.x1
xi			; x2 4 Y2
For this study, we assume that process algebras have the operations of action prefixing
and nondeterministic choice. For each action a, ap is a process whidi performs an a and
thereafter behaves like p; for all p and q, p + q mQy behave like either p or q. These have the
rules (for each a):
a			a
________			X1HYi			X2HY2
a			a			a
ax H x			x1 + x2 H ili			xl + x2
If ? is a rtile format (that is, a set of rules), an JZ language is a finite signature Z of
operations together with a finite set of rules 1? C ?, where all operations in R are in ? and
used with the correct arity.
`The last rule has one hypothesis for each b Ei Act whicl, we abbrevjate with a ciuantifier.
4
Symbol
a, b, c, d
(3
s
p, q, r
I, u, t'
x, y,
Usage
Actions; elements of Act
Actions or			elements of Act?.
String of actions
Processes
Process terms
Variables
ii??igure 1: Conventions
In this study it is convenient to use readyfoin?u1as and nail transilions, Ready formulas
comprise a term and a set of actions, written rs([) B. The intent of rs(1) = B is that
the possible actions of I are precisely the elements of B. The ;" operator may be phrased
conveniently with ready transition formulas:
riYi			?2rs(x1)=
a			a
X2			Yi			2			i 2 -> Y2
Ready formulas can be expressed as many positive and negative transition formulas with
some care with variable names, and thus rules with ready formulas rs(r) = R as hypotheses
amount to CISOS rules. Thus, by the methods of [S, 7]., rules involving ready formulas
and null transitions uniquely define approriate, computable, finitely branching transition
relations p q between closed terms.
Null transitions, x H y? are a notational convenience later on: they are intended to mean
that  and y are bound to the same term. This can be trivially expressed in the GSOS
format by using x everywhere y appears. ??e set Acta Act u f&], and with a slight pun we
use the notation x 4 y for ? c Ad? to range over r H y and r
In this study we work with a variety of objects including variables: terms, transition
formulas, rules, and so forth. For any such object il, Vars(?) is the set of variables in fI.
If x C Vars(?) and ? is a suitable object, then fl[ := ?] is ? with ? substituted for x. No
constructs in this paper bind variables, so the definition is not subtle.
It is often convenient to rephrase this in terms of substilutions (also calied insiantiations
when they refer to rules), which are partial functions a from variable names to Procs. NVe
extend a to terms I with Vars(I) C dom(a) by:
a(f(I1(n)) = f(a(Ii)
If ? is a transition formula ?4+ C Procs x Act x Procs, and a is a substutition, and
Vars(?) C dom(a), then we may define the relation a,?# ?:
I%u			<#			a(I)4a(?i)
14			?			?qCProcs.a(I)?q
a,?4+			=			rs(t)=B			?			Vb c P.Bq C Procs. a(1) 4
Vb ? B.?q c Procs. a(t) 4
a,4			?=			f%u			?			a(I)=a(ii)
Term			Notation			Reference Type
ready set			rs(p)			(1)			set of action
ready pair			(s ? X)			Definition 2.1			(string of actions ? set of actions)
ready semantics			R?]]			(2)			set of ready pairs
Figure 2: Ready Definitions
??e extend ? to sets of formulae:
a,?WJJ			W)cTha,%+K?.
The GSOS theory of [?, 7] shows for any USOS language , there is a unique appropriate
transition relation ?`; that is, one satisf,'ing the following properties:
1. For any process term p = f(pi,. . ,p?) 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(x?) = pi for each i
a ? ante(p)
(c) a(cons(p)) = p 4 q.
2. For each rule p and instantiation a such that a,A# ante(p), then a,## cons(p).
This relation is denoted H'C, or simply H when  is clear from- context. The same holds for
languages in related formats; in particular, GSOS rules extended with ready formulas and
null transitions.
2.3 Ready Semantics
In this study, we concentrate on ready semantics. To describe these, we need several defini-
tions all involving the word "ready," which are summarized in l?igure 2. The ready set of a
process p is the set of actions that p is ready to perform:
rs(p) = ?a p 4?			(1)
Definition 2.1 A ready pair (s ? X) for a process p compflses a string 5 and set Y of
actions such that, for some p', p 4 p' and X = rs(p').
The ready semantics of a process, R?p]], is the set of ready pairs of the process; that is,
= f)?rs(fr))Ip4p'?			(2)
Ready semantics are a slightly refined version of faWur 5 semantics [10]. Failures seman-
tics differs from ready semantics by only providing partial information about the ready sets.
Failures semantics are fully abstract for observing traces in CSP. Ready semantics are not
fulty abstract for any known process algebra, aside from some fiiirly contrived ones designed
specifically for that purpose; e.g., the language of Section
6
However, for practical purposes, it isn't too far off. As ready equivalaice is finer than
failures, anything which is proved correct up to ready semantics is also correct up to failures.
It isn't much finer. Semantically, the two models have similar information; failures are a
slight blurring of the information in readies. Practically, we know of no natural examples
of protocols which are correct with respect to failures hut riot ready semantics. The two
semantics are equally easy to understand and work with; indeed, the formal manipulations
are almost identical. Failure semantics simply requires an extra step (taking closures) in
many proofs.
The real reason for working in ready semantics in this study is, of corirse, that the
mathematics we present works quite cleanly for them and the hest known results for failure
semantics are much less appealing. We fiope, however, that these results on ready semantics
will give some insight into similar results for failures.
3 GSOS Operations which Violate Linear Semantics
In a linear-time semantics, the meaning of a process is given by a set of annotated runs.
We are thus lead to suspect that operations which act on a single annotated run at a
time will behave reasonably. In particular, operations which use information not present
in the annotated run are likely to not respect the semantics. GSOS rules Miow copying
and polling, which use information not available in ready pairs; both capabilities can violate
ready semantics.
3.1 Polling
The first CISOS phenomenon which breaks ready equivalence is polling, or testing dur?ing
execution. This arises naturally in many settings. For example, we introduce the operation
tA, with the intent that ? ?A Q allows P and Q to communicate via actions in A, and also
P may ask whether or riot Q is willing to do such an action without actually performing it.
We require that for each action a E A, there be actions ay arid an. all distinct from each
other and from the a's. If P ??Y p, and P L>fl p", then P tests Q for the ability to do a. If it
can do a, P will then behave like P'; otherwise, it will behave like P". 1'or each a E A, ?A
has these rules; the action 0 is some fixed uninteresting action.
a			a			ay			a			an			a
XiYi,X2Hy2			x1HYi,x2H			Hy?,x2			(3)
Xi			x2 4 Yi			Y2			?1 tA 2			:Yi tA 2			i tA 2 4 Yi			2
The polling operation can distinguish between ready equivalent processes. Let P1
a(b + cd) + a(f + cc) and P2 a(b + cc) + a(j + cd); see Figure 3. P1 and P2 are ready
equivalent, both having the ready set
(??taJ),(a?t6,c?),(a?tc,f?),(ab??),(ac?fdJ),
(acd ? ?), (ac ? (eJ), (ace ? o), (af ?
7
Pi
WY
WA
o			0			0			0
W			f A			W			?c			A
o			0			0			0			Q			0			0
o			0			0
Figure 3: keady Equivalent Processes
Let P3 be a.by.c.d, and A fa, b, ccl, 6, ff. Then
?3 ?A ?1			?3 fA P2
4			by.c.d ?A (b + cd)			4			by.c.d tA (b + c6)
4			cd tA cd			4			ccl ?A cc
4			dtAd			4			clf4C
(The other computation from ?3 ?A ?2 doesn't even get that far.) So, P3 ? ? P1 has a trace
0000; ?3 ?A ?2 has no such trace. Thus, polling - as exemplified by the tA operation -- violates
ready semantics.
3.2 Copying
The other GSOS phenomenon which breaks ready equivalence is copying. Ready pairs
include very limited information about possible alternate paths of computation. It is thus
not surprising that copying operations, which duplicate processes and cal-i run them along
independent computation paths, can violate ready semantics. For example, the processes
= a(bc+ bd) and Q = abc + abd are ready
RIP? = = ?(&?faJ),(aafbt),(ah?fct),(ab?fdt),(abc?o),(obda?)?
P and Q differ only in that P decides whidi of c or d to do on its second action, and Q
decides on its first.
It is straightforward to distinguish them using copying operations. If we run P for one
step, it has not decided; if we run Q one step, it has decided. I?hus, if the operation split
duplicates its argument after one step, the duplicated children of F could behave differently,
while the duplicated children of Q must both obey the decision made at the first step arid
will thus behave the same. The following set of (admittedly contrived) CSOS operations
distinguish them.
x y
split(?) 4 g(yffi
split(P) can perform trace abbbcd in one of its three possible executions:
spht(a(bc+bd))4g(bc?bd)Hb(bc+bd)?(bc$bd)4c(bc$b4)4c??4????d???
However, split(Q) cannot perform this trace. The computations all follow the pattern:
split(abc+abd) 4g(bc) 4 bcII bc4 cli ac% c c4 0?? c 40 0
However, it cannot perform a abbbcd trace. Thus copying operations can distinguish between
ready equivalent processes. More generally, operations like split can distinguish between
processes equivalent in most linear-time semantics.
4 Straightforward Ready Rules
?Ve have shown that copying and polling are incompatible with ready semantics. They are
the only GSOS phenomena which which are incompatible. Specifically, we define the class
of slraightforward ready rutes, GSOS rules without copying and polling, and we show that
any set of operations defined by straightforward ready rules respects ready semantics.
Straightforward ready rules are designed to exploit the information avlable in a single
ready pair and nothing else. The information from t1ie s part of the ready pair (s ? X) is a
sequence of actions; thus, in each rule, we may watch a process p take a step.2 X gives us
full information about what actions p is willing to perform, but, as it comes only at the end
of the trace, once we have seen what p is willing to do, we cam?ot run p any further.
This leads to the following rule format. Rules have two kinds of hypotheses, action
hypotheses (x 4 y), and testing hypotheses rs(r) I?. Syntactic restrictions on the rules
prevent copying and ensure that, once a process has been tested, action hypotheses cannot
be applied to it.
Straightforward ready rules have the form:
fXi H? y,? i C			U frs(x?)			Bj?i C J--H?
f(?I`n) 4
where o?? E Acte by our conventions, and
1. I+ttkandl+uk=fl,...,nl.
2. I is a univariate term with variables at most fyili c J+J.
The positive antecedents allow execution of some arguments r? along traces Sj. The
ready test formula antecedents allow the rule to investigate the ready sets X. Restriction 1
ensures that a process cannot proceed once it has been tested; that is it cannot be polled.
Restriction 2 prevents copying.
2Multi-step antecedents can be inconsistent with negative tests as shown in [7]. Probably a stratified
system along the lines of [9] could be developed for ready equivalence hut we have not attempted this.
9
Tbeorem 4.1 If is a straightforward ready Thnguage, then ready semantics are adequate
and compositional for .
Proof: This theorem is a corollary of Theorem 4.2 below.
In fact, a stronger statement holds. The value of Rlf(pi,n)1 depends in a particu-
larly simple way on the values of R?p1?,R?p??: R?f(p7)? is a pointwise function of k?[p1?,
R?pn?. Let Rif? be the ftmction taking n sets of ready pairs Si R[p1?,... , =
to R?f(p1,. . . ,pn)?. Compositionality is equivalent to the statement that R[f? is well-defined.
In Theorem 4.2 we show that it not only well-defined, but pointwise defined.
Theorem 4.2 Any operation f in a straigh4lomvard ready Thngu?qe  is pointwise defined.
That is, there is a function ? on ready pairs such that
R?f?(S1= f?j(sin)sj E S?J
Proof: This theorem is proved by a detailed analysis of pn?cess execution. It is actually a
corollary of the proof of Theorem 5.10, and rather than presenting both we simply present
the more general one. However, a discussion of the methods is essential.
Executing a term f(p? for one step will in general result in a term t[y := q? for some
vector q of ot4children of p% hence we must consider how processes execute in all contexts,
not just as arguments to single function symbols. Following methods of [S, 7], we develop a
set of ruloids which describe the behavior of all terms.
Definition 4.3 Ruloids are rules in which the conclasion has the form t 4 u for some term
t, rather than the form f(?) 4 u as reqniredfor rules.
Rules carry proscriptive force; that is, they define tl-ie behavior of all terms of the language.
Ruloids simply carry descriptive force; that is, they explain how the rules cause complex
terms to compute.
In particular, for each univanate terni t and 0 E Act?, we calciilate a set 9?(t, s) of ruloids
which precisely capture the circumstances under which t can perform s
Definition 4.4 A set ? of ruThids is just right for a ?nivaHate term t and a string 5 of
actions if,
1. The conclusion of each p C 9? has the form t 4 I' for some
2.			P?rmally, let a : Vars(t) Procs,
C 9?', and extension a' D a to
9? explains all the transitions possible for instances of
and suppose a(t) 4 q. Then There is some ruloid p
Vars(p) such that:
(a) a' ? ante(p)
(b) a'(cons(p)) = a'(t) 4 q.
3. Every ruloid in 9? is valid. Formally, if a : Vars(p) Procs and a ? ante(p), then
a ? cons(p).
10
For example, the following set of ruloids for (x II are just right for that term and the
action a:
H X			H
____________________			o,rs(y)
iy);z)()?y);z			(x?y);)$11y');			??Zffi?x?i(;)z4
Indeed, it is a corollary of the proof of Theorem 5.10 that, for any straightforward lan-
guage , univariate term t, and string s of actions, there is a finite set ?(t, s) of straightfor-
ward ruloids which is just right for I and s. Lemma `1.2 follows fairly easily from this fact.
5 Limited copying is compatible with ready semantics
Copying running systems of processes is nontrivial to implement, and unusual as a language
feature. However, copying inactive processes is a useful way of specif,ying many standard
constructs, For example, Milner's !p operation [15j, which turns p into a server, and the
standard while loop, are best specified by rules of the form:
t
x4y			Yi			(5)
4 ?ll !x			while r? do x2			x2 while Yi do x2
where t is a distinguished "true" action and ?`;" is sequencing.3
These rules are not straightforward ready rules, as both x and its child y appear in one
and x2 is copied in the other. Nor are they equivalent to any straightforward context, as they
are not semantically poiritwise extensions of any function. Nonetheless, they make perfectly
good sense; the ready trace semantics of the two are compositional and adequate, and indeed
both rules have appeared in the literature.
The arguments of ! and while are being copied in a particularly innocuous way. Rather
than having chunks of running code be copied, with all their state, they simply copy parts
of the original program. From an implementer's point of view, the original program contains
a loop, or is reentrant.
From a semantic point of view, the danger in copying comes from the possibility of
detecting branching; as with split, of ailowing a process to possibly make a decision, then
copy it, and explore whether or not it made the decision. The behavior of such an operation
depends on information not in the processes' ready semantics.
However, it is semantically reasonable to use any information available in the ready
semantics; in particular, to use information from miiltiple ready pairs; that is, in multiple
independent runs from the beginning of the program. For example, R?!p? is the interleavings
of finite numbers of elements of Rj[p?, with suitable `Y's. \Vhile this function is not linear, it
is well-defined on sets of ready pairs.
In this section, we give a larger class of rules whidi admi?,s while arid !. Briefly, we
consider GSOS rules which obey a bookkeeping discipline which onky allows copying of
3A useful while operation will probably have otlier rules allowing x1 to con?niunicate with other processes.
11
unexecuted programs. For each univariate t?erm I appearing in the rules of the language, we
partition the variables in I into sets of frozen and liquid variables, Froz(t) and Liq(I).
The intent of these sets is that the frozen variables should represent subterms which must
necessarily be subterms of the original process in any execution; liquid variables could be
descendants of the process. Somewhat more formally: if some variable xi is frozen in 1, and
for some process term q and string s of actions we have q 4 I[.Th := p?, then pi is a subterm
of q and appears in each step of the execution. For example, x may properly be marked as
frozen in ax and x + y. However, x may not properly be marked frozen in x y; consider the
execution q = (a 11 b) I c Ha (011 b) IIc= (xli y)[x= (OIl b),y :=c], in which (Oil b) is not a
subterm of q.
We give a finitary definition for Froz(I) and Liq(I). It is an open problem whether this
finitary characterization is complete, but it seems good enough for many purposes. Let 
be a set of pairs (f, i) where ? fi,..., arity(f)t. Let [fj = ?i (f, i? C ??. The intent of
? is that, in the term f(x1, . . . , Xn), Xj is frozen iff (f, i? E ?.
We define the sets Liq?(I) and Froz?(I) by induction on univariate terms I as follows:
Liq?(x) = fx?
Frnz?(x) = 0
Liq?(f(I)) --H
Frnz?(f(I)) --H
U Liq?(Ii)
(UiEr[J] Vars(ii)) U (Ui?c'[f] Froz?(ti))
Vars(t) Liq?(I)
is always clear from context, so we omit the subscript and simply write Liq(I) and Froz(I).
A rule or ruloid is ?-winIerized if it treats frozen and liquid variables, as designated by
the set ?, properly. In a ruloid, frozen variables may be used without restriction, but liquid
variables may not be copied or tested during execution. Jn any event, children of a process
must be liquid, as they have certainly been executed. It suffices to place this restriction
on the rules for the language's operations; however, we will need to use this restriction on
ruloids, so we present the definition in foil generality.
Definition 5.1 A ruloid
Ui fxi ? Yiiil ? ? mit U trs(x?) = I3iJi C J?
i4t'
where each oii E Act?, is ?-winterized iff
1. I and I' are univariale, and each 0i5 E Act?;
2. fxi, . . . , XnJ = Vars(I), and Vars(I') C ?Yit , ynmnt and Vars(I) (fi Vars(I')W?
3. If Xi Yij is an anlecedeni and cib $ ?, and Yij E Vars(1'), Ihen Yij C Liq(t').
4Note that the variahies Xj cannot appear in tI. However we do allow ?transitions; if x7 ought to appear
in t' then the rule should have an antecedent X? y? and tI?at Yij appearing in t'.
12
4.
If Xj E Liq(1), then there is only exactly one hypothesis concerning r?; viz., efther
iflj = 1 and i ? I or rflj = 0 and i E I. Furthermore, if this hypoU?esis is a neutral
transition Xj y?i, and Yil E Vars(t'), then Yii E Liq(t').
A language  is ?-winterized if each n?le is ?-winterized. It is winterizable if it is ?-
winterized for some . `AJintenzabihty is obviously decidable, as (1) there are only a finite
number of candidates for , and (2) checking each of the finite number of rules against
Definition 5.1 is easy. The brute force algorithm is exponential. In Section A we give a
somewhat less naive 0(n2) algorithm for deciding winterizability.
Winterizability generalizes straightforward readiness; indeed, a language is ?-winterizable
iff it is a straightforward ready language. However, non-straigbtforward rules can be ?-
winterized if ? is nonempty. For example, consider the and while operations of (5). N%e
first must rewrite these rules in the format of Definition 5. 1:
If we set
then we have
x H y,r H Z
?? yj?!z
t
1			yi,x2			Y21,X2 H
t
while x1 do W2 H y21 ; while y? do y22
?= f(!,1?,(while,2)J
Froz(!x)			=			fxt			Liq(!x)			=
Ernz(y!z)			=			(zt			Liq(y?!z)			=			fyj
Eroz(while x1 do r2)			=			fx2t			Liq(while xl do x2)			=			fx1J
Froz(y21 while yi do y?2)			=			fy22?			Liq(y21 while y1 do Y22)			=			fy21,y1J
and we see that the rules for ! and while are winterized. Note that we have declared that
both arguments of ?;" are liquid, despite the fact that we know that its second argument is
frozen. Note that the rules are not ?`-winterized, where
as we have
?`--Hf(!. 1), (while, 2), (; ,2)?
Froz??(y21 ; while y1 do y22)			fyi, y22)
which violates part 3 of the definition, as y1 can be a partially executed term and thus must
be liquid.
This particular violation of winterization is safe the operational behavior of terms does
not depend on ?. However, if we modified the definition of `?;" in ?`?winterizable ways, e.g.
adding the ?`-winterized (though aberrant) rule
x1; x2 H W2 X2			(aberrant sematics)
then executed processes could be duplicated. in this aberrant systeni, if p = tp' Ht p?, then:
while p do 0 Ht 0 ; while p' do 0 4 (while p' do 0) (while p' do 0) (aberrant sematics)
13
which has duplicated p'. Similarly-structured examples show that ready semantics are not
necessarily respected in non-winterizable languages.
Some operations are not winterizable f:)r any ?; e.g., the operation g of (4). The r'ile
for split requires y to be liquid in g(y); however, the rule for g(y) requires it to be frozen.
Note that each rule alone is winterizable but no single  winterizes both simultaneously.
Similarly, the ?A operation of (3) isn't winterizable. The first rule forces x2 C Liq(x1 ?A x2);
but the second and third use r2 in ways that are only proper for frozen arguments.
The proof that winterizable languages respect ready semantics is rather long. I'irst, we
develop a ruloid lemma for languages in a weakened forin of the winterized format, showing
that if all rules are given in this format, so are all ruloids. Then we extend this to the full
?-winterized format, showing that if all the rules are ?-winterizcd, so are all the ruloids. ?Ve
then examine the structure of execution sequences, showing that tiie intended restrictions
on copying actually hold. NVe then give a characterization of all ready sets of o'(t) in terms
of information from the ready sets of a(x) for x E Vars(t). This shows that ready semantics
are adequate for all ?-winterized languages. ??e will conclude by showing that If  is a
winterizable language, then ready semantics are adequate and compositional for .
5.1 Ruloids for Winterizable Languages
We work with proto-wintenzabTh languages, in which the rules have the form:
`(xj%yijli1,...,n,51,...,n??ufrs(x?)B%iElJ			(6)
f(x1,cn) Thr
satisfying the parts of Definition 5.1 that do not niention frozen and liquid variables; that is:
1. f(xffi) and t' are univariate, and each a? C Ade;
2.			fxi, . . . ,			= Vars(t), and Vars(t') C (yii . . . ynmnt, and Vars(t) (f Vars(t').
The first technical result we show is a ruloid theoreni, showing that, all behavior of
univariate terms in proto-winterizable languages can be described by ruloids of the form (6).
Definition 5.2 A [t?r] test is a positiLe, null, or ready transition fr?rmuTh; that is, a hy-
pothesis to a proto-winterizabTh rule.
Notice that there is at most one ready transition antecedent rs() Bi for any vari-
able Xj. This does not lose generality. If there were two such antecedents with B? =
then they would have the same computational content (that is, both will be satisfied by
precisely the same instantiations). If there were two such antecedents with Bj $ B?, then
the rule would be unsatisfiable. Such ruVs appear in the construction, however. and we must
explicitly eliminate them.
Definition 5.3 Rules (or ruloids) of the form (6) except that they have two or more dift
ferent ready tests on the same variable are called impossible. ?`hen we are c mphasizing the
distinction, rules of the form (6) arc possible.
14
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. For the reader's sanity, we
annotate terms with their types.
We frequently need to choose one item from each element of a collection of sets.
Definition 5.4 Dependent Function Spaces. If & is a set, and % is a set for each
5 Ei &, we write (s : & i? T?) for the set of all fundions f wiTh dom(f) & and f(s) c Ts
for each 5 E &
For example, if & = fT1, T2,. . . , Tnt is a set of sets, (s : & H+ s) is the set of functions which
pick one element from each set in &; that is, ffldom(f) = & A f(T) ? 7)t
Definition 5.5 Set of Choices Jf & : set of set of A, define Choose(S) to be the sets of
ways of choosing one element 5 from each element of &. That is
Choose(S) = fran(e)Ie E (s : 5			s)? : set of set of A
For example,
Choose (fti, 2t, fa, b, ct?) = ff1, at, f1, bt, f1, ct, f2, at, f2, bt, f2, ct?
Lemma 5.6 Let  be any proto-winterizable language. Then for any term t and action
? Act u f&t, there exists a finite set of ruloids 1Z(I, e?) for 1 and a which is just right.
Proof: We will construct ??(t, c) by induction on t for all c simultaneously. The base cases
are easy: Let 9Z(x,a) = , and
x?y
k(t ?l =			x??forx?Vars(?)
where j is a vector of distinct variables the same length as and disjoint from xffi
For example, let us consider the term t = ?(z1 A z?), wiih the following rules,
contrived to illustrate ati aspects of the construction:
x1 H yii			x1			Y12, rs(xi) = fa,bt
:			?(x1) 4> yii + yi2
a			a
ZiHyi			.			2HY2			rs(z1)=g,rs(z2)=
yi			Pa2			--H			a			Pa3
Pal :			A z2 4>			A 2 H y?			ZI A 2 4> 0
P?i
rs(z1) = ?, rs(z2) = fbt
z1 A z2 H6 0
rs(z1) = ?, rs(z2) = fct
z1 A z2 4> 0
15
1 4> gi., rs(z2) = fct
Pb2			I A 2 4> 0
Pc2 :			1			y1, rs(z2) = fbt
z1 A 2 4> 0
Pcl :
For the induction step, consider t f(t1, . . . , tn). Let W(f, c) be the set of rules which
give f e-transitions.
We begin our running exampk by noting W(?,c)
For each rule p E W(f, c),
_ ?Xj%Yij?Ufrs(x,)BiliEI(fl))
4> u
we will construct a set of ruloids ?(t, c, fi) which explain the circumstances under which P
may give I a c-transition.
For each ij, we choose a way that the Xj ?? hypothesis can be satisfied. (?(p) is the
set of all such choice functions.
C(p) = (ii : (indices of %`s) I" ]Z(I?,a??) : index H ruloid
where we rename the variables in the ruloids g(ij) to be disjoint in each g E C(p). That is,
G(p) lists all the ways that all of the positive and null antecedents of p can be satisfied.
In this example,
= f[11 I' Pal, 12 i,' p?], [11 , Pa2, 12 pei, [11 ? Pa3- 12 ? peji
where Pc is the ?-transition rule for A 2
Pc : 1?Yci2HYc2
1 A z2 4> Ycl A Yc2
Ready tests are fairly complicated. Consider i c I(p); that is, an index i such that p
has a ready test antecedent rs(x,) = B?. For each a C Rj, we will construct R3(p, z-, a)
set of sets of ready tests on Vars(t?) stich that:
?W'?4> iff?1?ER3(p,i,a).a =1?.
and for each 6 ? we will construct a set R3(p,'i, 6) : set of set of ready test on Vars(i?)
such that
a ? Ii 4> ill' ?1? E R3(p, i, b).a 1= fi
To construct R?(p, i, a) for a C Bj, Jet Al be the set of sets of antecedents of ruloids for t?:
J?I' = fante(P')IF C ?((t', a)? : set of set of [t?rj tests
J3y induction, tj 4> iff some R E Al is satisfied. This makes Al is a good candidate for
R3(p, i, a), except that Al includes transitions x 4> y as well as ready tests. So, for ? a
test, define rl(y) : set of ready test
rt(x Hd y)			=			frs(x) = D?d E 1) C Actt
rI(x 4> y)			=			frs(x) = SIS c ActJ
rt(rs(x) = D) = frs(x) = DJ
16
Clearly, if y is a [+&r] test on x and dom(a) fx?, tben a can be extended to a' ? `? iff
a ? for some ? E 4(y).
Let p' E 9Z(t?, a). Choose(?rt(?) y C ante(?')?) : set of set of ready test is the set of ways
which guarantee that p' will fire. NVe collect these for all p':
R3(p,i,a) =
For example,
1?(zi A z2, a) =
Si =
52=
53 =
Choose(S1) =
Choose(S2)			=
Choose(S3)			=
l?3(P?,l,a) =
Similarly,
u Choose(?r1(y)Iy c ante(?')t) : set of set of ready test
p'Ei?(t a)
tpai, Pa2, Pa3t
tr!(y)I'? E ante(pai)i
?frs(z1) = (ai,rs(zi) = fa,bt,rs(zt) = (a, ci, rs(z1) = (a, 6, cit?
irt(y)Iy C ante(Pa2)i
tfrs(z?) = tai,rs(z2) = (a, 61, rs(z2) = (a,ct,rs(z2) = (a,6,cii?
(rt(?)Iy E ante(Pa3)i
= ?t, (rs(z?) =
(rs(zi) = (all, (rs(zi) = (a, bit,
(rs(z1) = (a,ctt,(rs(zi) = (a, 6, cit
(rs(z?) = (all, (rs(z?) = (a, bit,
(rs(z2) = (a, cii, (rs(z2) = (a,6,ctt
?(rs(z1) = ?, rs(z2) =
(rs(z1) = (aii,(rs(zi) = (a,bii,(rs(zi) = (a,cit,
(rs(z1) = (a,6,ctt(rs(z2) = (aii,(rs(?2) = (a, bit
(rs(z2) = (a, cit, (rs(z2) = (a, 6, cit,
(rs(zi) = ?, rs(z2) = ot
R3(P?, 1,6) =
(rs(z1) = (at, rs(z2) = (cit,
= (a, 61, rs(z2) = (cii,
(rs(?1) = (a,ct,rs(z2) = (cit,
(rs(zi) = (a, 6, ci, rs(z2) = (cit,
(rs(z1) = ?,rs(z2) =
The construction for 1?3(P, i, 6) for 6 ? ?? is somewhat trickier. for each ruloid p' c lQ(1?, 6),
we must find a reason (phrased as a ready test) why p' cannot fire. Now. P' cannot fire iff
some antecedent y of P' is false. `A'? thus define the set of denial? of y's, viz. the set of ready
tests ?` which, if they are satisfied, imply that y cannot be. Recall that rt(y) was the set
of all ready tests 4) which imply y; we define:
dn(y?) = (rs(r) = D 1) C Acti ri(y) : set of ready test
17
frs(z1) = fat,rs(zi) = oJ,.
frs(z1) = fat,rs(z2) = fctt
frs(z2)			fa,b,ct,rs(z2) = fa,a,cjt
where x is the source variable of y, which is therefore tl)e set of all ready tests wbich imply my.
Let
=			dn(y) : set of ready test
Choose(fR3(p i, d)Id c Actt)
fUSIS c R'2(p,i)t : set ofset
I??(p?,t,c) =
R'2(p,i)			=			: set ofset ofset of ready test
R2(p,i)			=			of ready test
For our running example,
A(pci) --H
A(pc2) --H
u
?Eante(p')
dn(rs(z1) = ?) Udn(rs(:2) = fct)
rs(z?)			=			fat,			rs(zi)			=			fbt,
rs(zi)			=			fa,ct,			rs(z1)			=			fb,ct.,
rs(z2)			=			fat,			rs(z2)			=			fbt,
rs(z2)			=			fa,ct			rs(z2)			=			fa,b,ct
dn(z1 ?a ??? ? dn(rs(z2) = fbt)
rs(r1)			=			?,			rs(z1)			=			f&t,
rs(z2)			=			?,			rs(z2)			=			fat,
rs(z2)			=			fa,ct,			rs(z2)			=			fb,ct,
rs(z1)			=			fct,			rs(zi)			= fa,bt,
rs(z1)			=			fa,b,ct,			rs(:2)			=
rs(r2)			=			fa,bt,			rs(z2)			= f6,Ct,
rs(z1)			=			fcj,			rs(?1) = fb,ct,
rs(z2)			=			fct,			rs(z2) = fa,ht,
rs(z2)			=			fa,b,ct
Thus, if dom(a) = frt, a = Y'p' for some Y'p' C A(p') iff a cannot be extended to
a' ? ante(p'). That is, a = yp" for some Y'p' C A(p') iff violates some antecedent of p'.
to construct R3(p, i, b) for b ? B?, we n?ist pick one y?' for each fi' in all possible ways:
P?(p, i, b) = Choose(?A(o')Ip' C ?(tj, b)t) : set ofset of ready test
In our example, R3(fl?,?,c) = Choose(fA(pi),A(p2)t) is U?e set of all two-
element sets with one element from A(pci) and one fron? A(pc2). There are too
many elements to list conveniently:
Finally, let
By the previous arguments, we have:
(?Il c R2(p, i).a ? I?) ? a ? rs(t?) = Bj
In the running example,
R'2(p?,1) = Choose(fR3(p?,i,a),i?3(p?,i,b),R3(p?,?l,c)t)
18
any
So,
R2(p?,1) =
We combine these:
?rs(zi) = fa?1,frs(ri) = fat,rs(z2) =
frs(z1) = (aJ, rs(z2) =
frs(zi) = ?a?J, ?rs(zi) = fat, rs(z?) = fctt,
frs(zi) = fat,rs(z2) = fctl
ffrs(z2) = (a, 6, ctt, frs(zi) = 0, rs(r2) Ot, frs(z2) = (a, 6, ctt?
(USIS ? R'2(p?,t)t
--H fct,
rs(z1) = faj,rs(z1) = (at,rs(z2) = fcJ,
rs(z1)			=			faj,rs(z2) =
rs(z1)			=			fat, rs(z1) = fat, rs(z2)
rs(z1)			=			fat, rs(z2) = fct
frs(z2) = fa,6,ct,rs(zi) = 0,rs(z2) = O,rs(z2) = fa,6,ctt
1?1i(p) = Choose(fR2(p, i)Ii E I(p)t) : set of set of set of ready test
R1(p) = fU SIS c R'1(p)t : set of set of ready test
to obtain a set of sets of ready tests such that:
c Ri(p).a WI?) ? a ? A rs(!?) =
t?I(p)
In the running erample, there is only one ready antecedent of p?, so I?i(p?) = I?2(fl?, 1).
Now, G(p) lists all possible ways of satisLying the transition forninla antecedents of p, and
J?i(p) lists all possible ways of satisfying the ready tests. We siniply need to put tbese
together. In the process, we must take care of properly substituting for variables Yi5 in the
target of p. So, for each g E G(p), let
g(i5) = ante(g(4)) : set of [+?r] test
= target(g(ij)) : term
For any g E G(p) and I? E Ri(p), let
Z(g,R) =			(U5g(ij))UB
t 4+ u[y4 :=
Note that u[y?5 := g(ij)] is univariate, as u is univanate arid the target variables in the
ruloids for the tj'5 were renamed apart.
There are far too many Z(g, I?) to show. Take g = [11 i, P,i.' 12 I, p?1; we give
Z(g,R) for the first two sets listed in R2(p?, J).
: fzi4+yi?u?z14+?e?,2?Ufrs(?1)=faj,rs(z2)=(Ct,rs(z2)=
I 4 Y1 + (y?i A y?)
19
P*2 :			Hay1?U?z1H?y??,2HEyE2?utrs(zi)fa?,rs(z2)fc??
t HC Yi t (y?i A
Define
c, p) fZ(g, 1t)lg E G(p), 1? E R1(p), and Z(g, 1?) is possibh?? : set of ruloid
which thus captures all the ways that I can make a c-transition via rule p. Note that excluding
impossible rules is safe; impossibie rules cannot contribute to the behavior of terms.
In our running exanip[e, P?i is impossible --H? 2 cannot have both ? and fct as
ready sets. Howevem P?2 is possible, and is a member of?(t, c,
Finally, we define
?(t, c)			U 9z(t, c, p) : set of ruloid
pEiV(,a?c)
which of course captures all ways that I can make a c-transition. t
Corollary 5.7 Let t be a univariatc term with variablcs x. Let a and at be substitutions of
processes for i such ??at for each x C f$), rs(a(x)) rs(a'(x)). Then rs(a(t)) rs(a'(t)).
Proof: The satisfiability of positive transition hypotheses of ruloids, x H? y, is determined
entirety by a(x)'s ability to do a baction; that is, whether or not b C rs(a(x)). Neu-
tral hypotheses x y are always satisiled. 1?eady hypotheses rs(r) R are satisfied ifi
rs(a(x)) = B. Thus, the satisfiability of a ruloid can he determined by the ready sets of the
a(x?)'s. The one-step behavior of 1 (that is, its ability to do an a or not) is given entirely by
ruloids. Hence the ready set of a(/) is determined entirely by the ready sets of the a(x?)'s;
the lemma follows trivially. ?
5.2 All Ruloids are Winterizable
""iTe develop some theory, ultimately showing that in a ?-winterizable language, all ruloids
are winterized.
Lemma 5.8 If x E Liq?1) andy E Liq(t2), ihen y E Liq(ti? := 12]).
Proof: Induction on Ii. If t1 is a variable, then it must be r, and the lemma is trivial. Other-
wise, t? = f(f7); we must have r E Vars(u?) for exactly one i, arid x E L1q(ii?) and (f, i) ?
Then 1i[x := 12] = f(iti, . . . , := 12]Un). By induction, we have y E Liq(u??i := 12]),
and hence y C LiqQi[r :1?]). ?
Lemma 5.9 If x C Liq(t) and x ? fy4 UVars(Th), Th(n r ? Liq(t[y':= Th]).
20
Proof: Trivial.
We claim that, if the rules are winterized, then the ruloids all terms I and actions a are
winterized as well.
Theorem 5.10 Suppose p ? ?(t, a) is a `ruThid in a ?-winterized language. Then p ?S
?-winterized.
Proof: We proceed by induction on terms; let I H? i? = cons(p). If I = .r or I = f(i) the
theorem is trivial. Otherwise,
I = f(11in).
We use the ruloid lemma construction, which explain how p is built. There is a rule p$ for f:
X.j H Yi5, ?Sr? = E
fi
j(x$1
which is the main rule used to construct p. For each ij, there is a ruloid Pij for an Qjj
transition of I?, and for each i E J tliereis a set R(i) of ready tests of Vars(I?). fly construction,
we have:
ante(p) = Uante(p?'j) U ? 11(i).
i5			jEl
We must show p winterized. It's trivial for I = x, and for I f(r). Otherwise, we know
p is winterized, and each Pij is as well.
The definition of "winterized" has two clauses about variables, which are satisfied by
construction. For clause 3 of Definition 5.1, consider an antecedent j y of p. Since
c Vars(I), and I is univariate, we have c Vars(I?) for some unique i. There is a single
antecedent x$j ??? Yij of p such that x g C ante(p?5). As Oij is winterized, we have
y ? Liq(ti??); and as p is wintenzed, we have Yij ? Liq('u%). Ilence, by Lemma 5.S, we have
y Ei Liq(u[y?5 := u??]); and by Lemrna 5.9, y C Liq(I') as desired.
For clause 4 of Definition 5.1, suppose that x E Liq(i). We must show that there is only
a single hypothesis concerning r, arid that if it is a null transition x y, that y C Liq(I').
If x E Liq(I), then we have x C Liq(I?) and (fr i) ? ?. So, Yj E Liq(f(r1,...  xn)). As p
is ?-winterized, there is exactly one autecedent fCA Xj.
If the antecedent for Xt in p is a transition X% Yij then Yij is liquid if present in r?. There
is a single antecedent of Pij concerning x, and this antecedent is the only one concerning x
in p as well.
Otherwise, the antecedent for ri in fi is a ready test. In this case, the construction gives
a single antecedeut (viz., a ready test) for r in R(fi, i), as p is possible.
Furthermore, the antecederit for r is a mill transition r y if either:
The transition from Xj is a null transition. In this case, `u? is t?? with the variables
renamed to y's. In particular, as r C Liq(I?5), we have y E Liq(ri?5). As Y'ij is liquid in
u, Lemmas 5.8 and 5.9 imply that y C Liq(I').
o+ The transition from r? is positive, and the transition in p? is null and hence y E Liq(i??5).
In this case, by Lemmas 5.8 arid 5.9, we know that g?? is liquid in I' as desired.
Thus, we have shown that p is -winterized. t
21
5.3 Winterization Forbids Copying and Polling
\?\?? give some formalism
example, Jet p and q be
In this section, we show the effects of our bookkeeping discipline.
allowing us to trace the execution of processes in contexts. For
processes, and consider a multi-step execution
whi1epdoq?>q' ;whilep'doq
The methods of this section will JIow us to say that, for example, p' is a descendant of p,
q'is a descendant of q, and q gets copied. This machinery formalizes the informai intent of
winterization presented at the start of this section.
It is convenient to investigate possible sequences of transitions between terms. Suppose
we have a (finite or infinite) sequence of transitions via winterized ruloids:
z=(t0?a0t1D>??t2,..)
where the transition 1i ? 1i+1 is an instance of ruloid p?. Suppose that the sets Vars(t?) are
all disjoint, and Vars(p?) are all as disjoint as possible; that is, if i ? j then
I --H it 1
Vars(p?) n Vars(p5)			1ars(t?) ?x31?, ? otherwi SC
?Ve say that x3? is frozen (resp. liquid) if it is frozen (resp. liquid) in tj. Note that the upper
index of a variable is unique; if k # i then r3? ? Vars(t?).
Definition 5.11 We define the relation r? 4 r?,, intended to mean That the variable w',5 ?n
Ij evolves via the string of actions 5 to the variable in I?'. (Strictly,, this depends on as
well)
o+ x? a r
3			3
o+ Ixt. 4 x?, and			?? x?11			E aflte(pji)? then			a y?11
3			3			ii			3			3			3
where sa is the concatenation of the string s and the 0- or I-eThment string a.
Lemma 5.12 Let G be the graph whose nodes are the variables x3?, with an edge from x3t, to
%?4 if i' it land ?a.x3? 4 4'i. Then G is a forest,
Proof: Trivial from the definition and the fact that a target variable = Yij appears in
only one antecedent of any ruloid.
Definition 5.13
v ___
o+ x? is initial iffor some Iv, we have Y50 a'
0 x3? is final if there is no x3%1 and a with ?;; 4
22
o+ x3??is ready tested if pi has a hypothesis rs$..?%)
o+ forks if there are distinct variables z1, z2 and single actions a1, a2 ? uch that:
1.			a1
Xj 0 z1 and X5			Z2
2.			neither z1			z2 nor z2			z1
Lemma 5.14 If p is a winterized ruTh id with hypothesis ;r y, and X is hquid in the source
of p, then y is liquid in the target of p f it appears at all.
Pro of: If a E Act, this follows from part 3 of Definition 5.1; otherwise, it follows from part
4. t
Corollary 5.15 If r? is liquid in Ii and Xj1 4 ???; then x3?11 is liquid in tj'.
Lemma 5.16 If ?31: is frozen, then r?1 ?? initial.
Proof: By induction on i. Let Xj? be frozen. If 0 then rj% is trivially initial. Otherwise,
we have x),?1 4 x3? for some k. x?k?' must be frozen; if it were liquid, l?emnia 5.14 would
require x3t to be liquid. By induction, X?k?' must be initial: x0? 4 xt71.
Furthermore, a = ?; if a ? ?, then Definition 5.1 part 3 would require ? to be liquid.
Thus, we have X0t 4 x),?1 4 Yj$ whence is initial.
Lemma 5.17
1. If r? is ready tested, then it is eiThei initial orjinal.
2. If Xj? forks, then it is initial.
Proof:
1.
2.
Suppose x3? is ready tested, but is not initial. By Lemma 5.16, r3? is liquid. By
Definition 5.1 part 4, no hypothesis of p? other than the ready test mentions %t. Hence,
x? is finat.
We proceed by contradiction. Suppose that is not initial. By Lemma5.16, Xj? cannot
be frozen (or it would be initial). We show that there is at most one r3i; for each i' > i
such that x3? a' x3t,., This is clearly true for i' = i. If it is true f:?r some i', then by
ii
Definition 5.1 part 4, there is at most one antecedent H 1 of Pi', and at thus at
most one variable with ?; 4 ?;;+1. Thus, all the descendants of rt; are linearly
ordered by ?. In particular, x3t. does not fork. Thus, if r3? forks, it must be frozen; and
hence is initial as desired.
23
5.4 ?-winterized languages respect ready semantics
Let I be any univariate term, with Vars(t) f?ThJ. Let (s ? X) be any ready pair. ?Ve
construct necessary and sufficient conditions on a(x?) under which (s ? X) c R?a(t)]. ?Ve
phrase the construction in language that resembles rules and ruloids. The antecedents we
require --H that is, the conditions on the a(r,)'s are Thng transition formulas:
o+ x y, intended to mean that x performs the string of actions 5 to get to y
o+ x ? 13 intended to mean that x can perform the string of actions s and then has 13
as a ready set; that is, that (s ? 13) E R?x?.
A long ruloid is a rule of the form
13
t4t'
where I and 1' are univariate, H is a set of long transition formulas, the x's all appear in I,
and the variables appearing in I' are all y's.
Rather predictably, we define:
a			r 4 y			? a(?) 4 a(y)
a			x			13 ? (s ? 13) c R?a(x)?
Definition 5.18 We say that a long ruloid is possible if There is at Tnost one antecedent
x 13 for any variable r.
Note that a long ruloid with hypotheses x ? fb, c?. T ? fe, ft is possible; the processes
of Figure 3 have these ready pairs.
Lemma 5.19 (Long Ruloid Len?ma) For any univariate term I and string 5 ofactions,
there is a set 1Z(I,s) oflong ruThijs which isjust rightforI and 5.
Proof: Define 1Z(t,a) to be the ruloid set oft for a with ready hypotheses rs(x) = 13 replaced
by the (semantically equivalent) long ready hypotheses r ? 13.
Ruloids can be concatenated in a fairly obvious way, if the target of the ?rst is the source
of the second. Define Pa Pa as follows. Let fI? and Ha be the sets of hypotheses of Pa and
Pa; and I 4 t' = source(pa) and I' 4 I" = target(pa). Let:
H1			=
H2			=			fr
Th?			=
=			fx
H			=			H1
HUV zI(x 4 y) c Ha, (y 4 E Ha?
ffl?uv 13 4 y) c -Ha, (y ? 13) E Ha?
4 yI(r 4 y) E Ha, no hypothesis of Ha mentions
?13I$?D CHa?
u H2 u H3 u H4
24
Then we define Ps Pa --H H
Let
1Z(t, sa) = fP5 Pa I Ps E 1z(i, 5), Pa E 1?(target(?5), a), Ps Pa is possil)le?
where without loss of generality the variables in Ps and Pa are renamed to be as disjoirit as
possible: Vars(P5) n Vars(Pa) = Vars(target(?5)).
The requirement that all elements of ?(t, a) are possible (that is, have no more than one
ready test for any variable) is essential for soundness. Otherwise, we could take rules
rHy			rsy=a,rsy=
f(x)4g(y)			g(?)4O
Note that the rule for 9(y) is impossible; 9(p) can never take a step. Thus f(aa t ab) `` aO.
However, without the possibility requiren?nt, the rules compose to
a			a
r 1 tat,i ? tbt
f(x)?O
which long ruloid would mean that j(aa + ab) , aa, which is not true.
Completeness of the Long Ruloids Long ruloids are equivalent to ordinary ones for
Is < 1. Suppose that a(t) = p and p 4 q 4 `r. By induction, we know that there exists a
long ruloid Ps = and an extension a' of a such that a' ? H5 and a'(t 4 t') = p 4 q.
By the ruloid lemma (renaming target variables if necessary) there exists a ruloid Pa = ,1ffi??1
and an extension a" of a' such that a" ? Ha and a"(t' 4 t") = q 4 r. Note that a" ? Hs.
Let Psa = Ps Pa, and H = ante(Psa).
The fact that Psa is possible follows from the fact that the transition happens. Consider
any antecedent x 4i Bin Pas. By construction, ? ? H2UH4. So, either ? 4 y c H5
and			?			C Ha, or			4i			E Hs. As a" = Hs U Ha, we have &`(x) W x ? B, and
hence rs(a"(x)) = B. Thus, all such antecedents have the same set ?; which is to say, there
is only one and the rule is possible.
Clearly a"(I %? 1") = p r. N?'e must show a" J= JI. We check each element of H.
1. If HUV z) E H1, then there is a y such that 4 y) E PI5 and 4 z) E Ha. As
a" ? H5, we have &`(r) 4 a"(y); and as a" ?= Ha, we have a"(y) 4 a"(z). Hence
a" ? r
2.			If			44			C H2 then we have			4 y) E JI8 and			44 Ii E `Ia for some variable
y.			We have a"(x) 4 a"(y), and a' ? y 44 B, so a" ?			1 13 as desired.
3.			If			4			E 113, then it is in Ils as well, and we have a"(r) 4 a"(y) as desired.
4.			If			44			E H4, then it is in Ils as well, arid we have a"(x) 44 B as desired.
So any transition is supported by a long ruloid.
25
Soundness of the Long Ruloids Let Psa --H ,H?, ?,)ra?11 --H Ps Pa be a long ruloid
in ?(1, sa). Suppose that a H. ??\?Te must show a(i) 4 a(I").
?Ve construct an extension ?? of a such that a' ?= H5 and a' ? Ha. \?\?Te will then have
a(t) = a'(I) 4 a'(t') 4 a'(t") = a(I"), and hence a(I) 4 a(I") as desired.
So, we must define a' on each variable y E Vars(i'). By construdiori,
Vars(I') rh (Var#[) u Vars(t")).
Consider a y E Vars(1'). There is a unique hypothesis (x 4 C H? concerning y. However,
y may participate in many antecedents of Psa
For each such y, let we will compute Ca, the set of values that a'(y) must have. NVe show
that Ca = 1, and hence that a' is well-defined.
1.
For each z with			4			C Ha, we have
a			x			z. For each such z, choose a q such that
the set of such q?'s.
E iii. As a ?--H ?i, we have
a(r) 4 q 4 a(z). Let C1 be
2. For each y ? B? Ha, we have a x ? I?. For each such v, H, choose a ?aB such
that a(.x) 4 ?vB and (v ? B) E R?vb?. Let C2 he tlie set of all (IvB `5.
3. If no hypothesis of Ha mentions y, then x 4 y E ff3. so y c dom(a). tn this case let
C3 = fa(y)J; otherwise, let C3 =
Finally, let Ca = Ci U C2 u C3. Note that Ca # ? if C1 and C2 are both empty, then
there are no hypotheses concerning y in Ha and hence C3 ?
Let be the sequence of ruloids enabling the transitions 4 1' 4 t".
??e claim that Ci' = 1. Clearly if Ci U C2 = e then C?I = C3 = i. Otherwise,
C3 = 0; suppose that Ci' > t. There must be two hypotheses in 1Ia concerning y:
1. If both are positive transitions, y i and y 2, then y forks. Hence, by Lemma5.t7
part 2, y must be initial in hence ?L = , arid each q and ?vB is simply a(x).
2. If the two hypotheses are y 4 arid rs(y) = R. By Lemma 5.t7 part 2, y must be
either initial or final. However, as there is a transition y 4 z, y cannot be final. Hence
y is initial; so t' = &. As before, all q's are a(r)
3.
The distinct transition fo??ulae are two ready tests. However, by the construction
which insists that all rtiloids be possible, all ready tests on y must be the same; this
case does not arise.
Hence, Cal = 1. Define a' to be:
a(z) z C dom(a)
=			q			z ? Vars(t') and q is the unique element of Cffi
Clearly, a' ? H5 and a' ? Ha. Hence, we have a'(I) 4 a'(i') 4 a"(i"), which is to say,
a(I) 4 a(t") as desired. ?
We are finally in a position to show that ready semantics are adequate for -winterized
26
languages.
Theorem 5.20 Let  be a ?-w?nierized [anguage and t a nnivar?ate -te?m. Jf a,a'
Vars(t) H Procs are substitutions wi?i R?a(x)? = R?a(x')?, then R?a(i)] =
Proof: Let (s ? B) c R?a(t)?; that is, there is a process q such that a(t) 4 q and rs(q)
Ii
By Lemma 5.19, there is a long riiloid p = t?u enabling this transition; that is, there is an
extension a of a such that a = H and a(u) =
Consider y ? Vars(u). There is a unique antecedent r 4 j' in ante (p) concerning this y,
and as a ? H, there is a process a(y) such that a(x) 4 a(y). By ready equivalence of a(x)
and a'(x), there are processes a'(y) such that a'(x) 4 a'(y) and
rs(a'(y)) = rs(a(y)).
(7)
Consider an antecedent x i B. ?Ve have (s ? c R?a(?)?, arid hence (5 ? I?) E R?&()?
as well. Hence, a' = ante(p), and so we have a'(t) 4 a`(v). By Lemnia 5.7 and (7), we have
rs(a(u)) = rs(a'(u)). Hence (s ? B) c R?a(t)? as desired.
5.5 Further Considerations
There are, of course, non-winterizabie operations which respect ready semantics. For exam-
ple, choose an action a. The operation ? given by
y			r
?x 4 (?x) II (*y)			? 4 ?x,
is not winterizable, as the first rule copies  (forcing (`, 1) E ?), and uses tlie child y (forcing
(`, t? ? ?). However, ?p H aW, a process which siniply performs a's forever, for every p;
and thus they are equivalent in every GSOS language. Up to semantic equivalence, ?p does
not depend on p, and hence trivially respects ready semantics. Note that tlie step-by-step
behavior of * including the descendants of ?p'- does depend in a fairly complex way
on
Similarly, consider the operation A, defined by
?y			rsy,6=B
4 Vy			Vy H
where B ranges over all sets of actions, and b ranges over all elements of B. For example,
A(a.(b + c)) does an a, then perfornis b and c actions forever. The behavior of Ap is
determined by p's ready semantics. However, A is riot winterizable, as the second rule leaves
y around despite having ready tested it.
It would be easy enough to extend the definition of winterization to allow arguments to
be repeatedly ready tested, as long as they are never executed. However, this would not
increase the class of definable operations. V could be equally defined by the rules:
rs(y) = B
Vx VB
VB VB
27
where B and b have the same range as before. That is, if operations have arguments available
for repeated ready testing but nothing else, it suffices to ready test tlie arguments once and
record that information.
Finally, some languages are not winterizabie for utterly stupid reasons. For example, the
operation ? defined by:
X H y, x
2+ x y r y
The rule is clearly not winterizable, as y must be liquid and it is copied. However, the rule
is not executable, as the antecedent requires x to both perfi?rm and not perform an a, and
hence ?(x) H 0 The presence of such %unk" rules obviously does riot effect the semantics
of the language. In [1] we give an algorithrri for eliminating junk rules.
We know of no systematic finite extensions of the winterized rule format which increase
their expressive power. It is an open question whether such a thing exists; indeed, finding a
formal definition of a "systematic extension" is a largely unexplored matter.
6 Equational Semantics
In this section, we argue that any winterizable language can be given a complete equational
axiom system with one infinitary induction principle, which is sound and coniplete for ready
semantics. The general method for doing this is described in [2], arid uses results of [4].
Reproducing the results of those papers would be long and unedif?ying; we simply describe
the necessary connective tissue.
The methods of [2] show how to give a complete axiom sytem for strong bisirnulation of
closed processes for an arbitrary GSOS language. The method requires the introduction of
auxiliary operations into the language [16], e.g., tlie operator generated for interleaving II is
the left-merge [5]. The process pttq behaves like p II q, except that p will necessarily take tlie
first step. For each a, left merge has a rule:
r
x[Ly 4> x' y
(8)
The methods of [2] automatically generate auxiliary operations and axioms for strong
bisimulation. The same operations and axioms, phis some suitable axioms explaining the
equivalence on finite trees, will characterize any other equivalence relation --H- assuming that
they make sense at all. The operations generated by [2] are GSOS operation, and thus
respect strong bisimulation and ready simulation, but there is no a priori reason why they
should respect other equivalences. Indeed, ?f does not respect some equivalences --H weak
bisimulation in particular.
?Iore generally, it is not clear that the auxiliary operations introduced by [2] fit any rule
format other than GSOS. The following iemrria shows that, for ready languages, they do:
Lemma 6.1 Let  be a straightforward (resp. winierizabTh) r?-;ady language. Let ` be ??e
auxiliary operations and their rules introduced by [2j. Then  u ` is straightt'orward (resp.
w?nterizable).
28
Proof: [2] requires the introdudion of some reasonably standard operations, including +
and prefixing, and to handle negative rules (and rules with ready tests) a family of operations
?B with operations
r4y
a
x?f3 4y
These operations are all straightforward winterizable.
The constructions of [2] are fairly intricate, and we refer the reader to [2, 3] for the details.
That method categorizes operations in ways largely independent independent of the classes
used in this paper. However, as the work of this paper can all be phrased within the GSOS
framework and [2] applies to all GS()S languages, [2] can be applied to a straightforward or
winterizable language to give a complete axiom system for strong bisimulation. There are
two cases in which auxiliary operators must be introduced. ?Ve show that, if the original
language is straightforward or winterized, the extended language will be as well.
The first case, which axiomatizes the so-called "smooth and non-distinctive" operations
(like II) in terms of simpler "smooth and distinctive" operations of the same arity (like ?f),
introduces new operations whose rules aniount to a subset of the rules of existing operations.
For example, the rules for [11 are essentially half the rules for j, with the function symbol in the
sources changed from to L It is clear that changing the function symbol in a straightforward
rule results in a straightforward rule. if the original rule was ?-winterized, define ?` to be
 extended so that the auxiliary operators have the same frozen arguments as tfie origin?
ones they were derived from; then the new rules are easily seen to be ?`-winterized.
The second case axiomatizes the non-smooth operations Axiomatizing a non-smooth
operation, say J(x), requires the introduction of a new operation which behaves like f except
that it has more arguments. For example, if f bas the rule
then [2] introduces
a			b
x H y, x
f(r) 4 f(y)
a			b
ri H y, x2
J'(xi,x2) 4 f(:q)
and an axiom f(r) f'(x, r). As before, if the rules for f are straightforward, then so
are the rules for f'. Similarly, if the rules for f are ?-winterized, then the rules for f' are
?`-winterized where ?` declares that arguments of f' corresponding to frozen arguments of
J are frozen. ?
This gives us a straightforward or winterizable ready language with a complete equational
axiom system for bisimulation. We can use the n?ethods of [4] to add equations expressing
ready equivalence as a quotient of bisimulation. In our setting, we need the single additional
equation:
a(br + t?) + a(by + ?)) = a(6x + by + u) + a(br + by +?;)
29
(9)
7 Full Abstraction
In general, a semantic equivalence is fully abstract with respect to a language  and a
notion of observable behavior iff two processes are semantically equivalent precisely when
they produce the same observations in all contexts. In process algebras, there are several
reasonable notions of observation. The coarsest notion is partial traces; that is, the set of
strings s of actions such that p HS.5
A few straightforward operations suWce to explain the differences between non-ready-
equivalent processes. NVe give a set of operations, FARSE (Full Abstraction for Ready
SEmantics), which make winterizable languages fully abstract for ready semantics. Indeed,
any winterizable language may be extended by FARSE to give a fully abstract language. Y\?e
must emphasize that the operations in FARSE are completely contrived. They bear some
vague resemblance to polling operations, but are clearly tuned towards full abstraction.
FARSE is the collection of operations and rules including the standard CCS operators of
0, prefixing, and ? and their rules, and three auxiliary operators tst, act, and red with the
rules below. ?7e leave the action alphabet unspecified, but insist that there be at least two
actions.
Fix two distinct actions c and d. The CCS operations are given their ordinary semantics.
The new operations are given behavior by:
y			.r4>y
tst(r,r') H0 act(y,x')			tst(r,;c') H0 red(y,x')
xy,H?y'			rs(x)B,rs(j?)=I;
act(x,r) HC tst(y,y')			red(x,x') HC 0
where a ranges over all actions, and 1? over all sets of actions. tst(Y??, p) gives T the ability
to coordinate actions and test final ready sets of p. Note that the FARSE operations are
straightforward ready operations, and indeed mQy be added disjointly to any straightforward
or winterizable language and the result will still be winterizable.
Theorem 7.1 Let  be any winterizable language inctudiag F4i?5F as a sublanguage. Then
ready semantics are fully abstract for partial traces for iC.
Proof: Ready semantics are adequate for , as  is winterized. It suffices to show that, if
R[[p? # R[q?, then there is a context C'[x] and trace r such that r is a trace of precisely one
of C\J)j and C[q].
If R?[p? # R?q?, then there is some ready pair (s ? X') in one and not in the other. ?Vithout
loss of generality, we assume (s ? X) c R?? Rj[q?. Let a1, a2 be the characters of
5 in order that is 5 ....... a?, and
Ts,x = c.a?.c.a2. ... .c.an.d.(Zt?x b.O)
5Partial traces are the philosophically easiest notion of ohservation to justify: if one can ohserve anything
ahout processes, one can surely ohserve their partial traces. Niore powerful notions of ohservation (e. g.,
completed traces, infinite traces, and so forth) are nut unreasonahle., hut are less unquestionahle than partial
traces.
30
We claim tst(Ts,x,p) c2%+2 iff (s ? X) C R??. Suppose tst(Ts..x,p) c2?2 By inspecting
the rules, we see that the only possible computations have the form
tst(Ts,x,p) 4 act(T?x,p)
4 tSt(To2?anx,P2)
4			tSt(d.(?bEx b.O),pn)
4			red((Z??x b.O),p?)
4o
where P P2 P3? p? and rs(p?) X. Thus, (? ? X) is a ready pair of p. Similarly,
if (r ? X) is a ready pair of p, that computation will be possible and thus c2?31+2 will be a
trace of tst(Ts,x,p).
So, the context C[x] = tst(Ts?x,?) distinguishes p from q hy partial traces; we have
C[p] c2IsI+2 , but ?(c[qi c2IsI+2 Hence  is frilly abstract as desired.
Clearly the same operations will make  fully abstract for more powerful notions of ob-
servation, such as completed traces. Note that any straightforward or winterizable language
is trivially fully abstract for observing ready pairs.
These operations are fully abstract for ready equivalence and partial traces, observing
partial traces. This cannot be regarded as a satisfactory solution to the full abstraction
problem, as the new operations are introduced siniply to test ready sets and are of dubious
computational content or use. We are not aware of any "natural" process algebra for which
ready equivalence is fully abstract. This is in sharp contrast to failure semantics, which are
fully abstract in standard process algebras.
8 Conclusion
We have given rule formats such that all languages defined in them respect ready equivalence,
such that complete equational axiom systems (with one induction principle) can be derived
from the rules. These rule formats are broad enough to cover most process algebras appearing
in practice.
Similar results hold for other linear-time process equivalences. The cleanest such result
concerns ready irace equivalence [18, 121, which are traces annotated with ready sets at ev-
ery point. Ready traces are appropriate (indeed, fully abstract) for the polling operation
of Section 3.1, broadcast operations, arid so forth. i\s with ready equivalence, ready trace
equivalence cannot tolerate general copying, but is consistent with winterizable copying; nil-
like ready equivalence, ready trace equivalence admits polling. If we remove the restrictions
designed to prevent polling from the rules, the resulting formats work for ready trace equiv-
alences. If we replace (9) by a suitable equational description of ready trace equivalence, the
results of Section 6 hold mutatis mutandis as well.
31
8.1 Open Problems
The main open question, of course, is finding a rule format for failure equivalence. NVhile we
have a rule format for failures, it involves an infinitary closure condition which we do not
know to be decidable from the rules alone, and thus do not consider it satisfactory. NVe and
our students are investigating the matter further.
In [7] we argued that GSOS format is a niaximal format for bisimulation. That argument
was informal, based on a series of examples showing that no simply-defined superclass of
GSOS rules necessarily behave properly. For lormats for coarser equivalences, a more precise
theorem should be possible. ?Ve conjecture that aThy language defined by non-winterizable
ready rules and satisfying some straightforward nontriviality conditions does not respect
ready equivalence.
Theorem 4.2 shows that all straightforward functions are pointwise defined. It might be
of some value to characterize the set of functions ? which pointwise define straightforward
functions f. There is doubtless a class of ?`s which `ought" to pointwise define R[f?'s
probably those satisfying some monotonicity, continuity, and computability properties --H and
it would be interesting to know if there are any ?`s which should define J's and don't.
A Algorithm for deciding winterizability
?7e give a polynomial time algoritlim which takes a proto-winterized language ? and returns
either a ? which winterizes it, or signals the language is riot winterizable.
var CL /* Set of (f, i) pairs that m'ist not be  ?/
CF			/* Set of (f, i? pairs that must be in ?
proc
melt (x,1)
1 Add (f, i) pairs to CL to make x liquid in I /
if x ? Vars(1) then return
if I has the form J(j)
then let i be the unique i such that .r E Vars(I?)
CL u= (f,i)
melt(x, Ij)
end melt
Ante-Count /? Variables with other than one antecedent must be frozen. ?/
for p C rules()
/? Count hypotheses concerning each variable ?/
var nhyp : array [Vars(p)] of int 0
for ? E ante(p)
nhyp[source variable of `?] += 1
for ?? E source variables of p
if nhyp [xj] $ 1
then CF U (f,i)
:32
Melt-Kids/* Proper descendants must be marked liquid ?/
for all positive antecedents r y of all rules p
melt(y, target(p))
Liquid-Copy /? Niake sure that all copies of liquid variables are marked liquid ?/
for p E rules()
f			function symbol of p
for all null transitions Xj H y of p
if (f,i) ? CF
then melt(y, target(p))
/* Compute the answer
if CL rh CF
then return CF
else fail
A.1 Correctness
Lemma A.1 The sets CL and CF are nondecr??siny. That is, if (f, i) E CL at any point
?n the algorill?m `s execution,, then (f, i? c CL from then on, and sin?ila#q for CF
Proof: The only assignments to CL and CF add elenients.
Len?ma A.2 Suppose that melt(x, -1) is called at some point in the pogram's execution,
uhere x C Vars(t), and the program returns successf'illy with a sct ?. Then x ? Liq?(t).
Proof: We proceed by induction on the size of t. If t is a variable, then the assurnption that
x E Vars(t) forces t = x, and so = fxt by de?nition. Otherwise, I = f(t), and as t is
univariate, there is a unique i such that x E Vars(t?). The program adds (f, i? to CL, and by
Lemma A.i, it remains there forever. The program then calls melt (x, tj) arid by induction
we have x ? Liq?(t?). As (f, i) c CL and the program returns successfully, we must have
CL rh CF, hence (f, i) ? ?. By the definition of Liq?(t), this rneans that x E Liq?(t) as
desired.
Lemma A.3 Suppose that p be a rule of , and the algoriihrn returnsF on input . Suppose
that Xj y?? is an antecedent of p,. andy,?' c Vars(t) where I = target(p). Then y,5 E Liq?(t).
Proof: The Melt-Kids loop calls melt(y5, t) for all such y?5 arid t. By Lemma A.2,
this means that y?5 c Liq?(t) as desired. ?
Lemma A.4 Let p be a rule of , and f(xW) = source(p), and suppose that the atgorithm
returns  on input . Suppose that x? E Liq?(f(x')). Then there is only a single hypothes?s
concerning Xj ?n
33
Proof: ?7e proceed by contradiction. Suppose that there arc zero or more than one hy-
potheses concerning Xj in p. The first subloop of Ante-Count counts the number of
hypotheses concerning the variables. The second subloop checks this count; if it is some-
thing other than one, then (f, i? is added to ?F, declaring Xj frozen. ?Te have (f, i) E ?;
thus Xj is not liquid in f(x?, as desired. ?
Lemma A.5 Let p be a rule of , and f(x) = source(p) and t = target(p), and suppose that
the algorithm returns ? on input . Suppose further Ihat there is a single antecedent con-
cerning Xj? and that antecedent has the form X? A> y with Xj E Liq?(f(rffi)). Then y ? Liq?(t).
Proof: Note that after loop Ante-Count finishes, no (f, i\) pairs are added to ?F. That
loop computes all the things which the rules insist must be frozen; the rest of the code is
simply making sure that things which must be liquid are not also required to be frozen.
Thus, if (f, i) ? EF in the if command in loop Liquid-Copy, then (f, i) ?
Suppose p is a rule with consequent f(r) A> t, and r? A> y is an antecedent with
Xj E Liq?(f(r?). NVe have (f, i) ? ?, and hence (f, i? ? EF. So, the loop Liquid-Copy
calls melt(y, target(p)). By Lemma A.2, y E Liq?(t) as desired.
Lemma A.6 Suppose that  is a proto-winteHzable language, and the aigorithm succeeds
with result ?. Then  is ?-winterizable.
Proof: Clauses 1 and 2 of the definition of winterizability follow from proto-wintenzability.
Clause 3 follows from Lemma A.3; clause 4 follows from Lemma A.4 and Lemma A.5. ?
Lemma A.7 Suppose  is a proto-wintrrizabTh language, and the algorithni fails on it. Then
 is not winterizable.
Proof:
Assume for contradiction that  is ?-winterizahle for some ? Tbe algorithm fails iff
EF n EL ? ?. Let (f, i) E EF n EL. As (f, i? c EF, there is a nih Pi for f with other
than one antecedents concerning the i'tb argument Xj. Thus.,  could only be ?`-winterized
if (f, i') ? ?`. ilence, (f, i? E ?.
There are two ways that (L i? could he added to EL. First, in tlie loop Melt-Kids,
from a rule P2 with an antecedent x A> y and target t, where the call melt (y, t) adds (f, i?
to EL. From the presence of the antecedent, we know that to satisfy part 3 of the definition
of winterized, we must have y E Liq?(t). As melt adds (f, i) to EL, there is a subterm
u = f(u) of t with y c Vars(u?) being the unique occurrence of ij in t. By tlie previous
paragraph, we know that (f, i? E ?, and hence y c Froz?(f(Th)); it is straightforward to see
that y Ei Eroz?(t) as well, violating clause 3 of the definition of ?-wintenzed. So, if (f, i?
was added by Melt-Kids, then  is not ?-wintenzed, which is a contradiction.
Otherwise, (f, i? was added to EL by a call to melt in the loop Liquid-Copy. In
this case, there is a rule p with an antecedent rj A> y, consequent g(.?') A> t, and (g,5) ? EF,
such that the call melt (y, I) adds (f, i? to EL. As before, there is a subterm u =
with y ? Vars(u?) being the unique occurrence of y in t. Again, (f, i? E ?, and hence
34
y ? Eroz?(f(u?) and thus y C Ernz?(t)., violating clause 4 of the definition of ??winterized.
So, if (f, i? was added by Liquid-Copy, then  is riot ?-wintenzed, also a contradiction.
Hence,  is not -winterizable for any , arid thus not winterizable. t
A.2 Complexity
The algorithm as given is not complete; iri melt, the algorithm must find the unique i such
that x C Vars(t?). Given this, the running time of the algorithm is easily computed.
A.2.1 Initialization
?Ve give an algorithm which does this in coristant time with 0(n2) preprocessing. Note that
melt (r ,t) is only called when I is a subterrri (riot necessarily proper) of the target of a nile
of . ?re represent terms as abstract syntax trees with space for extra information at the
nodes: at each node u f(Th), there is a table du indexed by variables, so that duW? i if
x E Vars(u?) and x is not present in du if x ? Vars(r?). This is possible because the terms
appearing in  are univariate.
The tables can be filled in by a straightlorward bottom-up walk over the tree:
proc fill(I) returns set of variables
/? Returns the set ofvariables in I */
var S			set of variables /? to accumulate the return value ?/
V : set of variables
if I is a variable x then return fx?
else I has the form f(i1,...,trn)
3 :--H--H
for i := 1 to m
V := fill(Ij)
for x E V do atWi
3 u-- V
return 3
end fill
/? Initialize all the tables */
for each rule p do fill(target(p))
Melt(x,I) will only be called with I a node of a tree of a target of a rule. There are 0(n)
such nodes to be processed. Fill is cled once for each node. Each visit does m unions,
where in is the arity of f. This could he expensive in general; however, the sets V are all
disjoint, and could be represented by head-and-tail pointers to linked lists; so each unions
can be done in constant time, for a total of 0(n) time spent on set manipulation. Each
visit sets in table elements the list representation is well-suited for the for x C V loop
taking 0(m) = 0(n) time. Thus, the time spent at a node is 0(n), for a total initialization
time of 0(n2)
35
A.2.2 Running time
The procedure melt does no more than ?/? rccursive calls. Given the representation discussed
in Section A.2.1, each of the operations that melt does in particular, the r ? Vars(t) check
and calculation of i require only a single constant-time table lookup. Thus, a single call
to melt takes 0(n) time.
The first inner loop of Ante-Count is executed once per antecedent and takes unit
time, for a cost of 0(n). The second loop is executed once per source variable, and hence
costs 0(n). The total cost is 0(n) set insertions. N?\Te might as well represent EF by a table,
giving constant time lookup.
The body of Melt-Kids is executed once per positive antecedent, which is to say
0(n) times. The body is a call to melt. Thus, the total cost of Melt-Kids is 0(n2).
Finally, the inner loop of Liquid-Copy is executed for every null transition; there
are 0(n) null transitions. Each iteration checks (f,i) c ?F, which is constant-time with
the table representation. In the worst case, it does a call to melt, costing 0(n), on each
iteration. Thus Liquid-Copy is 0(n2).
Finally, checking that two sets do not intersect is easily done in 0(n2) time. Thus, the
entire algorithm takes 0(n2) time as desired.
B Acknowledgements
I would like to thank Sam ?Veber for his comments on this paper, and Paul Taylor for his
diagrams package.
References
[1] L. Aceto. Eliminating junk rules from GS()S languages. (I?npublished note; to appear,
probably as part of something else.), July 1992.
[2] L. Aceto, B. Bloom, and F. Vaandrager. Turning SOS rules into equations. In Proceed-
ings of LIC5 `92, pages 113--H124. IEEE Computer Society Press, 1992.
[3] L. Aceto, B. Bloom, and F. Vaandrager. Turning SOS rules into equations. Report
CS-R9218, CNVI, Amsterdam, june 1992.
[4] J. Bergstra, J. Klop, and E.-R. Olderog. Readies and failures in the algebra of commu-
nicating processes. SIAAl J. Computing, 1 7(6):11 34--H1177,1988.
[5] J. A. Bergstra and J. ??. Elop. Fixed point semantics in process algebras. Technical
Report 1W 206/82, Department of Computer Science, Nlathematisch Centrum, Ams-
terdam, The Netherlands, 1982.
[6] B. Bloom. Partial traces and the semantics and logic of C ?-hke languages. Technical
Report 89-1066, Cornell, 1989.
36
[8]
[7] B. Bloom. Ready 5imulation, BisimuThtion, and the Semantics of CCS-Like Languages.
PhD thesis, Massachusetts Institute of Technology, Aug. 1989.
B. Bloom, 5. Istrail, and A. R. Meyer. Bisimulation can't be traced (preliminary re-
port). In Conference Record of the F?1eenTh Annual ACAl Symposium on Principles of
Programming Languages, pages 229?239, 1988. Also appears as MIT Technical Memo
MIT/LCS/TM-345.
[9] R. Bol and J. Groote. The meaning of negative premises in transition system specifica-
tions. Report CS-R9054, c\?\?TI, Amsterdam, 1990.
[10] 5. D. Brookes, C. A. R. Hoare, and A. NV. Roscoe. A theory of communica?ing sequential
processes. J. ACM, 31(3):560 599, 1984.
[11] R. de Nicola and M. C. B. Heunessy. Testing equivalences for processes. Theoretical
Computer Sci., 34(2/3):83 133, 1984.
[12] R. v. Glabbeek. The linear time branching time spectrum. In J. Bacten and J. Nlop,
editors, Proceedings COiVCUR 90 Amsterdam, volume 458 of Lect. Notes in Conip uter
Sci., pages 278--H297. Springer-Verlag, 1990.
[13] J. I'. Groote and F. Vaandrager. Structured operational semantics and hisimulation as
a congruence. Information and Computation, 100(2):202--H260, October 1992.
[14] Ni. Hennessy. Algebraic Theory of Processes. MIT Press Series in the Foundations of
Computing. MIT Press, Cambridge, Massachusetts, 1988.
[15] R. Milner. Functions as processes. In Paterson [17], pages 167--H180.
[16] F. Nioller. The importance of the left merge operator in process algebras. In Paterson
[17], pages 752--H764.
[17] M. Paterson, editor. Automata, Languages and Progniniming: 17th international Col-
loqium, volume 443 of Lect. Notes in Compr Sci. Springer-Verlag, July 1990.
[18] A. Pnueli. Linear and branching structures in the semantics and logics of reactive sys-
tems. In NV. Brauer, editor, Automata, Languages and Programming: 12?h CoUoquium,
volume 194 of Lect. Notes in Computer Sci., pages 15 32. Springer-Verlag, July 1985.
37
