On the Expressiveness of Interaction∗
Yuxi Fu

Hao LuBASICS, Department of Computer Science
MOE-MS Key Laboratory
for Intelligent Computing and Intelligent Systems
Shanghai Jiao Tong University, Shanghai 200240, China
February 12, 2010

Abstract
Subbisimilarity is proposed as a general tool to classify the relative
expressive power of process calculi. The expressiveness of several variantsof CCS is compared in terms of the subbisimilarity relationship. Similar
investigation is also carried out for the variants of the pi calculus. The relative expressiveness of the different forms of the choice operation and thedifferent ways of introducing infinite behaviors are systematically studied in both the frameworks of CCS and pi. Some issues concerning theexpressiveness of both CCS and pi are clarified. Several open problems
are solved along the way. The subbisimilarity approach and the relative
expressiveness results are applied to show the independence of the operators of the pi calculus. The definition of the subbisimilarity relationshipcan be further strengthened with computational requirement, leading toa uniform treatment of computation and interaction.

Keywords: Process calculus, expressiveness, bisimulation

Contents
1 Computation and Interaction
1.1 Criteria for Expressiveness . . . . . . . . . . . . . . . . . . . . . .
1.2 Results on Expressiveness . . . . . . . . . . . . . . . . . . . . . .
1.3 Issues to be Addressed . . . . . . . . . . . . . . . . . . . . . . . .
1.4 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
∗ Appeared in Theoretical Computer Science, 411: 1387-1451, 2010

3
3
6
7
9

2 Subbisimilarity for CCS
10
2.1 Semantic Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.2 Bisimulation Theory . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2.1 Subbisimilarity . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2.2 Subbisimilarity and Church-Turing Thesis . . . . . . . . . 19
2.3 Choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.3.1 Termination Preserving Encoding . . . . . . . . . . . . . . 28
2.3.2 Mixed Choice and Guarded Recursion . . . . . . . . . . . 29
2.4 First Order Recursion . . . . . . . . . . . . . . . . . . . . . . . . 37
2.4.1 Expansion Property of Replication . . . . . . . . . . . . . 38
2.4.2 Replication and Mixed Choice . . . . . . . . . . . . . . . 43
2.4.3 Replication, or Fixpoint . . . . . . . . . . . . . . . . . . . 46
2.5 Recursive Definition . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.5.1 Fixpoint, or Constant Definition . . . . . . . . . . . . . . 50
2.6 Interaction Hierarchy of CCS . . . . . . . . . . . . . . . . . . . . 60
3 Subbisimilarity for Pi
63
3.1 Pi Subbisimilarity . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.2 Choice in Pi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.3 Replication in Pi . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
3.4 Parametric Definition in Pi . . . . . . . . . . . . . . . . . . . . . 72
3.5 Interaction Hierarchy of Pi . . . . . . . . . . . . . . . . . . . . . 77
4 Application of Subbisimilarity
79
4.1 Operator Independence . . . . . . . . . . . . . . . . . . . . . . . 79
4.2 Model Assessment . . . . . . . . . . . . . . . . . . . . . . . . . . 82
4.2.1 CCS with Sufficient Computing Power . . . . . . . . . . . 83
4.2.2 Pi with Simple Semantics . . . . . . . . . . . . . . . . . . 83
5 More Subbisimilarities
85
5.1 Name Escape Communication . . . . . . . . . . . . . . . . . . . . 85
5.2 Value-Passing CCS . . . . . . . . . . . . . . . . . . . . . . . . . . 86
5.3 Asynchronous Pi . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
5.4 Internal Communication . . . . . . . . . . . . . . . . . . . . . . . 93
6 Effective Subbisimilarity

94

7 Towards a Model Independent Theory

98

A Proof of Proposition 10

100

2

1

Computation and Interaction

A fundamental issue in process theory is the expressiveness of process calculi.
The most crucial step in studying the expressiveness is to pin down a reasonabledefinition of expressiveness. What does it mean that one process calculus is(strictly) more expressive than another? We start with an overview of some of
the criteria used in the literature and some expressiveness results concerningthe π-calculus [43].

1.1

Criteria for ExpressivenessOne may start looking for the expressiveness criteria by asking the following
question: what is the essential difference between the expressiveness of the process calculi and the expressiveness of the Turing computing models [58]? Process calculi are operational models of open computing systems that formalizeinteraction between systems. In this sense process theory is a theory of interaction [41]. Turing computing models like λ-calculus [5] study closed computing
systems whose only interactions with environments are input and output actions.
Two computable functions are compared by their impacts on the environments,
which are but their input-output behaviors. In other words, the input and theoutput of a computable function are the only interactions of it with environments. The extensional functional equality amounts to saying that a function iscompletely determined by the impacts of these interactions. Generalizing thisview, a process is identified by the effect it may inflict on environments. Since
processes normally interact with environments continuously, the behaviors ofprocesses have to be judged in a co-inductive way. The bisimulation approach
was introduced precisely for this purpose [39, 50, 57].
The above discussion leads to an interactional approach to the study ofprocess expressiveness. The expressive powers of process calculi are comparedin terms of their interactabilities, the ability to interact with environments. In
process theory, interactabilities are defined using labeled transition systems.
Now let the operational semantics of L1 and L2 be defined respectively by thelabeled transition systems (S1 , T1 , −→1 ) and (S2 , T2 , −→2 ). Let 1 and 2 besome chosen observational equivalences of L1 and L2 respectively. Suppose
hJ K,bi is a translation from L1 to L2 , where J K is a map from S1 to S2 and b isa map from T1 to T2 . The following criteria have been used to judge the qualityof the translation [49, 46].
1. Operational Completeness is, from the point of view of interaction, theminimal criterion for “being more expressive”. Process calculi are operational models. For L2 to be at least as expressive as L1 , the former must
be able to simulate the operational behaviors of the latter. This normallyb
λλmeans that JP1 K =⇒2 2 JP2 K whenever P1 −→1 P2 . From the viewpointof interactions, Operational Completeness alone is just not strong enough.
It may well be that JP K can engage in an action to which P does not haveany counterpart action.
32. Operational Soundness requires that whatever JP K can do is the translation
λof an action of P . Formally it requires that JP K =⇒2 P2 always implies
λ0that P =⇒1 P1 for some λ0 , P1 such that JP1 K 2 P2 and λb0 = λ. Operational Soundness guarantees that JP K cannot affect the environments
more than P via interactions.

3. Operational Correspondence consists of Operational Completeness andOperational Soundness. This is a basic criterion when comparing the interactional behaviors of process calculi. In the cases when L1 , L2 are variants
to each other and 1 , 2 are bisimulation-like equivalences, Operational
Correspondence sometimes implies Observational Correspondence.
4. Observational Completeness is the minimal criterion from the point of viewof observation. Formally it imposes the condition that P 1 Q whenever
JP K 2 JQK. Observational Completeness often comes for free. Since all
the contexts of L1 are translated to the contexts of L2 , it follows that P, Q
should be indistinguishable if their translations in L2 are indistinguishable.
5. Observational Soundness places a substantial demand on the quality ofthe translation. It says that JP K 2 JQK whenever P 1 Q. Being areasonable criterion from the point of view of observation, Observational
Soundness is difficult technically. Many encodings studied in the literature
fail to meet this condition.
6. Observational Correspondence, often called Full Abstraction, is the combination of Observational Completeness and Observational Soundness. The
advantage of Full Abstraction is its wide applications. Like Operational
Correspondence, it can be applied to compare two process calculi withquite different action sets, say π-calculus [43] and the ambient calculus [12].
It must be said however that Full Abstraction is not of much use without
Operational Correspondence.
7. Computation Criterion asks that a process that might engage in an infinite
computation is distinguished from a process that cannot do that. How canthis computational property be used to classify interactions? Well in atheory of interaction, computations are internal interactions of systems. If
a process is exclusively engaged in an infinite computation, the process will
never get a chance to interact externally. So computations may interferewith interactions by not giving the latter any chance! Let’s say that P
is terminating if P cannot perform any infinite sequence of τ -actions. In
this paper Computation Criterion refers to the following property.
For every process P of L1 , P is terminating if and only if JP K
is terminating.
Computation Criterion has been used in the previous work [49, 7, 8]. It
can be seen as a reincarnation, in a general theory of interaction, of one
basic understanding of the Turing models, where a function that delivers
4an output upon receiving an input is different from any function that does
not deliver anything at all upon receiving the same input.
A different approach to the study of expressiveness in process calculi, thereductional approach, is based on the reductional semantics [34, 40]. In fact
the reductional approach has been more popular among the two. In this approach only computations are bisimulated. In other words, it is based on the
Operational Correspondence restricted to computation. The bisimulation ofcomputation alone is not a strong enough property for the models of interactions. Additional properties are necessary to uplift the reductional approach.
The solutions that have been proposed are to impose some additional structural
conditions and/or success-testing properties. Let’s take a look at some of them.
• Homomorphism refers to the property that JP | QK 2 JP K | JQK for allprocesses P, Q of L1 [49]. If we think of it, what this condition really says
is that the concurrent composition operator is model-independent.
• Stability [49] is not as popular as Homomorphism. It can be formulated
as JP σK 2 JP Kσ for every process P of L1 and every substitution σ.
Stability is based on the idea that the names are propertyless. If there isa translation from L1 to L2 , there should be a translation from L1 to L2
that is parametric on the names.
• Compositionality [28, 29] is a generalization of Homomorphism. It postulates that the translations of all the operators of L1 are structural.
• Barbedness [45] is a special success-testing property. It requires that if aprocess is capable of performing a certain type of observable actions, so
is its translation; and vice versa. Barbedness offers a simple and versatile
condition for the reductional approach.
Palamidessi uses Uniformity and Reasonability as criteria to compare theexpressiveness of the π-calculi [49]. Uniformity consists essentially of stronger
versions of Homomorphism and Stability where the equivalence 2 is replacedby the syntactical congruence ≡. Reasonability is related to Barbedness. The
following is taken from [49].
Concerning the notion of semantics, we call “reasonable” a semantics
which distinguishes two processes P and Q whenever there exists a
maximal (finite or infinite) computation of P in which the intended
observables (some visible actions) are different from the observables
in any (maximal) computation of Q.
Uniformity and Reasonability make it easy to differentiate various process calculi using the leader electoral systems [49, 51, 62]. Significant results using
the reductional approach have also been reported in a number of papers by
Gorla. See for example [28, 29, 30, 31]. The criteria Gorla has applied to analyze several groups of process calculi are Compositionality, Name Invariance (avariant of Stability), Operational Correspondence, Computation Criterion, and
5

π
πm

?

πs
π−

πi
πa

Figure 1: Encodings Between Pi Variants
Barbedness. The combined force of these criteria is duly demonstrated in theseparation results in loc. cit.
In [7, 8], Busi, Gabbrielli and Zavattaro made use of decidability properties
to tell apart process calculi. The weak point of the decidability criterion is thattwo formulations of an operational semantics might have different decidability
properties on the one hand and the same interactability on the other. Although
decidability per se does not say anything about interactability, it does often
imply the absence of Turing completeness, which is a strong separation criterion. Moreover the techniques used to establish decidability results can often
be modified to prove separation results.

1.2

Results on ExpressivenessWe now sketch some of the relative expressiveness results about the variants of
π-calculus. Let π be π-calculus with the binary choice (for example P + Q),
π m the π with the mixed choice (for example a(x).P + bc.Q), π s the π withthe separated choice (for example a(x).P + b(y).Q and cd.P + ef.Q), π i theπ with the input choice (for example a(x).P + b(y).Q), π − the π without the
choice, and π a the asynchronous π. Palamidessi summarizes in [49] the existing relative expressiveness of these variants by the diagram in Figure 1. The
sub-calculus relationship is indicated by the hooked arrow ,→. The plain arrow→ indicates the existence of a uniform and reasonable encoding. Boudol, oneof the proposers of π a , gives in [6] a translation from π − to π a that preserves
a Morris style contextual equivalence. Honda and Tokoro provide a different
encoding whose correctness is proved for some weak bisimilarity [34]. Theirasynchronous bisimilarity is adopted as the standard bisimulation equivalence
for the asynchronous calculi. Nestmann and Pierce study in [46] two encodings
from π i to π a . One is fully abstract with respect to the asynchronous bisimilarity but not termination preserving. The other is termination preserving but
not fully abstract. In π a [47] Nestmann examines some encodings of π s andargues without a proof that no fully abstract translation from the former to thelatter exists. Palamidessi proves in [49] that there is no uniform and reasonableencoding from π m to π s .
Some other variants of the asynchronous π-calculus have been considered6

in literature. In [53] the authors study the relative expressiveness of three
restrictions of π a . The P Oπ calculus is obtained from π a by forcing all the
output processes to be of the form !an. In other words, the output processes
are persistent. Similarly P Iπ is the calculus in which all the input processes
are of the form !a(x).T ; and P π is the variant in which both output and input
processes are persistent. It is argued in [53] that P Oπ and P Iπ are as expressiveas π a in a certain sense, and that P π is strictly less expressive than π a . However
the authors of [10] demonstrate that there are no encodings from π a to any threeof the variants that preserve testing equivalence [14, 32].
Some expressiveness results about Ambient Calculi are reported [42, 51, 30].
However the overall picture is not yet clear.

1.3

Issues to be Addressed

How forceful are the results stated in Figure 1? It is fruitful to take a look atthese results using the criteria discussed above.
1. From the viewpoint of Operational Correspondence, the encodings indicated by the arrows of Figure 1 vary considerably. For example there is an
encoding from π i to π a that satisfies Operational Correspondence [46]. On
the other hand the known encoding from π s to π a satisfies much weakerproperties than Operational Correspondence [47]. Using simple argument,
as we shall see later, one can show that the ‘tossing-the-coin algorithm’,
which can be programmed in π s by cf + ct, cannot be coded up in any of
π i , π a and π − in a way that Operational Correspondence is respected.
2. From the point of view of Observational Correspondence, the encodings
indicated by the arrows of Figure 1 are different. For instance, the nonexistence of a uniform and reasonable encoding from π m to π s does not ruleout the existence of a fully abstract encoding from π m to π s , with respect
to the weak bisimilarity, that respects Operational Correspondence. On
the other hand the arrow from π m to π a , as indicated in Figure 1, is supported by an encoding much weaker than a fully abstract encoding withrespect to the weak bisimilarity. Moreover, different encodings are making
use of different equivalences. For the encoding π i → π a the asynchronous
equivalence of π i is used. In the embedding π i ,→ π s the weak bisimilarityof π i is used. The question of how we should relate the asynchronous
calculi to the synchronous ones also comes up.
3. From the point of view of Computation Criterion, the encodings indicated by the arrows of Figure 1 are not all consistent. On the one hand,
Palamidessi has essentially proved that there is no uniform and reasonableencoding from π m to π s that satisfies Computation Criterion, which is indicated as a negative result in Figure 1. On the other hand, an encodingof π s in π a , indicated as a positive result in Figure 1, can hardly satisfy
Computation Criterion.

7

According to the above analysis, there is a real need to clarify the picture
about the relative expressiveness of the π-variants. It would be fruitful to lookat the models from the point of view of interactability. The computational
factor should also be considered since they interfere with the interactions. In
other words we expect to strengthen the results stated in Figure 1 by answering
the following question.
Question 1: What are the relationships between the π variants if
Operational Correspondence and Observational Correspondence are
adopted? What if Computation Criterion is also adopted?
To answer the above question, some open problems need be solved. The relative
expressiveness of π over π m has stood unanswered for quite some time. Fromthe viewpoint of interactions, the problem can be formalized as follows: Is therea (termination preserving) encoding J K from π to π m such that P ≈ JP K? The
answer is not just practically interesting, it is also theoretically important. Similarly the relative expressiveness of π m over π s is not completely settled, despiteof the result in [49]. The question to be answered is this: Is there a (termination
preserving) encoding J K from π m to π s such that P ≈ JP K? There is also a question on whether any form of the external choice is redundant. In other words,
is there an encoding J K from π s to π − such that P ≈ JP K? The choice operator
is often used in specification [39], whereas the concurrent composition “|” isan implementation operator. The third question can be equivalently stated asfollows: is there a specification that cannot be implemented without the choice
operator? Most of the above problems are open even for CCS.
The π-calculus has some well known relatives. These include the valuepassing CCS, the asynchronous π-calculus, the πI-calculus. It is interesting toinvestigate the expressiveness of these calculi using similar criteria.
Question 2: What are the comparative expressiveness of the wellknown π relatives if Operational Correspondence and Observational
Correspondence are adopted? What if Computation Criterion is also
adopted?
Sometimes two variants only differ in the ways the infinite behaviors are
introduced. The well known recursion mechanisms are the fixpoint operations,recursive definitions and replications. It is also interesting to see if different
recursion mechanisms make a difference in interaction.
Question 3: What are the comparative expressiveness of the various
recursion mechanisms from the viewpoint of interaction?
Answers to the above questions will not only improve our understanding of
Figure 1, but also help us to look for a model-independent theory of expressiveness. It is our belief that the theory of expressiveness is the most fundamental
part of the process theory, playing a role similar to that of the theory of computability in computation theory. It is also our belief that a model-independent
theory of expressiveness provides a unifying framework to integrate the process
theory and the computation theory.
8

1.4

Contributions

We set out to answer the questions and solve the problems stated in Section 1.3.
Our contributions are as follows.
1. We propose a general framework to compare the expressive powers of CCS
variants and π variants in a uniform manner. The major contributions canbe summarized in four statements.
(a) Subbisimilarities are introduced as a uniform tool to study the expressiveness of interaction, incorporating both Operational Correspondence and Observational Correspondence.
(b) The relative expressive powers of nine variants of CCS, and the corresponding variants of π-calculus, are characterized in terms of the
subbisimilarity.
(c) The relative expressive powers of these variants are also characterized
in terms of the codivergent subbisimilarity in which Computation
Criterion is incorporated.
(d) The effectiveness of the subbisimilarities is formalized and its link toChurch-Turing Thesis is pointed out.
2. By applying the subbisimilarity tool, we contribute to the theory of expressiveness in three aspects.
(a) A number of relative expressiveness results are obtained. The results
are concerned with the dynamic binding mechanism, value-passing
mechanism, and several variations of the name-passing mechanism.
(b) It is formally established that all the standard operators of the πcalculus are independent of each other.
(c) It is pointed out how the expressiveness results can be used to assess
the process calculi.
At a more technical level, our contributions are proof techniques for establishing
the negative results about expressiveness.
The paper is organized as follows. The subbisimilarities for CCS variants
are introduced in Section 2 to study the expressiveness of the choice operatorsand the recursions of different kind. Some open problems about CCS are solved,
and some issues are clarified. The approach is extended to the setting of the
π-calculus in Section 3 to investigate the relative expressiveness of the variantsof π-calculus. Section 4 gives two applications of the expressiveness theory. One
is about the independence of process operators. The other is about model assessment. Section 5 takes a look at the expressiveness of some π-related calculi
and the issue of static binding versus dynamic binding. Section 6 adds weight toComputation Criterion by discussing the effectiveness of the subbisimilarities.
Section 7 concludes with the remarks on the significance of the subbisimilarity approach and its implication to a model-independent theory of interaction.
Some of the long proofs are placed in the appendix.
9

2

Subbisimilarity for CCS

The importance of CCS [39] cannot be over emphasized. It is a cornerstone intheory of interaction [41]. Being one of the first process calculi, CCS provides aframework in which one could study interactions in a pure and distilled form.
As an operational model, CCS is a testbed for studying expressiveness ofprocess calculi. However discussion on the expressiveness of variants of CCS
have been rare. This is unfortunate since expressiveness has to be an important
issue in process theory.
In this section we shall reveal the relationships among several variants of
CCS in terms of expressiveness. Apart from serving as a technical preamble,
the results in this section are also interesting on their own.

2.1

Semantic Theory

The fundamental idea of theory of interaction is that a computing agent possesses a number of interfaces and that two computing agents interact throughthe interfaces. To indicate that an agent has a particular kind of interface weassign a name to an interface. Two agent may interact if they have interfaces ofsame (or complementary) names. We shall assume that there is a set of names
N ranged over by a, b, c, d, e, f, g, h. The notation N stands for {a | a ∈ N },the set of conames. The set N ∪ N ∪ {τ } of the action labels is ranged over by
λ. The notation λ is defined as follows: a if λ = a,def
a if λ = a,λ =τ if λ = τ.
The syntax of CCS expression is defined by the following grammar:E:= 0 | X | λ.E | E | E 0 | (a)E | E+E 0 | µX.E.

We have left out the relabeling operation for the following reason. Our interest
in CCS is to obtain results that can be easily transferred to π-calculus. For that
purpose the relabeling operation is not necessary. In the localization form (a)E,
the name a is local. A name is global if it is not local. The notation gn( ) (ln( ))stands for a function that returns the set of global names (local names). In the
fixpoint expression µX.E the process variable X is bound. A process variable
is free if it is not bound. The notation F V ( ) (BV ( )) stands for a functionthat returns the set of free variables (bound variables). To simplify notations,
we assume that the restriction, prefix and fixpoint operators bind tighter thanthe composition operator, which in turn binds tighter than the choice operator.
Unless otherwise indicated, the α-conversion applies to both local names andbound variables.
A CCS expression that does not contain any free variable is called a CCS
process. For a process calculus L, we shall write EL for the set of the expressionsof L and PL for the set of the processes of L.
10We will use the standard notations and conventions in process calculi. We
omit the inactive process 0 in most occasions. For instance the process expressions A | 0 and a.b.0 are abbreviated to A and a.b. A finite sequence ofnames a1 , . . . , an is often abbreviated to ea. When no ambiguity arises, e
a is also
used for the finite set {a1 , . . . , an }. The notation e will also be applied to othersyntactical entities. We shall use the notation
X
Ei
i∈I

where I is a finite indexing set, for finite summation, making use of the factthat the binary choice operator is associative. Similarly we write
Y
Ei
i∈I

for Ei1 | . . . | Ein where I = {i1 , . . . , in }. We also writeYE
ifor E | . . . | E .
| {z }
i times

The standard operational semantics of CCS is inductively generated by thefollowing rules.
Prefixλλ.E −→ E
Composition
λE −→ E 0aa

E −→ E 0
F −→ F 0τ
E | F −→ E 0 | F 0

λ

E | F −→ E 0 | F
Restriction
λE −→ E 0

a does not appear in λλ(a)E −→ (a)E 0
ChoiceλE −→ E 0λ

E + F −→ E 0
Fixpoint
λE{µX.E/X} −→ E 0
λµX.E −→ E 0
Notice that the symmetric rules are omitted. The standard reference bookon CCS [39] covers the fundamental theory about the model. We will assume11

that the reader is familiar with the labeled transition semantics and the basicbλoperators in process calculi. As usual we will write =⇒ and =⇒ for their
λλstandard interpretations. We write E −→ if E −→ E 0 for some E 0 , and E 9 ifτthere is no E 0 such that E −→ E 0 .
A process variable X in E is guarded if every occurrence of X in E isunderneath some prefix operation. We write α to stand for a renaming like{b1 /a1 , . . . , bn /an }. We write {E1 /X1 , . . . , En /Xn } for substitutions of variables. When applying the substitution to a process expression E, notationeE{E1 /X1 , . . . , En /Xn }, we get a process expression obtained by replacing Xeby respective E. Bound names need be renamed to avoid name capture. For
instance (e)(f )(ce | df | X){ae | bf /X} is the expression (g)(h)(cg | dh | ae | bf ).
Sometimes, especially when studying dynamic binding calculi, we need substitutions that do not admit α-conversion. For that purpose we introduce thedynamic substitution of variables [E1 /X1 , . . . , En /Xn ]. For instance the syntactic object (e)(f )(ce | df | X)[ae | bf /X] is the expression (e)(f )(ce | df | ae | bf ).
The substitutions of variables will be ranged over by ς. Sometimes we writeE[X1 , . . . , Xn ] to indicate explicitly that X1 , . . . , Xn occur in E. Accordingly
we write E[E1 , . . . , En ] for E{E1 /X1 , . . . , En /Xn } when no confusion arises.
Occasionally we extend the substitutions of variables to the substitutions of expressions. We write E{F/µZ.G} for instance for the expression obtained from
E by replacing all the occurrences of the subexpression µZ.G of E by F .
Lemma 1 (Stability Lemma). The following statements are valid.
λλα(i) If E −→ E 0 then Eα −→ E 0 α.
λλ(ii) If E −→ E 0 then E{H/X} −→ E 0 {H/X}.
λλ(iii) Suppose a 6∈ gn(E). If E{a/X} −→ E 0 {a/X} then E −→ E 0 .
For n ≥ 0, an n-step derivative of a process expression E is an E 0 such that
λ1
λn
E −→
. . . −→
E 0 . Let Drvn (E) be the set of the n-step derivativesof E. ByS0+ndefinition
Drv
(E)
=
{E}.
Let
Drv(E)
and
Drv
(E)
be
Drv
(E) and
n≥0
S
n
Drv
(E)
respectively.
A
computationofEiseitheran
infiniteinternaln≥1τττ
action sequence E −→ . . . −→ Ei −→ . . . or a finite internal action sequenceττE −→ . . . −→ E 0 . Let Cmp(E) be the set of all the computations of E. The
expression E is terminating if Cmp(E) does not contain any infinite sequence.
It is divergent otherwise.
The complexity of the operational theory of CCS is caused by the fixpoint
operator. There are very few results, if any, that characterize the infinite behaviors of the process expressions of CCS. However the subtle difference between
two variants of CCS is very likely to do with the infinite behaviors. The following lemma offers an important tool to analyze the operational behaviors of the
fixpoint operations.
λLemma 2 (Recursion Lemma). Suppose G[µX.E] −→ K. The following statements are valid.
(i) K ≡ G0 [µX.E] for some expression G0 [X].
12λ(ii) There exists some natural number i such that G[E[E[. . . [E [X]] . . .]]] −→| {z }
i timesλG0 [X] and i is no greater than the height of the derivation of G[µX.E] −→ K.
Proof. The proof is a typical example of induction on the height of derivation.
We take a look at two cases.
τ• G ≡ G1 | G2 . If for example the transition G[µX.E] −→ K1 | K2 isaacaused by G1 [µX.E] −→ K1 and G2 [µX.E] −→ K2 . By induction hypothesis some i1 , i2 , G01 [X], G02 [X] exist such that K1 ≡ G01 [µX.E], K2 ≡G02 [µX.E],a
G1 [E[. . . [E [X]] . . .]] −→ G01 [X]| {z }
i1 timesanda

G2 [E[. . . [E [X]] . . .]] −→ G02 [X].
| {z }
i2 times

Now assume i1 ≥ i2 . Let G0 [X] be G01 [X] | G02 [ E[. . . [E [X]] . . .]]. It is| {z }
i1 −i2 times

τ

obvious that G[E[. . . [E [X]] . . .]] −→ G0 [X].
| {z }
i1 timesλ• G ≡ µY.G1 [X, Y ]. It follows from µY.G1 [µX.E, Y ] −→ K thatλG1 [µX.E, µY.G1 [µX.E, Y ]] −→ K
is derivable with a shorter derivation. Let G2 [X] be G1 [X, µY.G1 [X, Y ]].
Then by induction hypothesis one immediately sees that some i, G0 [X]exist such that G0 [µX.E] ≡ K andλG2 [E[. . . [E [X]] . . .]] −→ G0 [X].
| {z }
i timesλIt follows that G[E[. . . [E [X]] . . .]] −→ G0 [X].
| {z }
i times

We are done.
In what follows, we often need to specify a particular occurrence of a process
variable. We shall write EhXi to indicate that a particular occurrence of a free
process variable X in E has been specified. If for example E ≡ a.X | B + A | X
then the specified occurrence could be the second X. We will write for example
EhF/Xi for the expression obtained by replacing the specific occurrence of X by
F . If E ≡ a.X | B +A | X and the specified occurrence of X is the second X then
EhF/Xi is a.X | B + A | F . Using this notation we could write E{G/X}hF/Xi
13

for a.G | B + A | F . This is the expression obtained by replacing all the occurrences of X in EhF/Xi by G. When no ambiguity arises we sometimes write
EhF i for EhF/Xi. To describe the operational property of EhXi, we introduce
the notation (EhG/Xi)† inductively defined by the following clauses.
(hG/Xi)†def(λ.EhG/Xi)†

def=

λ.EhG/Xi,

0†(E | EhG/Xi)

def=

E 0 | (EhG/Xi)† ,(EhG/Xi | E 0 )†def=

(EhG/Xi)† | E 0 ,((a)EhG/Xi)†def=(a)(EhG/Xi)† ,(E 0 + EhG/Xi)†

def=(EhG/Xi)† ,(EhG/Xi + E 0 )†def=

(EhG/Xi)† ,(µZ.EhG/Xi)†

def(EhG/Xi)† {µZ.EhG/Xi/Z}.

==

hG/Xi,

Intuitively (EhG/Xi)† is what remains if EhG/Xi performs an action inducedby G. Using this notation, we may describe the operational behaviors of expressions in a more specific manner. We shall identify EhXi† to (EhX/Xi)† .
Lemma 3. The following statements are valid.
λλ(i) If EhG/Xi −→ E 0 is caused by G −→ G0 , then E 0 ≡ (EhG0 /Xi)† .
λ(ii) If EhG/Xi −→ E 0 hG0 /Xi is caused by an action of G, then E 0 hG0 /Xi ∼E 0 h0/Xi | G0 .
Proof. Here ∼ is the structural bisimilarity, see Definition 2. The proof is a
simple induction on the height of derivation. Notice that the static binding
mechanism is important for the induction to go through.
A useful fact about EhG/Xi is that a communication between E and G must
be through a global channel name. This is formalized in the following lemma,
the proof of which is again an induction on derivation.
τaaLemma 4. If EhG/Xi −→ E 0 hG0 /Xi is caused by EhXi −→ E 0 hXi and G −→a
G0 , then EhXi† −→ E 0 hXi.
Conversely if two parts of a CCS expression can perform complementaryactions at a global channel, then they can interact through that channel. This
property can be described by the following two lemmas.
λ

λ

1
2
Lemma 5 (Confluence). If EhG/Xi −→(EhG0 /Xi)† −→E 0 hG0 /Xi is caused

λ

λ

2
1
by a λ1 of G and a λ2 of EhXi† , then EhG/Xi −→−→E 0 hG0 /Xi.

aaLemma 6. If EhG/Xi −→ (EhG0 /Xi)† −→ E 0 hG0 /Xi is caused by the actionaaτ
G −→ G0 and EhXi† −→ E 0 , then EhG/Xi −→ E 0 hG0 /Xi.
14

2.2

Bisimulation Theory

A basic technique in the observational theory of interaction is the bisimulation
technique [50, 39, 57]. The co-inductive nature of bisimulation can be seen fromdef

the following simple argument: To conclude if the two processes E = a.E 0 anddef
F = a.F 0 are observationally equivalent, one needs to know if E 0 and F 0 are
observationally equivalent. Now E 0 , respectively F 0 , may well be E, respectively
F . It has been demonstrated that co-induction is almost a universal tool inanalyzing the observational behaviors of interactions.
This subsection lays down the basic bisimulation theory of CCS. We shallfocus on the CCS defined above. However the results in this subsection are valid
for all the variants of CCS considered in this paper.
Definition 1. A binary symmetric relation R on ECCS is a bisimulation if thefollowing statements are valid whenever ERF .
(i) EςRF ς for every substitution ς of process variables.
λbλ(ii) If E −→ E 0 then F =⇒ F 0 RE 0 for some F 0 .
The bisimilarity ≈ is the largest bisimulation.
The stronger version of ≈ is often useful.
Definition 2. A binary symmetric relation R on ECCS is a structural bisimulation if the following statements are valid whenever ERF .
(i) EςRF ς for every substitution ς of process variables.
λλ(ii) If E −→ E 0 then F −→ F 0 RE 0 for some F 0 .
The structural bisimilarity ∼ is the largest structural bisimulation.
The equivalence relations ∼ and ≈ are defined on the set of the expressions
with free variables. It follows immediately from Definition 2 and Definition 1that both ∼ and ≈ are closed under the substitutions on variables. Moreover
the two relations are also closed under injective renaming.
Lemma 7. If E ≈ F then Eα ≈ F α for every injective renaming α.
If R is a symmetric relation on CCS processes, the condition (i) of Definition 1 and Definition 2 is vacuously satisfied. Fortunately we only have toconsider relations of this kind when establishing bisimulation equality for process expressions. This is due to the following lemma.
Lemma 8. E ≈ F if and only if E{a/X} ≈ F {a/X} for some name a that
does not appear in E | F .
Proof. One direction is obvious. For the other direction let S be the following
relation
E{a/X} ≈ F {a/X},

(E{G/X}, F {G/X}) G is a process expression,.
a does not appear in E | F | G
It follows from Lemma 7 that S is closed under substitution of variables. Now
λsuppose E{G/X} −→ H. There are three cases.
15

λ

λ

• The action E{G/X} −→ E 0 {G/X} is caused by E −→ E 0 . ObviouslybλλE{a/X} −→ E 0 {a/X} must be simulated by F {a/X} =⇒ F 0 {a/X} ≈b
λE 0 {a/X} for some F 0 . Hence F {G/X} =⇒ F 0 {G/X} S −1 E 0 {G/X}.
λλ• The action EhGi{G/X} −→ (EhG0 /Xi)† {G/X} is caused by G −→ G0 .
aThen Eha/Xi{a/X} −→ (Eh0/Xi)† {a/X}, which must be simulated byaF ha/Xi{a/X} =⇒ F 0 h0i{a/X} ≈ E 0 h0/Xi{a/X}
for some F 0 . Now
λF hG/Xi{a/X} =⇒∼≈∼F 0 hG0 /Xi{a/X}
F 0 h0/Xi{a/X} | G0
E 0 h0/Xi{a/X} | G0
E 0 hG0 /Xi{a/X}

where the structural bisimilarities are due to Lemma 3. ThereforeλF hG/Xi{G/X} =⇒ F 0 hG0 /Xi{G/X} S −1 E 0 hG0 /Xi{G/X}.
τb• The action EhG/Xi{G/X} −→ E 0 hG0 /Xi{G/X} is caused by EhXi† −→b

E 0 hXi and G −→ G0 . Thereforeab

Eha/Xi{a/X} −→ (Eh0/Xi)† {a/X} −→ E 0 h0/Xi{a/X}
which must be simulated by F ha/Xi{a/X} as follows:
F ha/Xi{a/X} =⇒ F1 ha/Xi{a/X}a−→ F2 h0/Xi{a/X}=⇒ F3 h0/Xi{a/X}b−→ F4 h0/Xi{a/X}=⇒ F5 h0/Xi{a/X}≈ E 0 h0/Xi{a/X}.
It follows from Lemma 5 that some F20 exists such that
F1 ha/Xi{a/X} =⇒ F20 ha/Xi{a/X}a−→ F3 h0/Xi{a/X}.
Lemma 6 and the following two-action sequenceb

F3 hG0 /Xi{a/X}b

F4 hG0 /Xi{a/X}

F20 hG/Xi{a/X} −→
−→
16

τ

imply that F20 hG/Xi{a/X} −→ F4 hG0 /Xi{a/X}. Hence
F hG/Xi{a/X} =⇒ F5 hG0 /Xi{a/X}∼ F5 h0/Xi{a/X} | G0
≈ E 0 h0/Xi{a/X} | G0
∼ E 0 hG0 /Xi{a/X}.
Consequently
F hG/Xi{G/X}

=⇒
S −1

F5 hG0 /Xi{G/X}
E 0 hG0 /Xi{G/X}.

We conclude that S is a bisimulation.
Lemma 8 allows one to concentrate on the bisimulations on processes. It
also indicates that our bisimilarity is the same as Milner’s bisimilarity on CCS
expressions [39].
Definition 3. A binary symmetric relation R on ECCS is a bisimulation up to∼ if the following statements are valid whenever ERF .
(i) EςRF ς for every substitution ς of process variables.
λbλ(ii) If E −→ E 0 then F =⇒ F 0 ∼ R ∼ E 0 for some F 0 .
The reason to introduce the above definition is the following useful fact.
Lemma 9. If R is a bisimulation up to ∼ then R ⊆≈.
Before ending this subsection we state a result that will be referred to lateron. See [39] for detail.
Lemma 10. If every occurrence of X in E is bounded by some prefix operation,then the equation X ∼ E has a unique solution up to ∼.
2.2.1

Subbisimilarity

To study the expressive power of CCS variants, we would like to introduce atool that embodies both Operational Correspondence and Observational Correspondence. The Equivalence Criterion has been frequently used to compare therelative expressive powers of the variants of a same model, see for example [49].
Given an equivalence relation , Equivalence Criterion can be stated as follows:
L2 is at least as expressive as L1 if for every P1 in L1 there is someP2 in L2 such that P1  P2 .
To apply this criterion, one needs to pin down an equivalence relation. It is ourview that the bisimilarity of Park [50] and Milner [39] offers the right balance
between the distinguishing power of the observer and the control power of theobservee. So most of the time we shall understand  as the weak bisimilarity
17≈. To prove that a process P1 of L1 is bisimilar to a process P2 of L2 , one
actually constructs a binary relation that contains the pair (P1 , P2 ) such thatthe bisimulation property holds of the relation. We shall call such a relation a
subbisimilarity. Let’s start with the following simple definition.
Definition 4. A relation R ⊆ S1 × S2 is total if ∀S1 ∈ S1 .∃S2 ∈ S2 .S1 RS2 .
It is surjective if ∀S2 ∈ S2 .∃S1 ∈ S1 .S1 RS2 .
We will write R; R0 for the composition of R ⊆ S1 × S2 and R0 ⊆ S2 × S3 ,and R−1 for the reverse relation of R.
Intuitively a subbisimilarity interprets every process of a variant by (at least)
one process of another variant in such a way that generalizes an encoding. The
following definition strengthens the definition of bisimulation of [27] with thetotality condition.
Definition 5. Suppose CCS1 and CCS2 are two CCS variants. A subbisimilarity from CCS1 to CCS2 is a total relation R ⊆ PCCS1 × PCCS2 such that thefollowing bisimulation property holds whenever P1 RP2 .
λ

b
λ

λ

b
λ

If P1 −→1 P10 then P2 =⇒2 P20 R−1 P10 for some P20 .
If P2 −→2 P20 then P1 =⇒1 P10 RP20 for some P10 .
We shall say that CCS1 is subbisimilar to CCS2 , notation CCS1 vccs CCS2 , ifthere is a subbisimilarity from CCS1 to CCS2 . We write CCS1 @ccs CCS2 if
CCS1 vccs CCS2 and CCS2 6vccs CCS1 .
It is obvious that the subbisimilarity relationship vccs is transitive. In what
follows, we often say that an interpretation J K from CCS1 to CCS2 is a subbisimilarity. This should be understood as saying that J K generates a subbisimilarity. To prove CCS2 6vccs CCS1 , one only has to show that some P2 of CCS2
exists such that for every P1 of CCS1 the pair P1 , P2 do not satisfy the bisimulation property. Equivalently it amounts to showing the following property:∃P2 ∈ PCCS2 .∀P1 ∈ PCCS1 .P2 6≈ P1 .
Our particular choice of subbisimilarity can be further justified in the following accounts:• The subbisimilarities are based on the assumption that the environments
are dynamically changing and therefore are strong enough to detect thedifference of two processes that are not bisimilar. This is a reasonableassumption for a model of interaction.
• A positive result stated in terms of subbisimilarity, say CCS1 vccs CCS2 , ismore significant than most positive statements using other weaker criteria.
• A counter example refuting the existence of a subbisimilarity can often
be modified to give a separation result when a set of weaker criteria is
applied. The negative results stated in terms of subbisimilarity are far
more general than they appear to be.
Our motivation is that the subbisimilarities should play a role similar to thatof the reductions in computing theory. This point is elaborated next.
18

2.2.2

Subbisimilarity and Church-Turing Thesis

The theory of computation is built upon a fundamental assumption (hypothesis)
referred to as Church-Turing Thesis [35, 16]. It is normally stated as follows.
Church-Turing Thesis: Two models of computation, M1 and M2 ,are equivalent in the sense that the functions definable in M1 aredefinable in M2 and vice versa.
Basically Church-Turing Thesis says that the theory of computation is modelindependent. Various extensions of the thesis have been proposed with thedevelopment of the theory of algorithm [2] and the complexity theory [64]. The
Extended Church-Turing Thesis is a generalization of Church-Turing Thesis. It
states that two models of computation not only define the same set of functions, they also simulate each other’s calculations of functions. The following
formulation is taken from [64].
Extended Church-Turing Thesis: For two models of computation,
M1 and M2 , there is a polynomial p such that t computation steps of
M1 on an input of length n can be simulated by p(n, t) computation
steps of M2 .
The Extended Church-Turing Thesis ensures that the bulk of the complexity
theory is model-independent. The practical implication of this thesis is that acompiler never changes the feasibility of programs. When moving from compilers
to interpreters, another aspect of Church-Turing Thesis comes in sight. An
interpreter should not introduce too much computational overhead to the extent
that a feasible solution is executed in an infeasible way. This is a strong versionof Church-Turing Thesis.
Strong Church-Turing Thesis: For two models of computation, M1
and M2 , there is a polynomial p such that a program of M1 of size n
is translated mechanically to a program of M2 in p(n) steps and thatthe program and its translation simulate each other’s computations.
Let’s try to formalize the computational and the effective aspects of ChurchTuring Thesis in an abstract setting. Suppose that (M0 , →0 ) and (M1 , →1 )are two models of computation. Let →∗i , for i ∈ {0, 1}, be the reflexive andtransitive closure of →i . If we ignore the feasibility requirement, Church-Turing
Thesis means at least that there is a recursive function that translates a program
M of M0 to a program N of M1 . A computational step M →0 M 0 is simulated
by several computation steps N →∗1 N 0 . It often happens that the program N 0
is syntactically different from the translation of M 0 . But the two are equivalentsemantically. A standard approach to get around this problem is to introduce
some equivalence relation on the set of all the programs of M1 . If M1 say is the
λ-calculus, the β conversion =β is often taken to be the equivalence. In someother cases a structural congruence is introduced to play the role. The use of
the equivalence relation is orthogonal to the interpretation. There is not any
canonicity in the choice of such an equivalence relation. A better approach is19

to extend the interpretation from a recursive function to a relation that inherits
the effectiveness of the interpretation function and reincarnates the equivalenceon the programs of M1 . So what Church-Turing Thesis tells us is that there
should be a total relation T from the set of the programs of M0 to the setof the programs of M1 such that given a program M of M0 the set of theinterpretations of M under T can be effectively generated. In both programming
practice and in theory, another aspect of effectiveness is necessary. Suppose T
is an interpreter and M0 TM1 . If M1 evaluates to M10 after a finite number ofcomputations steps, then the interpreter needs to find effectively some M00 suchthat M00 TM10 . After finding out M00 the interpreter may return M00 as the resultof the evaluation of M0 . A mild formalization of these effectiveness requirements
is given in the next definition.
Definition 6. A binary relation R from an effective set S to an effective set T
is effective if the following statements are valid: (i) If T 0 is an effective subset
of T , then {x | (x, y) ∈ R ∧ y ∈ T 0 } is effective. (ii) If S 0 is an effective subset
of S, then {y | (x, y) ∈ R ∧ x ∈ S 0 } is effective.
To appreciate Definition 6, recall that a partial numeric function f : X * Y
is effective if and only if its graph is effective. If f is effective and X 0 is aneffective subset of X then f (X 0 ) is effective. Conversely if f is effective and Y 0
is an effective subset of Y then f −1 (Y 0 ) is effective. The effective relations aremeant to generalize the effective functions.
Let T be a total relation from PM0 to PM1 that demonstrates the Turing
completeness of M1 assuming that M0 is Turing complete. The relation T
should validate at least the following statements.
1. If M TN and M →0 M 0 then N →∗1 N 0 T−1 M 0 for some N 0 .
2. If M TN →1 N 0 then M →∗0 M 0 TN 0 for some M 0 .
3. If M0 TN0 and M0 →0 M1 →0 . . . Mi →0 . . . is an infinite computation
sequence, then there must be some k ≥ 1 and N 0 such that N0 →+1
N 0 T−1 Mk .
4. If M0 TN0 and N0 →1 N1 →1 . . . Ni →1 . . . is an infinite computation
sequence, then there must be some k ≥ 1 and M 0 such that M0 →+0
M 0 TNk .
5. Effectiveness Condition: T is effective.
In the statement of Effectiveness Condition, we have confused for example theset PM0 with the set of the Gödel numberings of the elements of PM0 . No harmshould be caused by this confusion.
Conditions 1 and 2 follow from Extended Church-Turing Thesis. It is important to realize that the underlying philosophy of Extended Church-Turing
Thesis is that equivalence of computations is of a bisimulation nature. Conditions 3 and 4 are required by Church-Turing Thesis. This is because a programthat ends with a result upon an input is different from any program that fails
20

to deliver anything after receiving the same input. To go along with Strong
Church-Turing Thesis, Conditions 3 and 4 are formulated in a bisimulationstyle.
Condition 5 reminds one of Turing reduction. Without Effectiveness Condition the requirements 1-4 are too weak to be of any use. Consider the following
translation from the Deterministic Turing Machines to the λ-terms. It maps
def
all the terminating machines to I = λx.x and all the nonterminating machinesdefto Ω = (λx.xx)(λx.xx). This map satisfies the conditions 1-4 stated above.
However in no sense can it be used to demonstrate the Turing completeness ofthe λ-calculus.
Now how are the computations modeled in theory of interaction? The guideline is that, since computations are internal actions, they are modeled by theτ -actions. If a process interprets a program, then all the internal actions of
the process correspond to the computations of the program. From the observational point of view, since computations are calculations or evaluations, ifc, Mc0 of M, M 0 respectively in a process
M →∗ M 0 then the interpretations M
calculus should be equivalent interactively. In other words, we have the following
situation:ττc −→c0 ≈ Mc.
M. . . −→ M
In theory of interaction, what are the rules that govern the behaviors of theabove computation? If M is calculated half way through to an intermediate
d00 must be
state M 00 , our intuition about Turing computation suggests that M
cequivalent to M . In theory of interaction this is guaranteed [19].
τττLemma 11 (Computation Lemma). If P0 −→ P1 −→ · · · −→ Pn ≈ P0 thenP0 ≈ P1 ≈ P2 ≈ · · · ≈ Pn .
Although Computation Lemma is stated for ≈, it holds for almost all theobservational equivalences one can think of. Computation Lemma is a property about the internal actions of systems, it is not a property about processequivalences.
According to Computation Lemma, the self evolution of a system is carriedout in phases, which can be depicted as follows.
τ

τ

τ

τ

τ

τ

P0 −→ · · · −→ Pi1 −→ Pi1 +1 −→ · · · −→ Pi2 −→ . . . .
The phase one consists of all the states from P0 to Pi1 , which are all equivalentfrom the point of view of interaction. What phase one accomplishes is someinternal adjustment. It has not made any irretrievable decision. The step from
Pi1 to Pi1 +1 is fundamental. Once the system has done that, there is no goingback. This pattern is repeated again and again throughout the evolution.
Computation Lemma is of crucial importance to the encodings studied inthis paper. A typical scenario of applying Computation Lemma is the following:

21

λn

P0
τ

λ0
τ

Pn

P1

λ1

τ∗

τ∗

λi

Pi

Imagine that there is an agent traveling around the states of the circle. All thestates on the circle are equivalent by Computation Lemma. So as long as theagent is staying on the circle, it retains all the powers to kick off any of thepossible actions doable by Pi . But at any particular state, say Pi , the agent
might decide to kick off the action λi . Once it does that, the system moves tothe next stage. The circle is a reiterative infinite computation. It will be provedthat for many encodings this kind of infinite computation has to be introduced.
While on the subject, we mention that the fact stated in Computation
Lemma has been explored in the definition of branching bisimilarity [26] of
van Glabbeek and Weijland. It is argued in [26] that the branching bisimilarity,
which is stronger than ≈, should be preferred to ≈ in a number of applications.
As a matter of fact encoding between process calculi is an important application
where the branching bisimilarity has an edge over the bisimilarity of Park andMilner.
Once Church-Turing Thesis has been formalized in the above manner, theclose relationship between Church-Turing Thesis and subbisimilarity emerges.
Now suppose R is a subbisimilarity from CCS1 to CCS2 . Let Rc be the least
superset of R that satisfies the following closure properties:
1. If P1 SP2 then (c)P1 S(c)P2 ;2. If P1 SP2 and P is in both CCS1 and CCS2 , then P1 | P S P2 | P and
P | P1 S P | P2 .
These closure properties are elementary from the point of view of interaction.
So Rc must satisfy the conditions 1 and 2 given after Definition 6. It should
also meet the following primary condition of observation:
3. If P1 SP2 then P1 can do a non-τ -action if and only if P2 can do a non-τ action.
Using a routine argument, it is easy to show that if R satisfies the conditions 1,
2 and 3 just stated, then the composition ∼; R; ∼ is a subbisimilarity.
The conclusion is that, from the viewpoint of Church-Turing Thesis, thesubbisimilarities are generalizations from the interpretations between the computation models to the interpretations between the interaction models in a right22

direction. The generalizations are not completely faithful in that both divergence and effectiveness are neglected. This is why we need to strengthen thedefinition of subbisimilarity later.

2.3

ChoiceIn practice the general choice operator + is rarely used. It is often sufficient to
use the mixed choiceX
λi .Eii∈I

where the indexing set I is finite. From a programming point of view, theseparated choiceXX
ai .Eiai .Ei ori∈Ii∈I

is even better. The operational semantics of the mixed (separated) choice isdefined by the following rule.
λii∈I λi .Ei −→ Ei

P

It is worth remarking that a.E+τ.F for example can be defined in terms of theseparated choices by (b)((a.E+b.F ) | b), where b is fresh.
We write CCSm and CCSs for the CCS with the mixed choice, respectively
the separated choice. In both CCSm and CCSs the prefix operator could be
dropped. The power of choice can be further restrained by removing all forms ofchoice operator altogether. Let CCS− be the CCS without the choice operator.
The actions of CCS− satisfy the following diamond property.
λ0λLemma 12. Suppose E is in CCS− . If E −→ E 0 and E −→ E 00 such that
λ 6= λ0 , λ is not an interaction at n(λ0 ) and λ0 is not an interaction at n(λ),λ0λthen E 0 −→ E 000 and E 00 −→ E 000 for some E 000 .
Proof. This is a simple induction on derivations.
Using similar induction one could prove similar result for CCSs .
ab

Lemma 13. Suppose E is a CCSs expression. If E −→ E 0 and E −→ E 00 ,bathen E 0 −→ E 000 and E 00 −→ E 000 for some E 000 .
It comes as no surprise that CCS− is strictly less expressive than CCSs
in terms of interactability. What is surprising is that CCSs and CCSm areequivalent interactively.
Proposition 1. CCS− @ccs CCSm vccs CCSs .

23

Proof. It is clear that CCS− vccs CCSm . We have to show that CCSm 6vccs
CCS− . Suppose that P is a process containing no choice operations and thataa+b ≈ P . To match up the action a+b −→ 0 there must be some P 0 such thatab
P =⇒ P 0 −→. Now P 0 ≈ a+b. Therefore P 00 exists such that P 0 =⇒ P 00 −→.
a
Since P 0 contains no choice operator, it follows from Lemma 12 that P 00 −→.
ab
But then it follows from the same lemma that P 00 −→−→, which contradicts00
the fact that P ≈ a+b.
Next we show that CCSm vccs CCSs . It is enough to explain how theencoding of the mixed choice is defined. Let R be a.P +b.Q. The interpretationof R is defined by the following induction.
def

JRK

=

a.P +τ.µY.(b.Q+τ.(a.P +τ.Y )).

(1)

Intuitively JRK and µY.(b.Q+τ.(a.P +τ.Y )) satisfy the following equations
XY≈ a.P +τ.Y,≈ b.Q+τ.X.

Obviously JRK ≈ a.P +b.Q in CCSm and JRK is in CCSs . This is a simple
application of Computation Lemma.
It is well known that CCS with guarded recursion is finite branching. A
slightly weaker restriction, the mixed choice, however is not sufficient to guarantee the finite branching property. The infinite branching property is importantwhen defining a process that behaves like a random timer. When left alone, arandom timer ticks on its own. If a process sets the timer by interacting with
it at a particular interface, the timer terminates after a finite number of ticks.
The number of ticks is set at random. In CCS a random timer can be defined
as follows:def
RanT imer = µX.(s + tick | X).
(2)
RanT imer can be set at the interface s. To see how it works, notice that thefollowing derivation is admissible.
ss+tick | µX.(s+tick | X) −→ 0s
µX.(s+tick | X) −→ 0stick | µX.(s+tick | X) −→ tick | 0ss+tick | µX.(s+tick | X) −→ tick | 0sµX.(s+tick | X) −→ tick | 0..
.
sµX.(s+tick | X) −→ tick | . . . | tick | 0
Another way to look at the operational behavior of RanT imer is to unfold it
for i times. It is the following process
s+tick | (s+tick | (. . . | (s+tick | µX.(s+tick | X)) . . .)).
|
{z}i times

24

So an action sequence of RanT imer typically looks like this:
tick

tick

s

tick

tick

RanT imer |−→ .{z. . −→} −→ −→. . −→} 0.
| .{zi times

j times

After RanT imer has been set at s, it may turn into one of an infinite numberof semantically different processes. This property makes the random timer aprime counter example to separate the expressive powers of process calculi.
The random timer is about ability to make a choice for the future, when thepotential choices are infinite.
Lemma 14. CCSm , CCSs and CCS are infinite branching.
Proof. RanT imer, defined in CCS, is infinite branching. The following transitionaµX.(a | X) −→ a | . . . | a | µX.(a | X)
shows that both CCSm and CCSs are infinite branching as well.
As long as the recursion is not guarded, infinite branching is present. But
there is a crucial difference between the two examples given in the proof of
Lemma 14. All the derivatives of RanT imer after performing s are semanticallydifferent from one to another. On the other hand all the derivatives of µX.(a | X)
are semantically equivalent. The latter fact is actually a particular instance ofa general phenomenon. To establish the fact, we need some technical lemmas.
Lemma 15. Suppose EhXi, F hXi are expressions in CCSm and that both thespecified occurrence of X in EhXi and the specified occurrence of X in F hXi
are unguarded. Then EhF hXii ∼ F hEhXii.
Proof. Suppose that E is in CCSm and that EhXi indicates an unguarded
occurrence of X. By structural induction it is easy to show that EhXi ∼Eh0i | X. Hence
EhF hXii∼∼∼∼

Eh0i | F hXi
Eh0i | F h0i | X
F h0i | EhXi
F hEhXii.

We are done.
If an action of (µZ.G){E/X} is caused by a copy of E, then the action
must be caused by an occurrence of E in the unfolding of (µZ.G){E/X}. Thisintuition is formalized by the next lemma.
λLemma 16. Suppose G[X], E, F are expressions in CCSm . If G[E] −→ F
is caused by an occurrence of E, then there exist some G1 hXi, E 0 , where theλspecified X is unguarded, such that G ∼ G1 hXi and G1 {E/X}hE/Xi −→λG1 {E/X}hE 0 /Xi ≡ F is caused by E −→ E 0 .
25

λProof. Suppose G[E] −→ F is caused by an occurrence of E. We may prove
the lemma by induction on derivation.
• G ≡ X. This case is obvious.
• G cannot be a choice since all the choices are guarded in CCSm .
• G ≡ (a)G0 or G ≡ G0 | G00 . These cases are simple by induction.
λ• G ≡ µZ.G0 . Then G0 {µZ.G0 /Z}[E] −→ F has a shorter derivation. By
induction, there exist some G1 hXi, E 0 such that the specified occurrence
λof X is unguarded, G0 {µZ.G0 /Z} ∼ G1 hXi and G1 {E/X}hE/Xi −→λG1 {E/X}hE 0 /Xi ≡ F is caused by E −→ E 0 . But then G ∼ G1 hXi.
We are done.
An action of E[E] is caused either by E[X] or by an occurrence of E that
substitutes for X. What is interesting is that the latter situation can be avoided
in favor of the former.
Lemma 17. The following statements are valid for every E[X] of CCSm :λ(i) If E −→ F then E[F [µX.E]] ∼ F [µX.E].
λ(ii) If E[E] −→ F then E[F [µX.E]] ∼ F [µX.E].
Proof. We focus on the proof of (ii). There are several cases since the action
could be caused by an occurrence of E or by an interaction. Let’s take a lookat two major cases.
λ• The action E[E] −→ F is caused by an occurrence of the outer E. By
Lemma 16, there exist some E1 hXi, E 0 , where the specified occurrence of
X is unguarded, E ∼ E1 hXi andλE1 {E/X}hE/Xi −→ E1 {E/X}hE 0 /Xi ≡ F
λis caused by E −→ E 0 . It follows from E ∼ E1 hXi that some E10 hXi
λexists such that E1 hXi −→ E10 hXi ∼ E 0 . Now
λE1 {E/X}hE1 hXi/Xi −→ E1 {E/X}hE10 hXi/Xi ∼ E1 {E/X}hE 0 /Xi.
Therefore
λE[E] −→∼∼

E 0 [E]E10 {E/X}hE1 hXi/Xi
E1 hE10 {E/X}hXi/Xi ≡ F

where the second structural bisimilarity is due to Lemma 15.
We are done.
26

The above three lemmas can now be exploited to prove the following usefullemma.
Lemma 18. Suppose E[X] is in CCSm . The following statements are valid.
λλ(i) If µX.E −→ E 0 for λ 6= τ , then E −→ F and F [µX.E] ∼ E 0 for some F .
ττ(ii) If µX.E −→ E 0 then E[E] −→ F and F [µX.E] ∼ E 0 for some F .
τProof. Suppose µX.E −→ E 0 . By Recursion Lemma (Lemma 2),
τE[E[. . . [E [X]] . . .]] −→ F 0 [X]| {z }
i times

for some natural number i and some F 0 [X] such that F 0 [µX.E] ≡ E 0 . Byτ
repeatedly using Lemma 17, we can get some F [X] such that E[E] −→ F [X]andF [E[E[. . . [E [X]] . . .]]] ∼ F 0 [X].
| {z }
i−2 times

It follows that F [µX.E] ∼ F 0 [µX.E] ≡ E 0 .
What Lemma 18 tells us is that the one-step derivatives of µX.E are essentially the one-step derivatives of E[E]. This is the crucial property of the infinite
behaviors of CCSm . In the following proposition, Drv1 (E)/ ∼ is the quotient of
the set of the one step derivatives of E with respect to the structural bisimilarity∼.
Proposition 2. The quotient Drv1 (E)/ ∼ is finite for every process expression
E of CCSm .
Proof. We prove the result by a structural induction.
• If E is a mixed choice, Drv1 (E) is obviously finite.
• If E is of the form (a)E 0 , a simple induction suffices.
• If E is of the form E1 | E2 , we use induction hypothesis and the congruence
property of ∼.
• Suppose E is of the form µX.E1 . We prove by induction on the numberof the µ-operators that Drv1 (µX.E1 )/ ∼ is finite. The base case is when
E1 is free of the µ-operator. By the proof of the previous cases and theassumption that E1 does not contain any µ-operator, Drv1 (E1 [E1 ])/ ∼ isfinite. It follows from Lemma 18 that Drv1 (µX.E1 )/ ∼ is finite. Putting
together what we have obtained so far we conclude that Drv1 (E)/ ∼ isfinite for every E containing no more than one µ-operator.
Now assume that for all CCSm expressions F that contain at most i µoperators, Drv1 (F )/ ∼ is finite. The argument is made in two steps.

27

– Let F0 [X1 , .., Xm ], F1 , . . . , Fm be CCSm expressions that contain at
most i µ-operators. By structural induction it is easy to prove thatDrv1 (F0 [F1 /X1 , .., Fm /Xm ])/ ∼ is finite.
– Suppose that E1 contains i µ-operators. By the above property, thequotient Drv1 (E1 [E1 ])/ ∼ is finite. We conclude from Lemma 18
that Drv1 (µX.E1 )/ ∼ is finite.
The structural induction is complete.
Proposition 2 appears to be new. It is also valid of course for CCSs .
2.3.1

Termination Preserving Encoding

The encoding (1) given in the proof of Proposition 1 is assuring from an external point of view. No environments can ever detect any difference between
P and JP K. There is however something lost over the translation. The process
a.P +b.Q is translated to a.P +τ.µY.(b.Q+τ.(a.P +τ.Y )) which is divergent. The
point is that although the divergent computations introduced by the encoding
only go through states that are equivalent to the initial state, there is somedifference between a possibly divergent computation and an always terminating
computation. One is interested in knowing if Proposition 1 can be strengthened
to meet Computation Criterion.
The issue of divergence has been studied in the process theory. There arebasically two approaches. In the explicit approach applied for example in [4, 63]
a divergent process, say Ω, is introduced at the syntactical level, and a divergence
predicate is defined on the structures of the processes. This predicate is thenused in the definition of the equivalence relations. In the implicit approachsummarized by van Glabbeek in [25] divergence is treated at the operational
level. In this approach a straightforward requirement would be the following:
If P RQ then P is divergent if and only if Q is divergent.
This condition completely ignores the bisimulation nature of the subbisimilarity.
The right termination property that is consistent with the notion of bisimulationis the one discussed in Section 2.2.2.
Definition 7. A subbisimilarity R from CCS1 to CCS2 is codivergent if itmeets the Computation Criterion in the following sense.
τ

τ

τ

τ

τ

τ

If P RQ and P −→ P1 −→ P2 −→ . . . is an infinite computation,τthen Q =⇒ Q0 R−1 Pk for some Q0 and some k ≥ 1.
If P RQ and Q −→ Q1 −→ Q2 −→ . . . is an infinite computation,τthen P =⇒ P 0 RQk for some P 0 and some k ≥ 1.
2
1
2
We write CCS1 vccs
↓ CCS if a codivergent subbisimilarity from CCS to CCS
1
2
1
2
2
1
ccs
ccs
ccs
exists, and CCS @↓ CCS if CCS v↓ CCS yet CCS 6v↓ CCS .

28

The codivergence property defined above is essentially the eventually progressing property of Priese [52].
The next theorem says that one must be ready to sacrifice Computation
Criterion if the use of the choice is restricted.
m
ccs
Proposition 3. CCSs @ccs
↓ CCS @↓ CCS.
m
ccs
Proof. Clearly CCSs vccs
↓ CCS v↓ CCS. We have to prove that there are no
codivergent subbisimilarities from CCS, respectively CCSm , to CCSm , respectively CCSs .
Suppose that P is a terminating process with only separated choice. We
argue that P is not bisimilar to a+b. If P were bisimilar to a+b, then for eachτ
P 0 such that P =⇒ P 0 and ¬(P 0 −→), one would have that P 0 ≈ a+b, whichabwould imply that P 0 −→ and P 0 −→. This is a contradiction according toLemma 13.
Next we prove that the random timer RanT imer, which is terminating, is
not bisimilar to any terminating process in CCSm . Suppose that RanT imer
were bisimilar to some terminating P of CCSm . Let P 0 be such that P =⇒ P 0
and that P 0 cannot do any tau action. Clearly RanT imer ≈ P 0 . According to
Proposition 2, there are only finitely many semantically distinct Pi , where i ∈ Isfor some finite I, such that P 0 −→ Pi . For each i ∈ I there would exist someji < ω such thats

RanT imer −→ tick | . . . | tick | 0 ≈ Pi .
|{z}ji timess

Let j be such that j > supi∈I {ji }. It is clear that the action RanT imer −→Q0j tick cannot be matched up by any action of P .
2.3.2

Mixed Choice and Guarded Recursionm

In CCS process variables can be unguarded. One way to use a more manageable operational semantics is to use the guarded fixpoint. A fixpoint is guarded
if all its bound process variables are guarded. Let CCSgµ be CCS with theguarded recursion and CCSgm be CCSm with the guarded recursion. We shallprove below that all CCSm processes are definable in CCSgm . In this subsection
we will write !E for µZ.(E | Z) for some Z that does not appear in E.
The next lemma describes some of the most important properties of !E.
Lemma 19. !P ∼ P | !P ; !!P ∼ !P ; !(P | Q) ∼ !P | !Q; and !0 ∼ 0.
In the proof of the main result of this subsection, we shall make use of several
auxiliary results about CCSm . These results are stated in the following lemmas
and corollaries.
Lemma 20. Suppose E is a CCSm expression containing X. Then µX.(X | E) ∼µX.(X | E{0/X}).

29

Proof. Let µ be µX.(X | E) and µ0 be µX.(X | E{0/X}). Define R to be therelationG[X] is in CCSm ,YY.
( µ | G[µ],µ0 | G[0]) X is guarded in G[X],ijand i, j ≥ 1
Q
λNow suppose that i µ | G[µ] −→ H. If the action is caused by G[µ], it must
be caused by G[X] since X is guarded in G[X]. Therefore some G0 [X] exists
QQλλsuch that G[X] −→ G0 [X] and i µ | G0 [µ] ≡ H. But then j µ0 | G[0] −→Q00
j µ0 | G [0]. If an occurrence of X in G [X] is unguarded, then by Lemma 3
one has that G0 [X] ∼ G00 [X] | X for some G00 [X]. It follows easily from thisobservation thatYY
µ | G0 [µ] ∼ R ∼µ0 | G0 [0].
i

j
λ

Q

If the action i µ | G[µ] −→ H is caused by a component of
induced by someλµ −→ µ | E 0 [µ]Qi µ, it must be(3)

λwhich is in turn induced by E −→ E 0 . Now (3) can be simulated byλµ0 −→ µ | E 0 [0].

(4)Conversely (4) can be simulated by (3).
The above analysis suffices to show that R is a strong bisimulation up to ∼.
By letting G be 0 and i = j = 1, we get that µ ∼ µ0 .
Lemma 20 is a powerful result. It allows one to derive a number of interesting
properties of the fixpoints µX.E whenever E ∼ X | E 0 for some E 0 . Some ofthese properties are stated in the following corollaries. The intuition behindthese corollaries is that µX.(X | E) is structurally equivalent to !E{0/X}.
Corollary 1. µX.(X | . . . | X | E) ∼ µX.(X | E) if E is an expression of CCSm .
| {z }i≥1Corollary 2. µX.(!X | E) ∼ µX.(X | E) if E is an expression of CCSm .
Corollary 3. Suppose that X does not appear free in A. Then µX.(X | A | E) ∼!A | µX.(X | E) whenever A, E are in CCSm .
Proof. By Lemma 20, one has thatµX.(X | A | E) ∼ µX.(X | A | E{0/X})∼ !A | !E{0/X}∼ !A | µX.(X | E)
where the second equivalence is due to Lemma 19.
30

What the previous lemma and corollaries achieve is the simplification ofan expression, in some particular form, underneath a fixpoint operator. If an
expression E cannot be converted to some expression of the form X | E 0 , it isstill possible to manipulate the scope of the µ-operator of µX.E. The following
lemmas explain how we may go about it.
Lemma 21. Suppose that X is guarded in E and that it does not appear freein A. Then µX.(A | E) ∼ A | µX.E{A | X/X}.
Proof. Let µ1 abbreviate µX.(A | E) and µ2 abbreviate µX.E{A | X/X}. Let
R be the following relation{(G[µ1 ], G[A | µ2 ]) | G[Z] an expression} .
λSuppose G[µ1 ] −→ H. Since X is guarded in E, there are only three possibilities
for the cause of the action.
λλλ• G[µ1 ] −→ G0 [µ1 ] is caused by G −→ G0 . The simulation is G[A | µ2 ] −→G0 [A | µ2 ] R−1 G0 [µ1 ].
λλ• G[µ1 ] −→ G0 [A0 | E[µ1 ]] is caused by A −→ A0 . The simulation isG[A | µ2 ]

λ

−→
∼
R−1

λ

G0 [A0 | µ2 ]G0 [A0 | E[A | µ2 ]]G0 [A0 | E[µ1 ]].
λ• G[µ1 ] −→ G0 [A | E 0 [µ1 ]] is caused by E −→ E 0 . The simulation isG[A | µ2 ]

λ

−→
R−1

G0 [A | E 0 [A | µ2 ]]G0 [A | E 0 [µ1 ]].

We conclude that R is a structural bisimulation up to ∼.
If the environment has the process expression !R, say a piece of universal
resource, a neighboring process expression does not have to store a copy of R
beside it. It can simply make use of R when necessary.
Lemma 22. E{R/X} | !R ∼ E{0/X} | !R whenever E is in CCSm .
Proof. It can be easily proved that G | H{0/X} | !R is structurally bisimilar to
G | H{R/X} | !R for all expressions G, H in CCSm .
In a structural approach to translations of CCSm processes to CCSgm processes, process expressions like µZ.(X | Z) have to be dealt with. However thetranslations of such expressions have to be delayed until the variable binder µX
appears. In the middle of translating a CCSm process to a CCSgm process, theprocess expression we get looks almost in CCSgm except that it may contain
subexpressions of the form µZ.(X | Z). This is the reason we introduce thefollowing terminology.
31

Definition 8. A bound process variable Z in E is quasi-guarded if it is either
guarded or is the bound process variable of an expression of the form µZ.(Y | Z)
or µZ.(Z | Y ) for some process variable Y . An expression E is quasi-guarded if
all free process variables in E are guarded and all bound process variables in E
are quasi-guarded. An expression is in quasi normal form if it is of the form
(

k
Y

h=1

p
Y
(Xh | . . . | Xh )) | ( !Yg ) | F
{z
}
|
g=1
ih

such that k, p, i1 , . . . , ik are non-zero natural numbers and the following statements are valid.
1. X1 , . . . , Xk , Y1 , . . . , Yp are pairwise distinct process variables.
2. F is quasi-guarded.
So a quasi-guarded bound process variable is either guarded or to provide areplication of a process variable. We now prove that subexpressions like !Y canbe removed. For that purpose we define a syntactical operation on the processexpressions by the following induction.
0•X

def

•X

def

=

Y,

•X

def

E1•X | E2•X ,X
λi .(X | Ei•X ),Y(E1 | E2 )X(
λi .Ei )•X

=

=

def

=

i∈I

0,

i∈I
•X

def

=

(a)E •X ,(µZ.E)•X

defµZ.E •X .

((a)E)=The operation ( )•X inserts a copy of X right after every prefix. In what follows,
it is only applied to process expressions in which free occurrences of X have all
been removed. So we introduce the following notation:def

E ◦X = (E{0/X})•X .
It should be clear that E ◦X does not contain any subexpressions of the form !Xand that X is guarded in E ◦X . Operationally E •X enjoys the property statedin the following lemma.
Lemma 23. Suppose that E is an expression in CCSm and that X does notλλappear free in E. If E •X −→ H then E −→ H1 for some H1 such that H ∼X | H1•X .
Proof. Using the fact that (E{F/X})•X is the same as E •X {F •X /X}, one could
prove the lemma by induction on derivation.
32

We can now make use of the operations ( )•X and ( )◦X to state some important properties about CCSm .
Lemma 24. If E is an expression in CCSm and X does not appear free in E,
then !E ∼ µX.(E •X ) | µX.(E •X ).
Proof. Let µ• abbreviate µX.(E •X ). Define R to be the following relation

G[X] is in CCSm ,Y.
(!E | G[0],µ• | G[µ• ]) X is guarded in G[X],i
and i ≥ 2
We claim that R is a structural bisimulation up to ∼. Suppose that G[µ• ]performs an action λ. Since X is guarded in G[X], the action λ must be induced
λby G[X] −→ G0 [X]. Clearly in this case the actionYλµ• | G[µ• ] −→iYµ• | G0 [µ• ]iλλis simulated by !E | G[0] −→ !E | G0 [0]. Now suppose that µ• −→ H. Since X
does not appear free in E, the variable X must be guarded in E •X . It follows
λλfrom E •X [µ• ] −→ H that E •X −→ H 0 and H ≡ H 0 {µ• /X} for some H 0 . By
λLemma 23, one has that E −→ H1 and H 0 ∼ X | H1•X for some H1 such that
X is guarded in H1 . ConsequentlyYYYλµ• | G[µ• ] −→µ• | H | G[µ• ] ∼µ• | H1•X [µ• ] | G[µ• ],
i

i

i+1

which is simulated by
λ!E | G[0] −→ !E | H1 | G[0] ∼ !E | H1•X [0] | G[0].
Due to the guardedness, the proofs of the other cases can be safely omitted.
Lemma 24 says that !E can be equivalently presented in a more controlledmanner. Instead of introducing an infinite copies of E, one could introduce twocopies of µX.(E •X ). The latter is more manageable than the former for thereason that X is guarded in E •X .
We mentioned before that when converting a process of CCSm to a processof CCSgm , an expression like !Y has to be left intact until a binder µY props
up. But when the binder µY does appear, how do we eliminate !Y in favorof the guarded recursions? When unfolding µY.E, the subexpression !Y of E
becomes !µY.E. The first step could be to manipulate !µY.E into a shape thatis considerably simpler.
Lemma 25. If E is an expression in CCSm , then !µX.E ∼ !E{0/X}.

33

Proof. Generally F | !µX.E ∼ F | !E{0/X} for every process expression F inλCCSm . An action of !µX.E must take the form !µX.E −→ E 0 [µX.E] | !µX.E.
So the action
λF | !µX.E −→ F | E 0 [µX.E] | !µX.E ∼ F | E 0 {0/X} | !µX.E
λis simulated by F | !E{0/X} −→ F | E 0 {0/X} | !E{0/X}, where the equivalence
is due to Lemma 22.
Corollary 4. µX.E ∼ µX.E{(µX.E ◦X | µX.E ◦X )/!X} whenever E is in CCSm
and X is guarded in E.
Proof. The following equivalences are due to Lemma 24 and Lemma 25:
µX.E

∼
≡
∼
∼

E{µX.E/X}
E{!µX.E/!X}{µX.E/X}
E{!E{0/X}/!X}{µX.E/X}
E{(µX.E ◦X | µX.E ◦X )/!X}{µX.E/X}.

What the equivalences say is that µX.E is a fixpoint of the equation
X ∼ E{(µX.E ◦X | µX.E ◦X )/!X}.
Since X is guarded in E, one could apply the fixpoint lemma (Lemma 10) to
conclude that µX.E ∼ µX.E{(µX.E ◦X | µX.E ◦X )/!X}.
Let’s see an example. Suppose E ≡ µX.(a.X + a.!X). Then we have thefollowing rewriting:
E

∼
∼
∼
∼

a.E + a.!E
a.E + a.!(a.0 + a.!0)
a.E + a.!(a + a)a.E + a.(µX.(a.X + a.X) | µX.(a.X + a.X)).

Now E ∼ µX.(a.X+a.(µX.(a.X+a.X) | µX.(a.X+a.X))) follows from Lemma 10.
We are now in a position to prove the major lemma of this subsection.
gm
Lemma 26. CCSm vccs.
↓ CCS

Proof. Let E be in CCSm . We show by structural induction that E must be
structurally bisimilar to some process expression in quasi-normal form:
(

k
Y

h=1

p
Y
(Xh | . . . | Xh )) | ( !Yg ) | F.
|
{z
}
g=1

(5)

ih

Notice that Yg is not guarded in !Yg . But subexpressions of this form !Yg willbe thrown away on the way of converting a process in CCSm to a process in
CCSgm . The conversion is defined structurally by the following clauses.
34• If E is a mixed choice, it is already in the form of (5).
• If E ≡ E1 | E2 , then a simple application of the induction suffices. Boththe conversions of E1 and E2 may contain !Y . The strong equivalence!Y ∼ !Y | !Y is necessary to replace the two occurrences of !Y by !Y .
• If E is a restriction, then a simple application of the induction suffices.
• If E ≡ µX.E1 then by induction E1 must be structurally bisimilar to somequasi-normal form
k
Y
h=1

p
Y

!Yg | F1 .
(Xh | . . . | Xh ) |
{z
} g=1
|
ih

It follows by congruence thatE ∼ µX.(

k
Y

h=1

p
Y
(Xh | . . . | Xh ) |!Yg | F1 ).
{z
} g=1
|
ih

We are now converting
k
Y

µX.(

h=1

p
Y
(Xh | . . . | Xh ) |!Yg | F1 )
|
{z
} g=1

(6)

ih

into a structurally bisimilar quasi-normal form. The conversion of the
fixpoint can be defined in three cases.
– X 6∈ {X1 , . . . , Xk , Y1 , . . . , Yp }. According to Lemma 21 and Lemma 22,
the expression (6) is in this case structurally bisimilar tokY
h=1

where F1◦ is F1 {p
Y(Xh | . . . | Xh ) |!Yg | µX.F1◦
|
{z
} g=1
ih

Qk

h=1 (Xh | . . . | Xh ) | X/X}. Since every free process

|

{z
ih

}

variable in F1 is guarded, every free process variable, as well as X, inµX.F1◦ must also be guarded. Now using the following equivalence!(V1 | . . . | Vm ) ∼ !V1 | . . . | !Vmstated in Lemma 19 to convert the expression so that the induced
operator “!” applies only to individual variables. Moreover we may
apply Corollary 4 to remove all the occurrences of !X. The result isa quasi-normal form F1 structurally bisimilar to µX.F1◦ . So in thiscase (6) is structurally bisimilar to
k
Y
h=1

p
Y
(Xh | . . . | Xh ) |!Yg | F1 .
|
{z
} g=1
ih

35

(7)

– X = X1 . By using Corollary 1, Corollary 3, Lemma 20 and Lemma 19,
the expression (6) can be converted to
k
Y
h=2

!Xh |

p
Y

!Yg | µX.(X | F1 {0/X}).

(8)

g=1

By Lemma 24, the expression (8) is structurally bisimilar to
k
Y

!Xh |

p
Y

!Yg | F1

(9)

g=1

h=2

where F1 is the process expression µX.F1◦X | µX.F1◦X .
– X = Y1 . According to Corollary 2, Corollary 3, Lemma 20, Lemma 19
and Lemma 24, the expression (6) is structurally bisimilar to
k
Y

!Xh |

h=1

p
Y

!Yg | F1

(10)

g=2

where F1 is the process expression µX.F1◦X | µX.F1◦X .
It is clear from (7), (9) and (10) that E is structurally bisimilar to a quasinormal form. In (9) and (10) the bound variable X does not occur in any
subterm of the form !X. In (7) however such occurrence is possible. But
according to Corollary 4, these occurrences can be eliminated.
Now given a process P in CCSm , the structural conversion defined above allows
us to find a process P 0 that is structurally bisimilar to P . The process P 0 could
contain !0, which can be replaced by 0 of course. Therefore P is structurally
bisimilar to a guarded process in CCSgm .
The proof of Lemma 26 actually provides an effective procedure to convert
a CCSm process to a CCSgm process. Let’s see an example. Suppose F ≡Z | !X | !Y | (a.X + a.!X) and E ≡ µX.F . We may apply the following rewriting:
E

≡
∼
∼
∼
∼
∼
∼

µX.(Z | !X | !Y | (a.X + a.!X))µX.(X | Z | !Y | (a.X + a.!X))!(Z | !Y ) | µX.(X | (a.X + a.!X))!Z | !Y | µX.(X | (a.X + a.!X))!Z | !Y | µX.(X | (a.0 + a.!0))!Z | !Y | µX.(X | (a + a))!Z | !Y | µX.(a.X + a.X) | µX.(a.X + a.X).

The component µX.(a.X + a.X) | µX.(a.X + a.X) is in CCSgm . When applying
our conversion, the expression E is typically sitting inside a process in which
Y, Z are bound. Further conversions would deal with the components !Z, !Y .
36

Corollary 5. There is an algorithm I gm such that, for each CCSm process P ,I gm (P ) returns a CCSgm process that is structurally bisimilar to P .
The bulk of this section is devoted to dealing with the choice operator.
Without the choice operator Corollary 5 is much easier to prove. See [9] for a
proof of a similar result in Ambient Calculus which is of course choice free.
The above exercise suggests that the recursion semantics of CCSm can bealternatively defined by the following rule.
λE{E/X} −→ E 0
λµX.E −→ E 0 {µX.E/X}
It gives rise to a simpler semantics that enjoys the finite branching property.

2.4First Order Recursion

The result in Section 2.3.2 suggests to introduce the replication processes ofthe form !P at the syntactic level. This is what Milner did in [44], which was
actually motivated by a similar operation in linear logic [24]. Milner has defined
the semantics of the replicator by the following rule.
λP | !P −→ P 0
λ!P −→ P 0
The advantage of this rule is that it makes obvious the validity of the equivalence!P ∼ P | !P . Intuitively !P is the same as P | !P . In other words !P provides apotentially infinite number of copies of P . However the above rule introduces
infinite branching at the syntactical level, just like the unguarded recursion in
CCSm . One way to retain the finite branching property is to use the following
rule.
λP | P −→ P 0
λ!P −→ P 0 | !P
One may also use the following rules due to Busi, Gabbrielli and Zavattaro [7].
λP −→ P 0
λ!P −→ P 0 | !Paa

P −→ P 0 P −→ P 00
τ
!P −→ P 0 | P 00 | !P

It is easy to see that the three formulations of the replication are equivalent.
Let CCS! , respectively CCSm! and CCSs! , denote the variant of CCS, respectively CCSm and CCSs , whose infinite behaviors are defined by the replicator.
Our agenda in the present subsection is to work out the relative expressive powerof these variants.
One obvious advantage of using the replication instead of the fixpoint operation is that one could give a purely first order presentation of CCS. There isno need for process variables. This is why the above rules are defined on the setof processes, not on the set of expressions.
37

Let depth() ( ) be the function that returns the maximum number of nested
localization operations. It can be inductively defined as follows.
depth() (0) = 0,
depth() (λ.P ) = depth() (P ),depth() (P | P 0 ) = max{depth() (P ), depth() (P 0 )},depth() ((a)P ) = depth() (P ) + 1,
depth() (P +P 0 ) = max{depth() (P ), depth() (P 0 )},depth() (!P ) = depth() (P ).
A useful property of the replication is that the depth of the nested localization
operations in a process remain fixed over process evolution.
λLemma 27. Suppose P is in CCS! . If P −→ P 0 then depth() (P 0 ) = depth() (P ).
By Lemma 27, new nesting of localization operations is never created dynamically, rendering α-conversion unnecessary.
2.4.1

Expansion Property of Replication

First let’s take a look at a simple but illustrating example. Consider an arbitrarydef
infinite action sequence of the process A = b.a | !a.b | !b.a, say
b

τ

τ

τ

A −→ a | !a.b | !b.a −→ b | !a.b | !b.a −→!a.b | a | !b.a −→ . . . .
There appears some kind of periodicity in the infinite number of processes.
Both a | !a.b | !b.a and !a.b | a | !b.a have the same set of concurrent components{a, !a.b, !b.a}. Obviously !a.b | a | !b.a can do whatever a | !a.b | !b.a can do. This isa special case of a general phenomenon in CCS! : For an infinite action sequence
λ

λ

λ

0
1
2
A0 −→
A1 −→
A2 −→
...

in CCS! , there must exist two processes Ai , Aj , where i < j, such that Aj
contains everything Ai has. In other words, Aj can do whatever Ai can do. This
interesting property of the replication was first pointed out by Busi, Gabbrielli
and Zavattaro in [7]. In the terminology of order theory, it says that the set ofthe derivatives of a process of CCS! is a well quasi-order. This property is of
crucial importance to some of the counter examples given later on in the paper.
Busi and Zavattaro have provided in [9] a detailed proof that an expansion orderdefined for certain ambients is a well quasi-order. For the benefit of the reader,
below we give a self-contained account of this property.
In the rest of the subsection we introduce a syntactic order on the CCS! processes. This syntactic order formalizes the intuition that one process contains
every concurrent component of another. The adequacy of the formalization is
supported by the Compatibility Lemma. We prove the Expansion Lemma sayingthat the set of the derivatives of a CCS! -process is a well quasi-order under this38

order relation. It then follows that every infinite action sequence contains an
infinite chain of processes with increasing interactive capacities.
Let’s start with something in order theory [13, 37].
Definition 9. A quasi-order (X, ≤) is a binary relation ≤ that is reflexive andtransitive.
An important concept that is most relevant to us is the well quasi-order
structure [37].
Definition 10. A well quasi-order (X, ≤) is a quasi-order such that, for any
infinite sequence x0 , x1 , x2 , . . . in X, there exist indexes i < j with xi ≤ xj .
The main reason that a well quasi-order is an interesting structure is thefollowing property.
Lemma 28 (Erdös and Rado). Suppose (X, ≤) is a well quasi-order. An infinite
sequence x0 , x1 , x2 , . . . in X must contain an infinite increasing subsequencexi0 ≤ xi1 ≤ xi2 ≤ . . ., where i0 < i1 < i2 < . . ..
Proof. Suppose x0 , x1 , x2 , . . . is an infinite sequence in X. Consider the set{xi | ∀j > i.xi 6≤ xj }. By the definition of the well quasi-order, this set cannot
be infinite. Then an element beyond all the elements of this set starts an infinite
increasing sequence.
Finkel and Schnoebelen have surveyed in [17] some applications of the wellquasi-order structure in theoretical computer science.
We are going to define a quasi-order on CCS! processes, which turns out
to be a well quasi-order. To simplify the account, we make two syntacticalassumptions in the rest of this subsection. First of all we assume that all the
local names are distinct from all the global names in consideration. Moreover αconversion is not applied when a process replicates part of itself. This is harmlessin view of the remark after Lemma 27. Secondly we identify syntactically two
processes up to the symmetry and associativity of the compositions. We write
A = B if B can be rewritten from A, or vice versa, by applying the following
equalities
P | Q = Q | P,
P | (Q | R) = (P | Q) | R.

(11)
(12)

The proof of the following lemma is a routine induction on the number of rewriting steps.
λλLemma 29. If P = Q −→ Q0 then P −→ P 0 = Q0 for some P 0 .
The equalities (11) and (12) can be applied to convert every CCS! process
to a normal form.

39

Definition 11. Suppose that P is a CCS! process. A concurrent normal formof P is some
Y
Pi
i∈I

Q
such that P = i∈I Pi and, for each i ∈ I, Pi is not a composition. We saythat Pi , for each i ∈ I, is a concurrent component of P .
The terminology “normal forms” usually implies uniqueness up to someequivalence. Hence the following lemma.
Lemma 30. The concurrent normal form of a CCS! process is unique up to =.
By the above definition, in the following process
λ1 .A | !R | (c)(λ2 .B | !S) | λ3 .λ4 .(a.C | b.D)

(13)

there are four concurrent components. They are λ1 .A, !R, (c)(λ2 .B | !S) andλ3 .λ4 .(a.C | b.D) respectively. If the process (13) performs the λ3 action, then
λ4 .(a.C | b.D) becomes a concurrent component. If the process continues todo the λ4 -action, then the concurrent component λ4 .(a.C | b.D) splits to two
concurrent components a.C, b.D. Similarly !R may induce an action and produce new concurrent components. However there are only a finite number ofsyntactically distinct concurrent components ever created since every concurrent component is a sub-term of the process (13). This example leads to thefollowing definition [8].
Definition 12. The set of concurrent subexpressions of A, denoted by Csub(A),is defined by the following structural induction.
def

=

{0},

0

def

=

{λ.A0 } ∪ Csub(A0 ),Csub(A0 | A00 )def=

Csub(A0 ) ∪ Csub(A00 ),Csub(A0 +A00 )def={A0 +A00 } ∪ Csub(A0 ) ∪ Csub(A00 ),Csub((a)A0 )def=

Csub(A0 ),Csub(!A0 )def{!A0 } ∪ Csub(A0 ).

Csub(0)Csub(λ.A )=A concurrent subexpression is neither in composition form nor in localization
form. It is intuitively clear that Csub(A) is finite for each process. To appreciate
the next lemma, it is important to bear in mind that α-conversion is not used
when a subexpression is duplicated by an action.
Lemma 31. For each process P of CCS! , Csub(P ) is finite; and moreoverS0
P 0 ∈Drv(P ) Csub(P ) = Csub(P ).
Lemma 31 gives us a hint on how one might get a well quasi-order: One
could introduce an order relation that compares the sets of the occurrences of
the concurrent subexpressions in a structural way. This important syntactic
order relation were first proposed by Busi, Gabbrielli and Zavattaro [7].
40Definition 13. The syntactical expansion  on CCS! processes is defined inductively as follows:• P  P;• P  Q whenever Q = P | R;
• (c)P  (c)Q whenever P  Q;
• P  Q whenever P = P0 | P1 , Q = Q0 | Q1 , P0  Q0 and P1  Q1 .
Notice that in our approach we do not have 0 | P  P since we do notequate 0 | P with P syntactically. The absence of 0 | P = P simplifies some of
the arguments below. The next lemma for example follows immediately fromthe definition.
Lemma 32. If (c)P  A and A is not a composition then there exists some Q
such that A ≡ (c)Q.
The following is a useful lemma about the relation 6 that allows one to
reduce the size of the processes being compared.
Lemma 33. Suppose P0 | P1 6 Q0 | Q1 for processes P0 , P1 , Q0 , Q1 in CCS! . If
P1  Q1 then P0 6 Q0 .
The expansion order is transitive. Hence the following lemma.
Lemma 34. For each process P of CCS! , (Drv(P ), ) is a quasi-order.
Intuitively P  Q means that Q contains at least as many possible individual
processes running concurrently as P . The property described in the next lemmais called compatibility in [17].
Lemma 35 (Compatibility Lemma). Suppose that P, Q are CCS! processes. IfλλP  Q and P −→ P 0 then Q0 exists such that Q −→ Q0 and P 0  Q0 .
Proof. The lemma can be proved by a simple induction on the depth of thenested localization operations.
We have done all the preparations for the main lemma of this subsection.
The Expansion Lemma proved below is one of the key technical lemmas inclassifying the expressive power of CCS variants.
Lemma 36 (Expansion Lemma). For each process P of CCS! , (Drv(P ), ) isa well quasi-order.
Proof. Recall that Drv(P ) is the set of all the derivatives of P , including P
itself. We will prove the lemma by contradiction. Assume that in CCS! there
were an infinite sequence of processes
A0 , A1 , . . . , Ap , . . .
41

(14)

such that ∀m, n.m<n ⇒ Am 6 An . For each p ≥ 0, let
Y
Aip
i∈Ip

be Q
the concurrent normal form of Ap . Now consider the concurrent componentsof i∈I0 Ai0 . There are two possibilities:
Q• I0 is the singleton set {∗}. Then i∈I0 Ai0 contains a single concurrent
component A∗0 . By the assumption the following proposition holds∀p>0.∀i∈Ip .A∗0 6 Aip .
Let B0 be A∗0 in this case. We then continue to examine the infinite
sequence A2 , A3 , . . . , Ap , . . ..
• Q
The size of I0 is greater than 1. Let Ai00 be a concurrent component ofi0
ii∈I0 A0 . If A0 leads an infinite increasing sequenceip

iAi00  App11  . . .  Apkk  . . .

(15)

ip

where p1 < p2 < . . . < pk < . . . and Apkk is a concurrent component ofQii∈Ipk Apk , then according to Lemma 33 we may continue to examine theinfinite sequence
Y
Y
Y
Ai0 ,
Aip1 , . . . ,Aipk , . . . .
i∈I0 \{i0 }i∈Ip1 \{ip1 }i∈Ipk \{ipk }Notice that the number of the concurrent components ofQsmaller than that of i∈I0 Ai0 .

Qii∈I0 \{i0 } A0 is

If Ai00 does not lead any infinite increasing sequence like (15), then thereQimust exist some q > 0 and some concurrent component Aqq of i∈Iq Aiq
such that the following proposition holds∀p>q.∀i∈Ip .Aiqq 6 Aip .
i

Let B0 be Aqq in this case. We then continue to examine the infinite
sequence
Aq+1 , Aq+2 , . . . , Aq+k , . . . .
By the above construction we eventually obtain an infinite sequence
B0 , B 1 , . . . , B k , . . .
such that Bk0 6 Bk00 whenever 0 ≤ k 0 < k 00 and Bk contains a single concurrent
component for each k ≥ 0. In view of Lemma 31 and Lemma 32, we can subtractfrom this sequence an infinite subsequence
B r0 , B r1 , . . . , B rk , . . .
that satisfies either of the following conditions.
42

1. Brk is not in localization form for each k ≥ 0.
2. There exists some d such that Brk ≡ (d)Br0 k for all k ≥ 0.
The first case would lead to a contradiction by Lemma 31. The second casewould eventually lead to the same contradiction by Lemma 32 and Lemma 27
since we can repeat the above construction to Br0 0 , Br0 1 , . . . , Br0 k , . . ..
Lemma 36 and Lemma 28 immediately imply the following proposition.
Proposition 4. Suppose that P is a process in CCS! . If P0 , P1 , P2 , . . . is an
infinite sequence in (Drv(P ), ), then there is an infinite increasing subsequence
Pi0  Pi1  Pi2  . . ., where i0 < i1 < i2 < . . ..
Let’s say that an infinite action sequence
λ

λ

λ

0
1
2
A0 −→
A1 −→
A2 −→
...

in CCS! is well quasi-ordered if there is an infinite subsequence satisfying
Ai0  Ai1  Ai2  . . .
where i0 < i1 < i2 < . . .. Proposition 4 says that every infinite action sequencein CCS! is well quasi-ordered.
2.4.2

Replication and Mixed Choice

The relationship between the replicator and the fixpoint operator is obvious
when both choice and recursion are guarded.
Fact 1 (Milner [44]; Giambiagi, Schneider, Valencia [27]). CCS! vccs
↓ CCS andgmm!
ccs
CCS v↓ CCS .
Proof. Intuitively !P of CCS! can be interpreted in CCS as µX.(P | X). Conversely an encoding I ! from CCSgm to CCSm! is homomorphic on the nonfixpoint operators. It maps µX.E onto (d)(E{d/X} | !d.E{d/X}), where d does
not occur in E.
The above encoding provides an algorithm I ! that converts a CCSgm process
P to a CCS! process I ! (P ) that is bisimilar to P . The composition I ! I gm is analgorithm that converts a CCSm process to a CCS! process.
There are two points worth making about the encoding from CCSgm to
CCSm! . Firstly the encoding does not work for CCS. The process b + µX.(a | X)
would be encoded by b + (d)(d | !d.(a | d)), which has to be wrong since it has
the preemptive power to get rid of a. Secondly the encoding works for CCSm ,but it does not provide a termination preserving encoding. The interpretation of the terminating process µX.(a | X) for instance is the divergent process(d)(d | !d.(a | d)).
The result stated in Fact 1 can be strengthened significantly. In one direction
we have the following lemma.
43gm
Lemma 37. CCS! vccs.
↓ CCS

Proof. In view of Lemma 26, it is enough to define an encoding J K from CCS!
to CCSm . For every process P of CCS! , the translation JP K is a guarded choicedefinable in CCSm . The encoding J K is defined structurally:def• P ≡ 0. In this case, J0K = 0.
def

• P ≡ λ.P 0 . In this case, JP K = λ.JP 0 K.
P
• P ≡ P1 | PP
2 . By induction JP1 K is of the formi∈I1 λi .Qi and JP2 K is of
the form i∈I2 λi .Qi such that I1 ∩ I2 = ∅. Let JP K beλi =λjXi∈I1λi .(Qi |JP2 K) +Xi∈I2

λi .(JP1 K|Qi ) +X

τ.(Qi |Qj )i∈I1 ,j∈I2

obtained by applying the expansion law.
P• P
P ≡ (c)P 0 . By induction JP 0 K is of the formi∈I λi .Qi . Let JP K be
0
λ
.(c)Q
,
where
I
=
{i
|
i
∈
I
∧
n(λ
)
=
6
c}.
When
I 0 is empty, JP K
0
i
i
i
i∈I
is simply 0.
P• P ≡ P1 +P
P2 . By induction JP1 K is of the form i∈I1 λi .Q
Pi and JP2 K is of
the form i∈I2 λi .Qi such that I1 ∩ I2 = ∅. Let JP K be i∈I1 ∪I2 λi .Qi .
P• P ≡ !P 0 . By induction JP 0 K is of the form i∈I λi .Qi . If I = ∅ then let
JP K be 0; otherwise let JP K be the summation
λi =λjX

λi .(Qi | ZP ) +X

τ.(Qi | Qj | ZP ),

i,j∈I

i∈I

where ZP is the following fixpointλi =λjX
XµZ.(λi .(Qi | Z) +τ.(Qi | Qj | Z)).
i∈I

i,j∈I

The encoding clearly gives rise to a termination preserving subbisimilarity from
CCS! to CCSm .
The following result appears to be new. It summarizes the relationships
between several variants of CCS.
m
gm
m!
!
ccs
Corollary 6. CCS! vccs
vccs
vccs
↓ CCS v↓ CCS↓ CCS↓ CCS .

A proof of the following fact can be read off from the proof of the above
corollary.

44s!
Corollary 7. CCSs vccs
↓ CCS .

It is interesting to observe that Corollary 6 implies that the difference between CCS and CCSm is the same as that between CCS and CCS! . The former
is due to the variations on the choice and the latter is attributed to the twoforms of recursion.
An important consequence of Corollary 6 is that we could introduce the expansion order for CCSm and CCSgm so that Compatibility Property (Lemma 35)
and Expansion Property (Proposition 4) are valid for these calculi. The expansion order for CCSgm is defined in terms of the expansion order  for CCS! .
For CCSgm processes P, Q, P gm Q if and only if I ! (P )  I ! (Q).
The quasi-well order structure is an immediate consequence of this definition.
Proposition 5. Suppose P is a process in CCSgm . If P0 , P1 , P2 , . . . is an infinite sequence in (Drv(P ), gm ), then there is an infinite increasing subsequence
Pi0 gm Pi1 gm Pi2 gm . . ., where i0 < i1 < i2 < . . ..
Proof. Suppose P0 , P1 , P2 , . . . is an infinite sequence in CCS gm . Then in CCS!
one has an infinite sequence I ! (P0 ), I ! (P1 ), I ! (P2 ), . . .. By Proposition 4, there
is an infinite increasing subsequence I ! (Pi0 )  I ! (Pi1 )  I ! (Pi2 )  . . ., wherei0 < i1 < i2 < . . .. It follows that Pi0 gm Pi1 gm Pi2 gm . . ..
The compatibility of gm also holds.
λLemma 38. Suppose P, Q are processes in CCSgm . If P gm Q and P −→ P 0
λthen Q0 exists such that Q −→ Q0 and P 0 gm Q0 .
λ

Proof. Suppose A gm B and A −→ A0 . By definition I ! (A)  I ! (B). The
encoding I ! defined in the proof of Fact 1 satisfies the following property:QλλIf A −→ A0 then I ! (A) =⇒−→= I ! (A0 ) | i 0 for some i ≥ 0.
Q
λIt follows from I ! (A)  I ! (B) that I ! (B) =⇒−→ C and I ! (A0 ) | i 0  C. By
the definition of , the process I ! (B) literally contains the process I ! (A). So it
Q
λmust be the case that C = I ! (B 0 ) | i 0 and that B −→ B 0 . But then it is easy
!
0
!
0
0
m
0
to see that I (A )  I (B ). Hence A  B .
Now we may define an expansion order m on CCSm processes in terms of .
gm

For CCSm processes P, Q, P m Q if and only if I gm (P )  I gm (Q).
It is obvious that gm satisfies Expansion Property.
Proposition 6. Suppose P is a process in CCSm . If P0 , P1 , P2 , . . . is an infinite sequence in (Drv(P ), m ), then there is an infinite increasing subsequence
Pi0 m Pi1 m Pi2 m . . ., where i0 < i1 < i2 < . . ..
45

The structural bisimilarity between P and I gm (P ) forces m to inherit
all the good properties from gm . In particular CCSm satisfies Compatibility
Property.
λLemma 39. Suppose P, Q are processes in CCSm . If P m Q and P −→ P 0
λthen Q0 exists such that Q −→ Q0 and P 0 m Q0 .
2.4.3

Replication, or Fixpoint

We have seen in Proposition 3 that there is no termination preserving subbisimilarity from CCS to CCS! . Using Expansion Property proved in Section 2.4.1,
we can strengthen that result significantly.
Proposition 7. CCS 6vccs CCS! .
Proof. We show that RanT imer cannot be bisimulated by any process in CCS! .
Assume that a process A of CCS! bisimulated RanT imer. To bisimulate theactions
RanT imer −→ 0
there must exist some A0 , A00 , A000 such thats

A =⇒ A0 −→ A00 =⇒ A000 ≈ 0.
Clearly A0 ≈ RanT imer and A00 ≈ A000 ≈ 0. Now A0 should bisimulates
RanT imer −→ tick | 0. Therefore some A1 , A01 , A001 exist such thats

A0 =⇒ A1 −→ A01 =⇒ A001 ≈ tick | 0.
s

Again it is clear that A1 ≈ RanT imer. Now if A0 =⇒ A1 −→ A01 is bisimulatedsby RanT imer −→ Q, then A001 ≈ Q since Q cannot do any tau action. Hence
000
A1 ≈ A1 ≈ tick | 0. In this way we may construct the following infinite sequence
A0 =⇒ A1 =⇒ . . . =⇒ Ai =⇒ . . .
such that

s

tick

tick

Ai −→ =⇒
· · =⇒} ≈ 0| ·{zi timesfor each i ≥ 0. Now we may apply Proposition 4 to get an infinite increasing
subsequence
Ai0  Ai1  . . .  Aip  . . . .
By construction,
s

tick

tick

Ai0 −→ =⇒· · =⇒} ≈ 0
| ·{z

(16)

i0 times

and

s

tick

tick

Ai1 −→ =⇒· · =⇒} ≈ 0.
| ·{zi1 times

46(17)

It follows from Lemma 35 and (16) that
s

tick

tick

Ai1 −→ =⇒· · =⇒} A0
| ·{z

(18)

i0 times

for some A0 . If A0 6≈ 0 then the only actions A0 may perform are tick action. It is
impossible for A0 to perform an infinite sequence of tick action since RanT imer
cannot do an infinite sequence of tick action after an s-action. So we must have
tick

tick

A0 =⇒
· · =⇒} ≈ 0| ·{zk times

for some k > 0. According to Definition 13 it is easy to prove by structural
induction that
tick

tick

s

tick

tick

Ai1 =⇒· · =⇒} A00 −→ =⇒· · =⇒} ≈ 0
| ·{z
| ·{z

(19)

i0 times

k times

for some A00 . Since k > 0, there must exist some A000 such thattick

Ai1 =⇒ A000 −→ .
Now A000 would have to bisimulate RanT imer because Ai1 bisimulates the random timer. This is a contradiction since A000 would not be able to simulate thesaction RanT imer −→ 0. It follows that (18) must be in the following form
s

tick

tick

Ai1 −→ =⇒· · =⇒} ≈ 0.
| ·{z

(20)

i0 times

The action sequences of (17) and (20) must be induced by two distinct s-prefixes,
which must be the summands of a same mixed choice. Otherwise Ai1 would be
able to do two consecutive s-actions.
The above argument can be repeated to arrive at the following conclusion:
For each p ≥ 0, Aip contains a mixed choice with at least p + 1 summands. But
this contradicts Lemma 31.

2.5

Recursive Definition

The infinite behaviors can also be admitted through constant definition [39]. We
shall spend a minute to explain the mechanism of constant definition. Suppose
E1 , . . . , En are expressions with free process variables X1 , . . . , Xn . The following
is a finite set of constant definitions.
C1

Cn= E1 [C1 /X1 , . . . , Cn /Xn ],..
.
= En [C1 /X1 , . . . , Cn /Xn ].
47

We remark that we do not allow recursively defined definitions using an infinite set of equations. A prominent feature of the constant mechanism is thatit disallows the α-conversion. Take for instance the constants D1 , D2 defined
below.
D1
D2= a | (a)(b.c | D2 ),= b | (b)(a.c | D1 ).

The global name a in the definition of D2 is captured by the localization operator(a) in the definition of D1 dynamically. One has thatD1≡c | (c)(b.c | b | (b)(c.c | D1 ))τc | (c)(c | (b)(c.c | D1 ))c | (c)(c | (b)(c.c | c | (c)(b.c | D2 )))τc | (c)(c | (b)(c | (c)(b.c | D2 ))).

−→
≡
−→

These internal actions are possible only if renaming never happens.
A similar way of introducing the infinite behaviors is by using the dynamic
fixpoint, whose semantics is defined by the following rule.
λE[µX.E/X] −→ E 0
λµX.E −→ E 0
For the dynamic binding µ-operator, global names might get localized dynamically while unfolding the recursion. For instance µX.c | (c)(c | X) may not do
any action if the static binding is adopted. It is divergent if the dynamic binding is admitted. For the dynamic fixpoint operations the α-conversion is alsobanned.
Let CCSdef be the CCS with the constant definition and CCSdµ be the CCS
with the dynamic µ-operator. These two variants of CCS are completely the
same.
def
dµ
Fact 2 (Giambiagi, Schneider, Valencia [27]). CCSdµ vccs
vccs
↓ CCS
↓ CCS .

Proof. The conversions between CCSdµ and CCSdef are relevant to this paper.
So we take some time to explain them. Given a process P in CCSdµ , we may
convert it into a finite set of constant definitions in the following manner.
1. To start with we introduce the constant C = P .
2. Suppose the conversion has introduced the following set of constant definitions.
C
C1

Cn
48

= E0 ,= E1 ,..
.
= En .

If µX.En+1 is a subexpression in one of E1 , . . . , En such that En+1 does
not contain any occurrence of the µ-operator, then we replace the above
set of definitions by the following set of definitions.
C
C1

Cn
Cn+1

=
=
..
.
=
=

E0 [Cn+1 /µX.En+1 ],E1 [Cn+1 /µX.En+1 ],En [Cn+1 /µX.En+1 ],En+1 [Cn+1 /X].

3. The second step is repeated until there is no occurrence of µ-operator in
any of the definitions.
It is easy to see that P is structurally bisimilar to C.
Next we explain the converse conversion. Without loss of generality, supposethat we have in CCSdef the following set of constant definitions.
C1
C2= E1 [C1 /X1 , C2 /X2 ],= E2 [C1 /X1 , C2 /X2 ].

Now C1 , C2 form a solution to the following equations.
X1
X2= E1 ,= E2 .

Using the dynamic µ-operator of CCSdµ , one could construct the process expression µX1 .E1 . Substituting µX1 .E1 for X1 in the second equation gives riseto the equation
X2= E2 [µX1 .E1 /X1 ]from which we could construct µX2 .E2 [µX1 .E1 /X1 ]. It is easy to see that
C1
C2

∼ µX1 .E1 [µX2 .E2 [µX1 .E1 /X1 ]/X2 ],∼ µX2 .E2 [µX1 .E1 /X1 ].

We are done.
From now on we shall ignore CCSdµ . For the purpose of bookkeeping we
mention that there is another way of introducing the infinite behaviors usingparametric definition. Let CCSpdef be CCS with parametric definition. It isdef
pdef
proved in [27] that CCSpdef vccs
vccs
. We will formally intro↓ CCS↓ CCS
duce the parametric definition in Section 3.
Putting the issue of expressiveness aside for a moment, constant definition
does allow us to define interesting processes. Consider the process Counter49

defined in CCSdef .
CounterOE= zero.Counter + inc.(d)(O | d.Counter),= dec.d + inc.(e)(E | e.O),= dec.e + inc.(d)(O | d.E).

It is a simplified version of the counter defined in [7]. A process may increment
or decrement Counter by interacting with it at the interfaces inc and dec respectively. The process may also test if the current value of the counter is zerothrough interaction at zero. Obviously Counter has the following operational
behavior
dec zeroinc
inc dec. . −→} −→(21)
Counter −→. . −→}−→
| .{z
| .{z
i timesi timesfor every natural number i. The process Counter is capable of remembering thedifference between the number of inc’s it has performed and the number of dec’s
it has done. After it has done consecutive inc’s for a number of times, it must
do precisely the same number of dec’s before it can do the action zero. Counter
is about the ability to remember the past in the presence of the fact that thepotential configurations of the history are infinite. It requires the model to havesome kind of recording mechanism. For a process calculus, the ability to define
a counter says a great deal about Turing computability of the calculus.
2.5.1

Fixpoint, or Constant Definition

The Counter defined in the previous subsection is interesting in that it rules out
the possibility for CCSdef to hold of such property as stated in Proposition 4.
But how about CCS? It appears that CCS is closer to CCSm than to CCSdef .
We now justify this intuition.
A simple idea to convert a CCS process to a CCSm process is to rewrite every
binary choice, say A+B, to a mixed choice, say a.A+a.B. For the conversion
to cause no confusion, it is required that a does not appear in A | B. Formally
we define name indexed maps from CCS to CCSm by structural induction.
Ia (0)def

Ia (Y )def

Ia (λ.E)def=

λ.Ia (E),

Ia (E1 | E2 )def

Ia (E1 ) | Ia (E2 ),Ia (E1 +E2 )def

Ia ((c)E)def

Ia (µZ.E)

def

=
=

=

=

=

=

0,
Y,

a.Ia (E1 ) + a.Ia (E2 ),(c)Ia (E),µZ.Ia (E).

The properties of Ia are stated in the following three lemmas.

50

λLemma 40. If P −→ Q and a does not appear in P | Q then there exists someaaλi ≥ 0 such that Ia (P )−→. . −→} −→ Ia (Q).
| .{zi times

Proof. By using the equivalence Ia (E{F/Z}) ≡ Ia (E){Ia (F )/Z}, a simple induction on derivation suffices.
Using simple induction, we could also prove the converse of Lemma 40.
aaλLemma 41. If Ia (P )|−→ .{z. . −→} −→ A for some natural number i and somei times

λ

a

a

λ

a

a

λ 6= a, then P −→ Q and Ia (P ) |−→ .{z. . −→} −→ Ia (Q) −→. . −→} A for some| .{zj timesi−j times

Q and some j ≤ i.
Given a CCS process P , it is possible for Ia (P ) to do an infinite sequence of
a-actions. But if Ia (P ) can do a non-a-action λ, then the number of a-actions
that have to be done before λ can be enacted is bounded by a number Na (P )derived from the syntax of P . We explain below how the number Na (P ) is
calculated. Firstly we define the function Na ( ) inductively on the set of all
CCS! processes whose binary choices are all of the form a. + a. .
Na (0)def=

Na (λ.P 0 )def

Na (P1 | P2 )def

Na (a.P1 + a.P2 )

=

=

def

1,
1,
Na (P1 ) + Na (P2 ),=1 + max{Na (P1 ), Na (P2 )},

0

def

=

Na (P 0 ),Na (!P 0 )def

2Na (P 0 ).

Na ((c)P )=The last line of the induction takes into consideration that an action of !P iseither caused by P or is caused by an interaction between two copies of P . Now
for a CCS process P and a fresh name a, we define Na (P ) as follows:
Na (P )def=0

Na (I (Ia (P )))0

where the translation I removes the unguarded occurrence of the bound variables using the techniques developed in Section 2.3.2. The point of Na (P ) isthat it provides an upper bound for the number of a-actions Ia (P ) has to do
before making a non-a-action.
Lemma 42. Suppose P is a process in CCS. Then P cannot do any action
if and only if every action sequence of Ia (P ) with length no more than Na (P )consists of only a-actions.

51

0Proof. Since all choices in Ia (P ) are of the form a. + a. , the translation I
does not change the choice constructions appeared in Ia (P ). The proofs in0Section 2.3.2 establish that I (Ia (P )) is structurally bisimilar to Ia (P ). So the0minimal number of a-actions I (Ia (P )) has to do in order to do a non-a-actionis the same as the minimal number of a-actions Ia (P ) has to do in order to doa non-a-action. The lemma then follows from the definition of Na ( ).
The above lemma suggests to define the expansion order ccs of CCS processes in terms of the expansion order  in the following manner:
For processes P, Q of CCS, P ccs Q if and only if I ! (Ia (P )) 
I ! (Ia (Q)) for some fresh a.
Expansion Property is a straightforward consequence of this definition.
Proposition 8. Suppose P is a process in CCS. If P0 , P1 , P2 , . . . is an infinite sequence in (Drv(P ), ccs ), then there is an infinite increasing subsequence
Pi0 ccs Pi1 ccs Pi2 ccs . . ., where i0 < i1 < i2 < . . ..
Compatibility Property is also valid for ccs .
λLemma 43. Suppose P, Q are processes in CCS. If P ccs Q and P −→ P 0
λthen Q0 exists such that Q −→ Q0 and P 0 ccs Q0 .
λ

Proof. Suppose P ccs Q and P −→ P 0 . By Lemma 40 some i exists such
λ
a
a
λ
a
a
. . =⇒} −→ I ! (Ia (P 0 )).
that Ia (P )−→. . −→} −→ Ia (P 0 ). So I ! (Ia (P ))=⇒
| .{z
| .{z
i timesi timesa
λa

But then some Q0 exists such that I ! (Ia (Q))=⇒. . =⇒} −→ I ! (Ia (Q0 )) and| .{zi timesI ! (Ia (P 0 ))  I ! (Ia (Q0 )). ThereforeaaλIa (Q)−→. . −→} −→ Ia (Q0 ).
| .{z

(22)

i timesλIt follows from (22) and Lemma 41 that Q −→ Q0 . Hence P ccs Q.
Let CCS−def be the variant of CCS− with the dynamic fixpoint operator.
Similarly we have CCSmdef and CCSsdef . What is the relationship between
CCSm and CCSmdef ? Using the α-conversion one may rename the local namesof a process expression in a variant with static fixpoint operations such that allnames are distinct. Clearly for such a process expression dynamic and static
fixpoint operations make no difference. Hence
CCS−

vccs
↓

CCS−def ,

CCSs

vccs
↓

CCSsdef ,

CCSm

vccs
↓

CCSmdef .

52

Busi, Gabbrielli and Zavattaro have shown in [7, 8] that the termination property is decidable in CCSm but undecidable in CCSmdef . The technique used intheir proofs essentially imply that dynamic recursion is strictly stronger interactively than static recursion in the setting of CCS. A different argument forthis fact is given below.
Proposition 9. The following properties hold:(i) CCS−def 6vccs CCS− ;(ii) CCSsdef 6vccs CCSs ;(iii) CCSmdef 6vccs CCSm ;(iv) CCSdef 6vccs CCS.
Proof. (ii,iii) Counter is actually defined in CCSsdef . Now suppose there were a
process D of CCSm that bisimulated Counter and that the simulated sequenceof actions is the following:
inc

inc

inc

inc

D =⇒ D1 =⇒ . . . =⇒ Di =⇒ Di+1 . . . .
Since the above sequence is in CCSm , we may apply Lemma 39 and Proposition 6
to conclude that there must exist Dp and Dq , where p < q, such that Dq can
do whatever Dp can do. But then the following sequence of actions would bepossibledec zeroinc
inc dec. . =⇒} =⇒D=⇒. . =⇒} =⇒
| .{z
| .{z
q timesp timeswhich contradicts the assumption that D bisimulated Counter.
(iv) In view of Lemma 43 and Proposition 8, the above argument can be
repeated to show that CCSdef 6vccs CCS.
(i) In CCS−def , and CCS− as well, one could define the internal choice E +̇ F
as follows:
E +̇ Fdef=(h)(h.E | h.F | h)where h does not appear in E | F . Using internal choice one could define a weakform of the counter in CCS−def in the following manner.
D0
O0
E0

= zero.D0 +̇ inc.(d)(O0 | d.D0 ),= dec.d +̇ inc.(e)(E 0 | e.O0 ),= dec.e +̇ inc.(d)(O0 | d.E 0 ).

Although D0 does not always do what the environments anticipate, it does
exhibit the same memory capacity as Counter. For this reason the approach
used above can be applied to establish (i).
The fact that dynamic fixpoint operations, or constant definitions, are muchstronger than static fixpoint operations, or replications, is reinforced by anotherfact: CCS with dynamic fixpoint operations and mixed choices is strong enoughto code up CCS with arbitrary choices. It is a phenomenal result that bringsout the power of constant definition.
53

C0ϕ
ϕ
Cλ.E
ϕ
C(a)E
ϕ
CE1 +E2
ϕCE
1 | E2ϕ
VE1 |E2
WEϕ1 |E2= eϕ ,ϕ= eϕ + λ.(eϕ )CE,ϕ= (a)CE ,ϕϕϕϕ) + τ.(eϕ )(CE),| eϕ .CE| eϕ .CE= eϕ + τ.(eϕ )(CE
1 +E2
1 +E2
1
2
ϕ
ϕ
= eϕ + τ.(h)(VE1 |E2 | WE1 |E2 ),ϕϕ= τ.(eϕ )(CE,| eϕ .VEϕ1 |E2 ) + h.CE
1
1 | E2ϕ= τ.(eϕ )(CE| eϕ .WEϕ1 |E2 ) + h,2

where ϕ ∈ {>, ⊥}, ϕ = ¬ϕ and e> , e⊥ are fresh names.
Figure 2: Transformation from CCSdef to CCSmdef .
Proposition 10. CCSdef vccs CCSmdef vccs CCSsdef .
The proof of CCSmdef vccs CCSsdef can be readily copied from the proof of
Proposition 1. The proof of CCSdef vccs CCSmdef is complex. One needs toconstruct a translation from CCSdef processes to CCSmdef processes. To define
the construction we start with a sound translation from finite CCSdef processes
to CCSmdef processes. The encoding JP Kf of a finite CCS process P can be
defined as follows:
def

JP Kf

=

µZ.JP KZ

where J KZ is defined inductively by the following clauses:
def

=

J0KZ

def

Jλ.P KZ

def

J(a)P KZ

def

JP1 +P2 KZ
JP1 | P2 KZ

=
=

=

def

=

τ.Z,
τ.Z + λ.JP Kf ,(a)JP KZ ,

τ.JP1 KZ + τ.JP2 KZ ,(h)(µZ 0 .(τ.JP1 KZ 0 +h.Z) | µZ 0 .(τ.JP2 KZ 0 +h)).

The intuition about JP KZ is that it retains all the capabilities of P using only
separated choices. To accomplish that, JP KZ introduces a number of computational choices in such a way that all these internal choices can be undone bygoing back to where it started. In JP KZ there are a number of loops or, as we
prefer to call them, internal loopings. Here Z is the starting point to which aninternal looping may go to and by doing so it forgets all the choices it has made.
The loops may be connected so that an internal looping cannot only go backlocally but also globally. The soundness of the encoding J Kf is guaranteed byComputation Lemma.

54Unfortunately the above translation cannot be extended to deal with theinfinite behaviors. Suppose we were to define JµX.E1 Kf . A straightforward approach is to let it be JE1 {µX.E1 /X}Kf . By structural property, each occurrenceof µX.E1 would get interpreted as JµX.E1 KZ for some bound Z. We were in a
non-well-founded situation since the interpretation JµX.E1 KZ would depend onsome JµX.E1 KZ 0 for some other Z 0 .
One way to get out of the awkward cycle is to use the first order pointers,some special names, to access the backup points. These pointers must be carefully introduced such that only a finite number of names are necessary. Dynamic
binding plays a crucial role here.
We define a translation from CCSdef to CCSmdef in four steps.
1. First a translation from CCSdef expressions without any µ-operations toconstant definitions in CCSmdef is defined. This translation, given in Figure 2, is a first order counterpart of the above encoding. For each CCSdef⊥>
are introduced,, CE
expression E without µ-operator, two constants CE
one of which is indexed by the boolean value truth > and the other byfalse ⊥. These two translations are defined uniformly using a boolean
variable ϕ. The names e> and e⊥ are used to trace back to the starting
point of an internal looping. The alternating use of e> , e⊥ is essential,
and is reminiscent of the alternating use of d, e in the counter defined in>andSection 2.5. If E contains free process variables Y1 , . . . , Ym , then CE
>
>
⊥
⊥
⊥
CE are parameterized over the constants CY1 , . . . , CYm , CY1 , . . . , CYm .
⊥>, constructs a structure that adds internal tau, or CEThe translation CE
actions on the top of the structures of E. These internal actions are
introduced to force all choices to be separated choices. The additional
choices by the extra tau actions must be done in such a way that they canbe undone if wanted. Let’s explain the idea using diagrams.

• C0ϕ is able to go back to the previous checkpoint by synchronizing
through name eϕ . The name eϕ acts as a pointer to the backup at theprevious checkpoint. In the following diagram, the bullet represents
the current state and the circle indicates the checkpoint.

ϕ• Cλ.E
has to make a decision. Either it chooses to call up the backup at
the previous checkpoint by synchronizing through name eϕ , or it does
the λ-action prescribed by λ.E and forgets all about the history. Inϕ(eϕ )CEthe local name eϕ sets up a new checkpoint. In the following
diagram the box represents the state after the λ-action.

55

λ
ϕ
• The intended meaning of the constant C(a)E
should be clear.
ϕ• The constant CE
can make a decision among three choices. It
1 +E2
may call up the backup at the previous checkpoint. It can do aninternal τ -action, part of the internal looping, and then turns intoϕϕ
ϕ
ϕ). The process expression (eϕ )(CE)(eϕ )(CE| eϕ .CE| eϕ .CE
1 +E2
1 +E2
1
1
ϕ
consists of two parts. The expression eϕ .CE1 +E2 records the backupϕϕCE
at the present checkpoint. When CE
is engaged in an inter1 +E2
1
nal looping, it retains the right to reset the system to the previousϕϕstate CEby synchronizing at eϕ . But once CE
has done an
1 +E2
1
action prescribed by E1 , the alternating use of eϕ and eϕ makes sureϕthat the checkpoint and the backup eϕ .CE
are completely for1 +E2
gotten. It should be pointed out that in the internal looping statesϕϕ), the system still reserves the right to kickof (eϕ )(CE| eϕ .CE
1 +E2
1off any actions of E2 . The third choice is symmetric to the secondone.

λ1 . . . λm

λ1 . . . λnϕϕ
• The constant CE
is a little more complex than CE. Again
1 +E2
1 | E2it may go back to the previous state by synchronizing at eϕ . It
may also evolve to (h)(VEϕ1 |E2 | WEϕ1 |E2 ). Now VEϕ1 |E2 can evolve toϕϕ(eϕ )(CE| eϕ .VEϕ1 |E2 ). While CE
is looping, it can trigger eϕ .VEϕ1 |E2
1
1
ϕso that the system goes back to VEϕ1 |E2 . If CE
chooses to do an1
action defined by E1 , the checkpoint and the backup eϕ .VEϕ1 |E2 arethrown away. The system WEϕ1 |E2 plays the similar role. It does forE2 what VEϕ1 |E2 does for E1 . Finally when both VEϕ1 |E2 and WEϕ1 |E2
ϕare evolving independently, they may agree to go back to CE
1 | E256

together. This is achieved by a synchronization at h. The ability
to synchronize at h is indicated in the diagram by two neighboring
cycles and the arrow pointing to the bullet.

λ1 . . . λm

λ1 . . . λn

2. Secondly each CCSdef process P with n occurrences of the µ-operator isunrolled to a set of n equations
X1

Xn= EP1 ,..
.
= EPn ,

in the way as explained in the proof of Fact 2. Let EP be the CCSdef
expression obtained by replacing the n fixpoints in P by the corresponding
process variables X1 , . . . , Xn . We then have a new equationX= EP

for a fresh process variable X.
3. Thirdly we have a set of constant definitions in CCSdm . This set consistsof the following definitions
>
CX

>
= CE
,
P

>
CX
1

>
= CE
1 ,

>
CX
n

..
.
>
= CE
n,
P

⊥
CX

⊥
= CE
,
P

⊥
CX
1

⊥
= CE
1 ,

⊥
CX
n

..
.
⊥
= CE
n,
P

57

P

P

>
>
⊥
⊥
plus the constant definitions introduced by CE
1 , . . . , CE n , CE 1 , . . . , CE n .
P

P

P

P

It should be pointed out that the encoding of a particular occurrence of the>⊥process variable Xi , say, must be either CX
or CX. This is guaranteediiby the alternating use of e> and e⊥ .
4. Finally the encoding JP K is given by the following definition:
def

=

JP K

>
(e> )CX.

The encoding J K so defined makes full use of dynamic binding mechanism. It
is very much like Counter defined in Section 2.5.
To understand the encoding, the reader is advised to work out the encodingof the process P ≡ µX.(a+b | X). The equations derived from this process are
X
Y

= Y,
= c + d | Y,

which can be simplified to a single equationX= c + d | X.

(23)

The constant definitions that correspond to (23) are given as follows:
PX
Pc+d | X
Qc= Pc+d | X ,= a + τ.(b)(Qc | b.Pc+d | X ) + τ.(b)(Qd | X | b.Pc+d | X ),Qd | X= b + c.(a)P0 ,= b + τ.(h)(Q1d | X | Q2d | X ),Q1d | X

= τ.(a)(Pd | a.Q1d | X ) + h.Qd | X ,Q2d | X
Pd
P0

= τ.(a)(PX | a.Q2d | X ) + h,
= a + d.(a)P0 ,
= a,

>
⊥
where we write a for e> , b for e⊥ , PE for CE, and QE for CE. The followinginternal action sequence is an instance of an internal looping of the interpretation
JµX.(c+d | X)K.

(a)PX

τ

(a)(b)(Qd | X | b.Pc+d | X )τ(a)(b)((h)(Q1d | X | Q2d | X ) | b.Pc+d | X )τ(a)(b)((h)(Q1d | X | (a)(PX | a.Q2d | X )) | b.Pc+d | X )τ(a)(b)((h)(Q1d | X | (a)((b)(Qc | b.Pc+d | X ) | a.Q2d | X )) | b.Pc+d | X )c(a)(b)((h)(Q1d | X | (a)((b)((a)P0 | b.Pc+d | X ) | a.Q2d | X )) | b.Pc+d | X .

−→
−→
−→
−→
−→

58

The last process can be equated to d as is shown below.
(a)(b)((h)(Q1d | X | (a)((b)((a)P0 | b.Pc+d | X ) | a.Q2d | X )) | b.Pc+d | X∼ (a)(b)((h)(Q1d | X | (a)((b)(0 | b.Pc+d | X ) | a.Q2d | X )) | b.Pc+d | X )∼ (a)(b)((h)(Q1d | X | (a)(0 | a.Q2d | X )) | b.Pc+d | X )∼ (a)(b)((h)(Q1d | X | 0) | b.Pc+d | X )∼ (a)((h)(Q1d | X ) | 0)
≈ d.
In this example, four steps of internal looping are made before the action c is
performed. In the first three steps of internal looping, the agent wanders along
the summation and the composition structures of c + d | X and then reaches
a recurrence of PX . After the fourth step the agent reserves the right to go
back to any of the previous states. But once it kicks off the action c, it throws
away all the pointers that lead to the backups. This is evidenced by the strong
equivalences. The last equivalence says that the sequence of actions correspondcto µX.(c+d | X) −→ d.
Having explained the encoding in detail, we now make some further comments about some design decisions of the encoding.
• Does the encoding provide a translation from CCS to CCSm ? The answer
is definitely negative. The problem is to do with infinite behaviors. In
the interpretation of say (23), the constant PX plays two roles: First it
represents the interpretation of the fixpoint µX.(c + d | X); Second it is astate that can turn the clock back. To fulfill the first role, PX must berecursively defined. To accomplish the second task, PX must contain a(global) name that points to the previous backup. But the interpretation
PX should not introduce additional global names apart from those alreadyappeared in E. The only way for PX to do both jobs is to use dynamic
binding.
• Why should we stick to the two local names e> , e⊥ ? Why can’t we use
a fresh local name every time a different local name is called for in theencoding? The reason that we cannot do that is again due to infinite
behaviors. Had we done that, then the encoding of a fixpoint expression
could lead to an infinite number of constant definitions.
• Can we use one local name instead of the two local names e> , e⊥ ? The
answer is again negative. One of the tricky part of the encoding is todefine the internal looping in such a way that it can always go back to theright starting point. If CE1 +E2 is defined bye + τ.(e)(CE1 | e.CE1 +E2 ) + τ.(e)(CE2 | e.CE1 +E2 )using only one pointer e, then after CE1 +E2 wanders to (e)(CE1 | e.CE1 +E2 )it can never go back to CE1 +E2 . Another possibility would be not to use
59

CCSsdef

CCSdefCCSmdef

CCSs

CCS

CCSm

CCSs!

CCS!

CCSm!

Figure 3: Subbisimilarities of CCS
the operator (e) locally. But then things would be messed up when trying
to go back to the previous backups. So one local name is not an option atall.
In some sense the dynamic fixpoint and the names e> , e⊥ are forced upon us.
The proof of the correctness of the encoding can be found in Appendix A.

2.6Interaction Hierarchy of CCS

We can now summarize the main results of Section 2.
Theorem 1. The subbisimilarity relationships between the nine variants of CCS
are depicted in Figure 3.
In Figure 3 an arrow → indicates the existence of a subbisimilarity and 9means the nonexistence of such a subbisimilarity. In other words, CCS1 → CCS2
means that CCS2 is at least as expressive as CCS1 ; and CCS1 9 CCS2 meansthat there is a process in CCS1 that cannot be expressed in CCS2 . It is clear
from Figure 3 that all the subbisimilarity relationships between the nine variantsof CCS have been unveiled.
The second major result tells the story of the expressiveness of CCS when
Computation Criterion is applied.
Theorem 2. The codivergent subbisimilarity relationships between the ninevariants of CCS are depicted in Figure 4.
In Figure 4 the tailed arrow  represents a codivergent subbisimilarity and6 rules out any codivergent subbisimilarity.
It should be remarked that the diagram in Figure 4 does not spell out everything. Some positive and negative results have either been proved before or canbe easily derived by transitivity. In fact all the codivergent subbisimilarity relationships among the nine CCS variants are known. The following summarizes
the facts that are not explicitly indicated in the diagram of Figure 4.
Fact 3. The following statements are valid.
def(i) CCSdef 6vccs CCSm , CCSm vccs
.
↓ CCS
60

CCSdef

CCS

CCS!

CCSmdef

CCSm

CCSm!

CCSsdef

CCSs

CCSs!

Figure 4: Codivergent Subbisimilarities of CCS
def(ii) CCSdef 6vccs CCSs , CCSs vccs
.
↓ CCS
mdef
mdef
ccs
ccs
(iii) CCS
6v CCS, CCS 6v↓ CCS
.
mdef
mdef
s
s
ccs
ccs
.
(iv) CCS
6v CCS , CCS v↓ CCS
sdef(v) CCSsdef 6vccs CCS, CCS 6vccs
CCS
.
↓
sdef
(vi) CCSsdef 6vccs CCSm , CCSm 6vccs.
↓ CCS

Proof. All the positive results are immediate by composition. The proofs of
CCSdef 6vccs CCSm , CCSdef 6vccs CCSs , CCSmdef 6vccs CCS, CCSmdef 6vccs
CCSs , CCSsdef 6vccs CCS and CCSsdef 6vccs CCSm are basically an iteration ofsdef
the proof of (iv) of Proposition 9. The proof of CCSm 6vccs
is the same
↓ CCS
sdef
ccs
as that of Proposition 3. In view of the fact that CCS 6v↓ CCS
follows
mdef
mdef
ccs
ccs
from CCS 6v↓ CCS, the only thing left is to prove CCS 6v↓ CCS.
We show that RanT imer cannot be bisimulated by any terminating processof CCSmdef . The crucial property about RanT imer is that it has an infinite
number of s-derivatives. We prove by structural induction the following fact: A
process expression E of CCSmdef has only a finite number of s-derivatives if itsatisfies the following three conditions about its immediate actions.
1. E cannot do any τ -action;
2. E can do at least one s-action; and3. E cannot do two consecutive s-actions.
Here is the structural induction.
P
1. If E is a summationi∈I λi .Ei then clearly E has a finite number ofs-derivatives.
2. Suppose E is a composition E0 | E1 . If E0 (or E1 ) can do an immediates-action, then E1 (or E0 ) can never ever do any s-action. By induction
hypothesis E0 (or E1 ) has a finite number of s-derivatives. So E has afinite number of s-derivatives.
3. If E is (c)E 0 then by structural induction E 0 has a finite number of sderivatives. Consequently E has a finite number of s-derivatives.
61

4. Now suppose that E ≡ µX.E 0 . We show by structural induction that
all the occurrences of X in E 0 are guarded. Assume that there were an
unguarded occurrence of X in E 0 .
• E 0 cannot be a mixed choice since all occurrences of X in a mixed
choice are guarded.
• If E 0 ≡ E0 | E1 , then we may assume without loss of generality thatthe unguarded occurrence of X is in E0 . In this case E1 does not haveany s-derivatives for otherwise E would be able to do two consecutives-actions. So we may continue the structural induction with E0 .
• If E 0 is (c)E 00 then we continue the structural induction on E 00 .
• E 0 ≡ µZ.E 00 . In this case we continue the structural induction on
E 00 .
The above structural induction must stop. In other words, there is no
unguarded occurrence of X in E 0 . It follows that E has only a finite
number of s-derivatives.
A terminating process CCSmdef must meet the above three conditions if it bisimulated RanT imer. Such a process does not exist by the above argument.
Several general conclusions about the expressiveness of CCS can be drawn
from the interaction hierarchy of CCS.
• Constant definition in CCS is strictly more expressive than fixpoint operator. Fixpoint in CCS is strictly more expressive than replication.
• General choice in CCS is strictly more expressive than guarded choice. If
all choices are guarded, then fixpoint operator is equivalent to replication
operator.
• There are specifications written in CCS that cannot be implemented by
CCS processes without the choice operators. An automaton is fundamentally different from a concurrent system.
These conclusions are also of practical interest. In most applications, CCS withconstant definition and guarded choice is preferred.
Theorem 1 and Theorem 2 point out that dynamic binding, admitted by constant definition and dynamic µ-operator, is strictly more powerful than static
binding in CCS. The essential reason for the difference is that dynamic binding achieves a certain degree of name-passing through process relocation. We
would gain more insight if the following question can be answered: What would
happen to the relative expressiveness if CCS is extended with name-passing
communication mechanism? We will soon know the answer.

62

3

Subbisimilarity for Pi

In this section we apply the idea of subbisimilarity to investigate the interactability of the variants of π-calculus. Most results we have established for CCS carryover to π-calculus. To make our transformation from CCS to π smooth, we shallbe using a particular presentation of π-calculus.
We start by explaining an unusual feature of the standard presentation of π.
In the pioneering paper on π-calculus [43], as well as a huge number of following
works [60], π-calculus and its variants are defined by adopting a uniform set ofnames. A name has both a constanthood and a variablehood. The name x in
xy.A is a constant name when it acts as a channel to communicate. On theother hand, the name x in y(x).xy.A has to be a variable name in a correctunderstanding of the semantics of π-calculus. This confusion of constant names
and variable names has made the theory of π-calculus more complex than it
should be.
In this paper we adopt the definition of π-calculus given in [23]. We takethe view that all names are constant. In order to define mobility, we introducename variables. Let Nv be the set of name variables. The following convention
will be maintained in the rest of the paper.
• N will be ranged over by a, b, c, d, e, f, g, h.
• Nv will be ranged over by u, v, w, x, y, z.
• N ∪ Nv will be ranged over by l, m, n, o, p, q.
An assignment ρ is a map Nv → N . A substitution σ is a partial map Nv *N ∪ Nv whose domain of definition is finite. A substitution is often givenby the notation {n1 /x1 , . . . , ni /xi }, where {x1 , . . . , xi } is the domain of thesubstitution and {n1 , . . . , ni } is the range of the substitution. Both assignmentand substitution are used in postfix manner.
The syntax of the core π-calculus is given by the following grammar.
E:= 0 | n(x).E | nm.E | τ.E | E | E | (a)E | µX.E.

We shall let π − denote this calculus. The set of the action labels is {ac, ac, a(c) |a, c ∈ N } ∪ {τ }. There are input actions like ac, output actions like ac, andrestricted output actions like a(c). In ac, ac, a(c), the name a is subject nameand the name c is object name. The derived notation a(c).E stands for (c)ac.E.
We will abbreviate a(c).E to a.E if c does not appear in E. Similarly a.E stands
for some a(x).E such that x does not occur in E.
The rules that introduce the operational semantics of π − are defined below.
Prefixaca(x).E −→ E{c/x}acac.E −→ Eττ.E −→ E

Composition
λE −→ E 0λ

E | F −→ E 0 | Fac

ac

E −→ E 0 F −→ F 0
τ
E | F −→ E 0 | F 0
63

ac

a(c)

E −→ E 0 F −→ F 0
τ
E | F −→ (c)(E 0 | F 0 )RestrictionacλE −→ E 0a(c)E −→ E 0(c)E −→ E

0c does not appear in λλ(c)E −→ (c)E 0

Fixpoint
λE{µX.E/X} −→ E 0
λµX.E −→ E 0
For a comprehensive account of the theory of π-calculus, one could consult [23].
The power of π-calculus comes from the ability to create potentially infinite
number of new names during execution. The following example illustrates thepoint. Let N abbreviate the process(b)(bc0 | µX.(aa+(b(z).z(c0 ).bc0 | X))).
It is obvious that N admits the infinite action sequenceτ c0 (c1 ) τ c1 (c2 ) τ c2 (c3 )N −→ −→ −→ −→ −→ −→ . . . .
It can also perform the finite action sequenceaa

τ c0 (c1 ) τ c1 (c2 )τ ci (ci+1 )N −→−→ −→ −→ −→ . . . −→ −→ ∼ 0
for all i ≥ 0. A variant of the above process is the following(b)(c0 (c0 ).bc0 | µX.(b(z).z(c00 ).bc00 | X))
which can bisimulate a process N 0 whose only action sequence is the following:c0 (c1 )c1 (c2 )c2 (c3 )N 0 −→ −→ −→ . . . .

(24)

We shall see that (24), without any tau actions between any observable actions,can be achieved by parametric definition.
Different choice operators induce different variants of π − :• π is π − extended with binary choice;• π m is π − extended with mixed choice;• π s is π − extended with separated choice.
By replacing fixpoint operator by replicator, one gets π ! , π m! and π s! .
The interactability of these variants of π-calculus depends to a great extent
on their infinite behaviors. So the question comes naturally, what operational
properties do π-variants inherit from CCS variants? An important aspect of
the operational semantics is described in Lemma 36. Does π ! for instance enjoy
the expansion property? Ex post facto, we could say that the motivation of64

π-calculus is precisely to defeat Lemma 36. The input prefixes of π draw input
values from an infinite set of names. So we can have following infinite behavior:
c c

c c

τ

τ

c c

τ

2 3
1 2
0 1
−→ . . . .
−→−→(b)(c0 (z).bz | !b(y).y(z).bz) −→−→−→No two processes in the above sequence are comparable in terms of expansion
order. Similarly the localization operator combined with the output operator
have the ability to generate an infinite number of new names. Let L be theprocess bc0 .c0 d | !b(z).z(c0 ).bc0 .c0 d in π ! . In the following infinite action sequenceτ c0 (c1 ) τ c1 (c2 ) τ c2 (c3 )L −→ −→ −→ −→ −→ −→ . . .
no two processes are compatible with respect to a syntactic order like . The
conclusion we draw from the examples is that we cannot expect to have a resultin π ! as general as Lemma 36. What we can discuss is which infinite action
sequences are well quasi-ordered. As it turns out, there is not too much tosay on this. The counter is definable in π ! by simplifying the register given
in [7]. The two concurrent components of the counter are given by the following
recursive definitions.
Zero
Succ

def

=

(c)(c | !c.(zero.c + inc.succ(d).d.c)),def!succ(x).(c)(c | !c.(dec.x + inc.succ(d).d.c)).

=

The process Counterπ , the counter in π, can be defined as follows.
defCounterπ = (succ)(Zero | Succ).
It is pointed out in [7] that Counterπ can be defined in a very small fragmentof πI-calculus [54] with a limited use of the restricted output. The implicationof this fact is that one should not expect a well quasi-order in the π-like calculi
if localization operator plays a significant role. Having said that, we still havea general guideline for a well quasi-ordered infinite action sequence. In thefollowing lemma Csub(Pi ) is the set of the concurrent subexpressions of Pi anddepth() (Pi ) is the depth of the nested localization operations, the definitions ofwhich are the same as in CCS! .
Lemma 44. In π ! the infinite action sequence
λ

λ

λ

0
1
2
P0 −→
P1 −→
P2 −→
...

is well quasi-ordered by  if the followings are met.
S
1. i∈ω Csub(Pi ) is finite;S
2. i∈ω ln(Pi ) is finite;
3. supi∈ω {depth() (Pi )} < ω.

65

The three conditions of the lemma guarantee that the proof of Lemma 36
can be used in the present setting.
For an application of the lemma, suppose
λ

λ

λ

2
1
0
...
P2 −→
P1 −→
P0 −→

is an infinite action sequence in π ! . It is well quasi-ordered if the following
conditions are met.
• If P0 contains an output prefix ac then c is not restricted by a localization
operator (c) in P0 .
• The set {c | ∃i≥0.∃a∈N .λi = ac} is finite.
Since only a finite number of new names are introduced, the conditions ofLemma 44 are satisfied. There are interesting cases where there are new names
produced by restricted output actions but the number of such names is finite.
Since π ! is Turing complete, there is no algorithm to check if an internal loopingof a process of π ! is well quasi-ordered.
In what follows, the random timer of π refers to the process defined by thefollowing equation.
def

RanT imerπ = µX.(aa + bb | X).

3.1

(25)

Pi Subbisimilarity

To compare the interactional powers of π-variants, we need to define subbisimilarity relationship on them. Such a relationship must be strong enough tocharacterize the interactability of π-processes. Similar to the case of CCS, a subbisimilarity for π-variants generalizes bisimulation equivalence on one π-variant
to a relationship from one π-variant to another. It is therefore instructive totake a look at the observational theory of π-calculus first.
A number of observational equivalences have been proposed and studied for
π-calculus [60] formulated using a uniform treatment of names. The early equivalence [43] is defined in terms of the standard bisimulation. But to guaranteethat the equivalence is closed under input prefix operation, it is required that if
two processes are equivalent then all their substitution instances are equivalent
as well. Consider the processes defined below.
C
D0
D1
A
B0
B1

def

=

def

=

def

=

def

=

def

=

def

=

u(x) | bd,u(x).bd + bd.u(x),u(x).bd + bd.u(x) + τ,c(u).C,c(u).D0 ,c(u).D1 .
66

Now C is early equivalent to neither D0 nor D1 because A is early equivalent toneither B0 nor B1 . However B0 + B1 is early equivalent to A + B0 + B1 since an
input action of A can be simulated by either B0 or B1 , depending on whether
the input name is b or not. The action
cz

A + B0 + B1 −→ z(x) | byfor example is simulated bycz

B0 + B1 −→ z(x).by + by.z(x).
Notice that z(x).by + by.z(x) is not early equivalent to z(x) | by. In a uniform
treatment of names, there are reasons that even B0 + B1 and A + B0 + B1
should not be regarded as equivalent. The argument is that in a distributed
computing framework, environments are always changing; it is more reasonable
to adopt a dynamic viewpoint. After B0 + B1 has simulated the cz action, theenvironments might have changed considerably so that they might be able tochange z to b. So we need to have equivalences capable of withstanding thestrong dynamic power of the environments. One such an equivalence is theopen bisimilarity of Sangiorgi [55, 22] and the quasi-open bisimilarity [59, 18] of
Sangirogi and Walker. Compared to the bisimilarity for CCS, the definition of
the open bisimilarity is complex for the reason that one needs to deal with an
infinite family of relations rather than a single relation.
Our adoption of the name dichotomy between names and name variablesconsiderably simplifies the observational theory of π-calculus. For example thebisimulation equivalence for π-processes can be defined just like in CCS.
Definition 14. A symmetric relation R on π-processes is a π-bisimulation if
the following statement is valid.
bλλIf P RQ −→ Q0 then P =⇒ P 0 RQ0 for some P 0 .
The π-bisimilarity ≈π is the largest π-bisimulation.
b
λλIf one replaces =⇒ by −→ in the above definition, one gets the structuralπ-bisimilarity ∼. We remark that we use the same notation ∼ in both π and
CCS. The overloading will never cause any confusion.
There is a more contextual approach to the equational theory of π-calculus.
Instead of imposing the bisimulation condition on the labeled semantics, thecontextual approach relies on barbedness condition on reductional semantics.
λWe say that a π-process P is immediately barbed at a, notation P ↓a, if P −→for some λ whose subject name is a, and that P is barbed at a if P =⇒↓ a. A
binary relation R is barbed if ∀a ∈ N .P ⇓a ⇔ Q⇓a whenever P RQ. We are now
in a position to introduce the barbed bisimilarity of Milner and Sangiorgi [45].
Definition 15. A symmetric barbed relation R on π-processes is a barbed πbisimulation if the following statements are valid.

67τ

1. If P RQ −→ Q0 then P =⇒ P 0 RQ0 for some P 0 .
2. R is closed under the composition and the localization operations.
The barbed π-bisimilarity ≈bπ is the largest barbed π-bisimulation.
Using the technique of [45], it is easy to prove the following fact.
Fact 4. The π-bisimilarity ≈π and the barbed π-bisimilarity ≈bπ coincide in
every π-variant studied in this paper.
Fact 4 is assuring in that the labeled semantics and the reductional semantics
give rise to the same equivalence relation on π-processes in a bisimulation framework. It also suggests that we may use either the labeled transition approachor the reductional approach to study the relative expressiveness of π-variants.
We go for the former option since it simplifies the proofs.
Definition 16. Suppose that π 1 and π 2 are two π-variants. A subbisimilarity
from π 1 to π 2 is a total relation R ⊆ Pπ1 ×Pπ2 such that the following statements
are valid whenever P RQ.
λ

b
λ

λ

b
λ

If P −→1 P 0 then Q =⇒2 Q0 for some Q0 such that P 0 R Q0 .
If Q −→2 Q0 then P =⇒1 P 0 for some P 0 such that P 0 R Q0 .
We say that π 1 is subbisimilar to π 2 , notation π 1 vπ π 2 , if there is a subbisimilarity from the former to the latter. The notations @π , vπ↓ , @π↓ are definedaccordingly.
Clearly the subbisimilarity relationship vπ is transitive. The largest subbisimilarity from a π-variant to itself is the π-bisimilarity ≈π .
In what follows we make use of Definition 16 to classify the interactabilityof the name passing interactions.

3.2

Choice in Pi

The relative expressiveness of choice operators in π-calculus bears resemblance
to that in CCS. As a matter of fact some of the results established in Section 2
can be readily stated for π-calculus since the proofs are almost unchanged.
Proposition 11. π − @π π m vπ π s and π −def @π π mdef vπ π sdef .
Proof. A reiteration of the proof of Proposition 1.
If Computation Criterion must be met, the picture remains the same as in
CCS.
Proposition 12. The following statements are valid.
(i) π s @π↓ π m @π↓ π.
(ii) π sdef @π↓ π mdef @π↓ π def .
68Suppose P is a π-process. The encoding of P is defined as follows:
def

JP K

=

(e)JP Ke .

The indexed translation JEKx is defined structurally as follows:
J0Kp

def

=

p,

Jλ.EKpdef=

p + λ.(e)JEKe ,J(a)EKp

def=(a)JEKp ,JE1 +E2 Kp

def

JE1 | E2 Kp

defµZ.(p + τ.(e)(JE1 Ke | e.Z) + τ.(e)(JE2 Ke | e.Z)),

JµX.EKp

def

=

=

=

µZ.(p + τ.(d)(µV.(τ.(e)(JE1 Ke | e.V ) + d.Z)
| µW.(τ.(e)(JE2 Ke | e.W ) + d))),(b)(b(c).cp | µX.b(c).c(z).(p + τ.JEKz ς)),where ς = {(b(c).cp1 | X)/JXKp1 , . . . , (b(c).cpi | X)/JXKpi }.
Figure 5: Translation from π to π m
Proof. Both the proof of π s @π↓ π m and the proof of π m @π↓ π are copies of theproof of Proposition 3.
The construction carried out in the proof of Proposition 17 indicates thatsome kind of dynamic binding for fixpoints can be achieved by making use of
the communication mechanism of π-calculus. This property is explored in the
proof of following proposition.
Proposition 13. π vπ π m .
Proof. We define a translation J Kp , indexed by the names, from π-processes to
π m -processes. This is given in Figure 5. The translation is very much like the
one given in Figure 2. The major differences are stated below.
• Whereas the encoding given in Figure 2 gives rise to a finite set of recursive equations, the structural definition in Figure 5 is nonrecursive. The
translation JP Ke of a π-process P is a π m -process. It is not a constantdefined by equations.
• While the extra recursions introduced by the encoding J Keϕ of Figure 2
are achieved through recursive constant definitions, they are realized by
fixpoints in the interpretation J Ke of Figure 5.

• Both encodings use names to trace back to the backup points. The interpretation of Figure 2 has to use two names e> , e⊥ in an alternatingmanner to keep track of the correct local pointers. On the other hand theencoding of Figure 5 does not need that dichotomy since the pointers canbe locally updated by internal communications.
69• The main semantic difference between the two encodings is their treatments of the recursions. In the interpretation of the constant definition
C=P
of CCSdef , the interpretation of an occurrence of C that appears in P
must be assigned of the correct pointer. This can only be done by using
the dynamic binding of CCSmdef . In the present interpretation ofµX.E
different occurrences of X in E get interpreted with different indexed
names by α-conversion. Let JXKe1 , . . . , JXKei be all the distinct indexedinterpretations of X in JEKz . In order for the internal computations of
JµX.EKe to act correctly, JXKe1 , . . . , JXKei must be interpreted asb(c).ce1 | X, . . . , b(c).cei | X
respectively.
The correctness of the encoding is proved in a completely same fashion as the
τ0
proof of Proposition 10. As in the proof of Proposition 10, the relation −→isintroduced to indicate internal computations. In(b)(b(c).cp | µX.b(c).c(z).(e + τ.JEKz ς))
which is the interpretation of JµX.EKe , the communications at b and c areinternal computations. Let R be the following relationτ∗

0{(P, Q) | JP K −→Q for some π process P }.

The relation R also satisfies a kind of bisimulation property, which is a consequence of the properties described next. The first property is the following
one.
τ

∗

τ

∗

0
0
If JP Ke −→Q then Q −→Q0 for some Q0 such that Q0 ∼ JP 0 Ke
0for some P ∼ P .

The proof of this property is almost the same as the proof of Lemma 51 ofτ0 τ0 τ0
Appendix A. If P ≡ µX.E, then JµX.EKe −→−→−→ JEKe ς are the threestep internal communications forced upon JµX.EKe . Here ς stands for some
substitution{(b(c).ce1 | X)/JXKe1 , . . . , (b(c).cei | X)/JXKei }.
It can be easily seen that JEKe ς ∼ JE{µX.E/X}Ke . Trivially E{µX.E/X} ∼µX.E. The second property is about simulation.
τ

λ

∗ λ

0
If P −→ P 0 in π-calculus than JP Ke −→−→ Q0 in π m -calculus for00 e0some Q such that JP K R ∼ Q .

70

In other words, the encoding of P simulates the operational semantics fully.
The proof of the second property is similar to that of Lemma 52 of Appendix A.
The third property is to do with operational reflection.
τ

∗ λ

λ

0
If JP Ke −→−→ Q0 in π m -calculus, then P −→ P 0 in π-calculus for0
some P such that P 0 R ∼ Q0 .

This last property says that the encoding simulates the operational semantics
faithfully. The proof is similar to that of Lemma 53 of Appendix A.
We conclude that R is a subbisimilarity.

3.3

Replication in Pi

Let’s now turn to the replication operator. The proof of (ii) of Lemma 26 isdone in such a way that can be routinely generalized to the π-setting. Hencethe following proposition.
Proposition 14. π m vπ↓ π m! and π s vπ↓ π s! .
Unlike in CCS, the converse of Proposition 14 fails. It appears that the
expansion law is critical for the validity of Lemma 37.
Lemma 45. π ! 6vπ↓ π m! .
Proof. Consider the process A = f (x).(a | x + c | x). Suppose there was a π m!
process B that was bisimilar to A. We may assume that B 9. Now consider
the actionfb
f (x).(a | x + c | x) −→ a | b + c | b.
(26)
It must be simulated byfb

B −→=⇒ D(27)

τfor some D such that ¬(D −→). Now D must be able to do the following actions
a

−→,

D

b

−→,

D
D

c

−→ .

Action (28) and action (30) must be induced by a same mixed choiceX
λi .Di

(28)
(29)
(30)

(31)

i∈I

for otherwise D would be able to do an a-action followed by a c-action. For
similar reason D must contain a mixed choiceX
λj .Dj
(32)
j∈J

71

that induces (29). Choices (31) and (32) should not be distinct for otherwise D
would be able to perform a b-action followed by either an a-action or a c-action.
Now suppose (31) and (32) are the same choice. The action sequencefa

B −→=⇒ D{a/c}can only be matched up byfaf (x).(a | x + c | x) −→ a | a + c | aτwhich is a contradiction since a | a + c | a −→ 0 yet D{a/c} 9.
An even more significant negative result about the expressiveness of π ! isstated next.
Proposition 15. π 6vπ↓ π ! .
Proof. We use RanT imerπ , defined in (25), as the counter example. Suppose
there were a process P in π ! that bisimulated RanT imerπ . By codivergenceproperty, we may assume that P 9. If we can prove that the set
aa{P 0 | P −→ P 0 }(33)

is finite, we may use the argument in the proof of Proposition 3 to complete theproof. The finiteness of (33) can be simply established as follows: The prefix aathat can be immediately fired cannot be underneath any replication operator.
This is because RanT imerπ cannot do an infinite sequence of aa action. But
then a simple structural induction suffices, bearing in mind that P may not doany τ -action.

3.4

Parametric Definition in Pi

In π-calculus dynamic binding is far more tricky than in CCS. Take for instancethe process ac.P | (c)(R | a(z).Q). One way to define the operational semantics
would be to admit following communicationτac.P | (c)(R | a(z).Q) −→ P | (c)(R | Q{c/z})
where the name c received through the communication gets captured dynamically. This way of defining the semantics seems to ban the α-conversion completely. But then one would haveτ(cc | a(c).P ) | a(z).Q −→ (c)((cc | P ) | Q{c/z})
in which cc has got bound as a side effect in a structural operational semantics!
This is really something undesirable. Even with the extra help of additional
syntactical gadgets to bypass this problem, there are still other unintended
communications like
τa(c).P | a(z).(c)Q −→ (c)(P | (c)Q{c/z}).
72

A standard solution to avoid such problems is to admit name escape. This
makes good sense since it goes along with the idea of dynamic name binding
very well. Now we can modify the above semantics in favour of the following
reduction:τ(xx | a(c).P ) | a(z).Q −→ (xx | (c)P ) | Q{c/z}.
The π-calculus with name escape does not have bound output actions, andaccording to the definition of this paper it is not a π-variant. Moreover it isconsiderably weaker than π-calculus proper, as we shall see. These observations
are significant in the following sense:• Since we do not allow name escape, we must keep the α-conversion.
• Since we allow the α-conversion, we must not have dynamic fixpoint operation. For the same reason constant definition should be prohibited.
We conclude that in π-calculus constant definitions are problematic.
The purpose of the above discussion is to explain why in π-calculus the parametric definitions [27] are always preferred. A finite set of parametric definitions
take the following shape:
D1 (x11 , . . . , x1n1 )= E1 ,..
.
Dn (xn1 , . . . , xnnn ) = En .
For each i ∈ {1, . . . , n}, the name variables xi1 , . . . , xini are parameters thatsatisfy the condition f v(Ei ) ⊆ {xi1 , . . . , xini }. When using the definiendum
Di (xi1 , . . . , xini ), the parametric names xi1 , . . . , xini must be instantiated. For
instance the expression Di (n1 , . . . , nni ) stands for Ei {n1 /xi1 , . . . , nni /xini }. The
power of parametric definition is due to the fact that, for each i ∈ {1, . . . , n},
the definiendum Di (xi1 , . . . , xini ) may appear in any of E1 , . . . , En in an instantiated form. The following is a concrete example of parametric definition.
D1 (x, y, z) = xx | (a)(zb | D2 (a, b, z)),D2 (x, y, z) = yy | (b)(za | D1 (a, b, z)).
Notice that the instantiations D1 (a, b, z) and D2 (a, b, z) are respectively theexpressions aa | (a)(zb | D2 (a, b, z)) and bb | (b)(za | D1 (a, b, z)). Another exampleof parametric definition isL(x)=(c)(xc | L(c)).

Clearly L(c0 ) admits the action sequence of (24).
Parametric definitions admit α-conversion. In [27] it is shown that parametric definitions and constant definitions are equivalent in CCS. This result
supports the view that constant definitions are abbreviations of parametric definitions.
73

def

J0K
X
J
λi .Ei K

=

def

=

i∈I

i∈I
def

J(a)EK

JE1 | E2 K

JD(n1 , . . . , ni )K0,X

λi .JEi K,=(a)JEK,

def

JE1 K | JE2 K,

=

def

=

(cD )(cD (c).cn1 . . . . .cni | µX.cD (z).z(x1 ). . . . .z(xi ).JEKς).

In the fifth line of the definition, we assume that D(x1 , . . . , xi ) = E is a parametric definition, that D(z11 , . . . , z1i ), . . . , D(zk1 , . . . , zki ) are all distinct instantiations of D(x1 , . . . , xi ) in E, and that the substitution ς is[(cD (c).cz11 . . . . .cz1i | X)/JD(z11 , . . . , z1i )K, . . . , (cD (c).czk1 . . . . .czki | X)/JD(zk1 , . . . , zki )K],and that cD , c are fresh names.
Figure 6: Translation from π mdef to π m
Let π def be π-calculus with parametric definition but without fixpoint operator. Let π mdef , respectively π sdef , be obtained from π def by replacing general
choice by mixed choice, respectively separated choice. It should not come as asurprise that parametric definition is strong enough to code up fixpoint.
Proposition 16. π vπ↓ π def , π m vπ↓ π mdef , π s vπ↓ π sdef .
Proof. Static fixpoints can be easily defined in terms of parametric definitions.
The expression µX.E, in which E does not contain any µ-operator, is translated
to the parametric definition
X(x1 , . . . , xn ) = E{X(x1 , . . . , xn )/X}.
The general fixpoint expressions can be translated in an inside-out fashion.
In the other direction, parametric definition can be simulated by fixpoint
operator, which draws a sharp contrast to the situation in CCS. The instantiation of a parametric definition can be achieved by local communication as longas choices are guarded. Milner has used this idea in [44] to code up parametricdefinitions in π m! -calculus.
Proposition 17. π mdef vπ↓ π m and π sdef vπ↓ π s .
Proof. The codivergent subbisimilarity from π mdef to π m is generated by anencoding from the former to the latter, which restricts to an encoding from π sdef
to π s . Formally the structural encoding from π mdef -processes to π m -processes
is defined in Figure 6. LetD(x1 , . . . , xi ) = E
74be a parametric definition. For simplicity we assume for the moment that E
does not contain any instantiation of any definiendum other than D. In E
there might be several instantiations of the definiendum D. To understand theencoding it is useful to think of D as being interpreted asµX.cD (z).z(x1 , . . . , xi ).JEKς

(34)

where cD is a name that can be used to access the definiendum and JEKς isobtained from JEK by replacing every instantiation of D by its encoding. The
encoding of the instantiation D(n1 , . . . , ni ) is given bycD (c).cn1 . . . . .cni | µX.cD (z).z(x1 , . . . , xi ).JEKς.

(35)

Obviously in (34) the expression (35) is equivalent to cD (c).cn1 . . . . .cni | X.
Hence the definition in Figure 6.
The intuition about the translation is that every time the fixpoint in (34) is
unfolded, the name variables in E are updated via internal communications.
Let’s now take a look at the operational aspect of the encoding. First of all
notice that in π m -calculus one has that
JD(n1 , . . . , ni )K =⇒ (cD )JEKς{µX /X}σand
JD(n1 , . . . , ni )K ≈π (cD )JEKς{µX /X}σwhere µX stands for µX.cD (z).z(x1 ). . . . .z(xi ).JEKς and σ is {n1 /x1 , . . . , ni /xi }.
It might occur to the reader whether something would go wrong if some occurrence cD (c).cn1 . . . . .cni communicates with another copy of µX rather than theneighboring µX . That such a communication would do no harm is guaranteedby the following property:
In π m -calculus, (cD )JEKς{µX /X}{n1 /x1 , . . . , ni /xi } is structural bisimilar to JE{n1 /x1 , . . . , ni /xi }K.

Now define the relation R from π mdef -calculus to π m -calculus as follows:def

R = {(P, JP K) | P is a π mdef process}.

Let ≈π↓ be the largest codivergent π-bisimulation. The composition R; ≈π↓ satisfies the following properties:• It is codivergent.
λλ• Suppose P1 R JP1 K ≈π↓ Q1 . If P1 −→ P2 then JP1 K =⇒ P 0 ≈π↓ JP2 K.
bλ

By definition some P 00 exists such that Q1 =⇒ Q01 ≈π↓ P 0 . Therefore
λJP2 K R ≈π↓ Q01 . In the other direction if Q1 −→ Q01 then P 0 exists suchb
λthat JP1 K =⇒ P 0 ≈π↓ Q01 . It can be proved that some P2 exists such thatbλP1 =⇒ P2 for some P2 such that JP2 K ≈π↓ P 0 . Hence P10 R ≈π↓ Q01 . So therelation R; ≈π↓ satisfies the bisimulation property.
75

D0 (x)Dτ.E (xez)z)
Dpq.E (xeDp(v).E (xez)
D(a)E (xez)
DE1 +E2 (xez)
DE1 | E2 (xez)
VE1 |E2 (xuez)
WE1 |E2 (xue
z)

=
=
=
=
=
=
=
=
=

x,
x + τ.(c)DE (cez ),x + pq.(c)DE (cez ),x + p(v).(c)DE (cez v),(a)DE (xez a),x + τ.(c)(DE1 (cez ) | c.DE1 +E2 (xez )) + τ.(c)(DE2 (cez ) | c.DE1 +E2 (xez )),x + τ.(c)(VE1 |E2 (xcez ) | WE1 |E2 (xcez )),τ.(c)(DE1 (cez ) | c.VE1 |E2 (xuez )) + u.DE1 | E2 (xez ),τ.(c)(DE2 (cez ) | c.WE1 |E2 (xuez )) + u,

where c is a fresh name.
Figure 7: Transformation from π def to π mdef .
We conclude that R; ≈π↓ is a subbisimilarity.
Having seen several encodings, it should now become a routine to give an
encoding from π def -calculus to π mdef -calculus. First of all we need to define
a transformation from π def -expressions containing no parametric definitions toπ mdef -expressions. This encoding is defined in Figure 7. It copies the idea of theencoding of CCS into CCSm . Next we generalize it to the processes containing
parametric definitions. Suppose the following definitions are in π def -calculus:
C1 (f
x1 )

= P1 ,..
.
Ci (xei ) = Pi .

Their translations are defined as follows:DC1 (fx1 )= DP1 ,..
.
DCi (xei ) = DPi ,where an instantiation Cj (en) on the right hand sides of these definitions istranslated to DCj (en). The verification that such an encoding is correct follows
the same argument given in the proof of Proposition 10.
Proposition 18. π def vπ π mdef .

76

3.5

Interaction Hierarchy of Pi

We have now obtained all the subbisimilarity relationships demonstrated in thefollowing reasoning:
π!

vπ↓

π

vπ↓

π def

vπ
vπ
vπ↓
vπ↓

π mdefπ sdef
πs
πm

vπ↓

π m!

vπ↓

π s!

vπ↓

π! .

The propositions involved in the above inference are Proposition 18, Proposition 17, Proposition 16 and Proposition 14. These subbisimilarity relationships
lead to the first of the two main results of this section.
Theorem 3. All the nine π-variants are interactively equivalent.
Theorem 3 reinforces our belief that communications in π-calculus is far morerobust than the interactions of CCS. The name passing mechanism is so strongthat a restriction of it often would not reduce its interactive power and that it
often uplifts a weak form of an operator to be just as expressive interactively asa strong form of the operator.
Having said that, different π-variants do differ if Computational Criterion istaken into consideration. The following theorem states the second main resultsof the section.
Theorem 4. The codivergent subbisimilarity relationships between the nine πvariants are depicted in Figure 8.
Proof. The negative result π ! 6vπ↓ π m! can be promoted to π 6vπ↓ π m and π def 6vπ↓
π mdef .
The nine π-variants can be classified to at most five equivalence classes.
Mixed choice, and separated choice as well, forces the three forms of recursion
to be equivalent.
The only open problem left for further study is stated next.
Problem 1. π def vπ↓ π?
Consider Local Random Timer defined as follows:
LT imer(x)def=aa + (c)(xc | LT imer(c)).
77

?

π

π!

π mdefπm

π m!

π sdef

πs

π s!

π def

Figure 8: Codivergent Subbisimilarities of Pi
This process is in π def -calculus. It has the following operational behavior:c0 (c1 )ci (ci+1 ) aa ci+1 (ci+2 )LT imer(c0 ) −→ . . . −→ −→−→cj (cj+1 ). . . −→ 0

for any chosen j ≥ i ≥ 0. An interesting operational property of Local Random
Timer is demonstrated in the following transition:c0 (c1 )LT imer(c0 ) −→ LT imer(c1 ) ∼ LT imer(c0 ){c1 /c0 }.
We conjecture that there is no π-process that can bisimulate LT imer(c0 ) in a
non-divergent way. Although the conjecture has not been proved, the following
remarks might be useful for further investigation. Assume that there were aπ-process P that bisimulated LT imer(c0 ) and that P cannot do any τ -action.
Here are some observations about P :1. Since P can perform both the aa-action and the c0 (c1 )-action, it cannot
be in prefix form.
2. Suppose that P is a composition P0 | P1 . Then either P0 ∼ 0 or P1 ∼ 0.
Otherwise the operational behavior is different from that of LT imer(c0 ).
So we may assume that P is not a composition.
3. Suppose that P is a summation P0 +P1 . Without loss of generality, we
c0 (c1 )may assume that P0 −→ =⇒ P00 ≈ LT imer(c1 ). Hence P00 {c0 /c1 } ≈LT imer(c0 ) ≈ P .
4. There must be a subexpression aa.A of P underneath a µ-operator. Otherwise there would be only a finite number of aa-derivatives.
5. There must be a subexpression of the form µX.E such that there is anunguarded occurrence of X in E. Otherwise there would be only a finite
number of aa-derivatives.
78

6. There must be a subexpression of the form µX.E such that there is a
subexpression aa.A of E and that there is an unguarded occurrence of X
in E. Moreover aa.A and the unguarded occurrence of X must not be ina concurrent position.
7. No reachable occurrence of X in µX.E can be in concurrent position withthe unguarded occurrence of X. Otherwise P would be able to do two aa
actions sequentially. Such unreachable occurrences of X can be removed.
The intuition is that after action ci (ci+1 ), a component of the residual of theaction must pass ci+1 to another concurrent component via a local name. The
above observations suggest that action aa cannot maintain this capability whilesetting the timer randomly.

4Application of Subbisimilarity

In this section we put into use the results obtained in Section 2 and Section 3.
We shall be discussing two issues. One is about the independence of the operators of π-calculus. This problem cannot be tackled without any results on
expressiveness. The other is about choosing a representative among the variantsof a process calculus. This is made easier by the results on expressiveness.

4.1

Operator Independence

An important application of a theory of expressiveness is to formally establish
the independence of process operators. In this section we take π-calculus as an
example to explain the general approach.
Let π0 be a π-variant and π0−op be obtained from π0 by removing the operator
op and the associated operational rules from π0 . We say that the operator op is
independent to the other operators of π0 if π0 6vπ π0−op .
The name passing communication mechanism of π-calculus makes possible
the internalization of the conditionals useful in programming. It is interesting tosee how the conditionals enhance the interactability of π-calculus. The syntaxesof the match and the mismatch operators are [p=q]E and [p6=q]E respectively.
The semantics is defined by the following rules.
λλE −→ E 0

E −→ E 0λλ[a=a]E −→ E 0[a6=b]E −→ E 0

We use the notations π = , π 6= and π c to stand for the π-variant with respectively
the match operator =, the mismatch operator 6= and both the match and mismatch operators. In view of Theorem 3, we assume that the recursion capacityof π c (π = , π 6= ) is provided by replication. It is clear that π vπ π = (π 6= ) vπ π c .
More about the interactability of the conditionals are given next.
Proposition 19. The following statements are valid.
(i) π = 6vπ π and π = 6vπ π 6= .
79

(ii) π 6= 6vπ π and π 6= 6vπ π = .
(iii) π c 6vπ π = and π c 6vπ π 6= .
Proof. (i) Consider a(x).[x=c]bb. Suppose a(x).[x=c]bb R P for a π-process P
and a subbisimilarity R from π = to π. The two consecutive observable actionsacbba(x).[x=c]bb −→ [c=c]bb −→ 0 must be simulated by P in the manner P =⇒acbb

P1 −→ P2 =⇒ P3 −→ P4 =⇒≈ 0. We claim that for a fresh d some P20 , P30 , P40
exist such thatadbb
P1 −→ P20 =⇒ P30 −→ P40 .
(36)This fact can be proved by induction. The tricky part is to do with prefix
operator. Suppose without loss of generality that P1 ≡ a(x).P10 . Then clearly
P10 {c/x} ≡ P2 and P10 {d/x} ≡ P20 . It should be clear that P2 ≈ bb. Thisequivalence implies that the internal actions in P2 =⇒ P3 must be via local
names. Since P2 does not contain any match operations, the substitution {c/x}bbdoes not enable any internal actions in P10 . Therefore P10 =⇒−→, from whichad(36) follows. But (36) contradicts the fact that a(x).[x=c]bb −→ [d=c]bb. Henceπ = 6vπ π. The argument for π = 6vπ π 6= is similar.
(ii) Suppose a(x).[x6=c]bb were equivalent to a process P of π (π = ). Foraebba fresh e the two consecutive actions a(x).[x6=c]bb −→ [e6=c]bb −→ 0 must be
ae

bb

ac

bb

simulated by P =⇒=⇒. But then P =⇒=⇒, which cannot be simulated bya(x).[x6=c]bb of course.
(iii) The proofs are similar.
Theorem 5. All the operators of π c -calculus are independent.
Proof. Prefix operator and fixpoint operator are easily seen to be independent
from the other operators. The proof of Proposition 11 shows that choice operator is independent. Proposition 19 says that match, and mismatch as well, is
independent from the rest of the operators of π c -calculus.
Localization operator is independent because restricted output actions areinteractively different from input actions and free output actions. We will go
for a formal proof of this fact. Consider Counterπ . It is easy to check that
only after performing equal numbers of inc’s and dec’s can Counterπ do a zeroaction. For instance the following is an admissible sequence of actions:inc

inc decdec zeroCounterπ =⇒. . =⇒}=⇒. . =⇒} −→ .
| .{z
| .{z
i timesi times

Let π −L be obtained from π-calculus by removing the localization operator.
Now π −L does not have any bound output actions. A translation from π to
π −L must explain how the observable actions of the former are translated to
the latter. In other words we need to specify a map of the following type.
ι : {ac, ac, a(c) | a, c ∈ N } → {ac, ac | a, c ∈ N }.

80

In the present proof we do not have to assume anything for ι, which makes
our negative result really strong. We prove that π-calculus cannot be encodedin π −L -calculus by showing that there is no π −L -process that can demonstrate
the operational behavior of Counterπ under any map ι whatsoever. Let us saythat a π −L -process P0 has Counting Property if there exist pairwise distinct
a, b, c ∈ N ∪ N such that following four conditions hold.
• The following infinite action sequence is admissible
ad

ad

ad

i
1
0
....
. . . Pi =⇒
P1 =⇒
P0 =⇒

ad

(37)

adi−1

bej−1

be

0
0
. . . =⇒
. . . =⇒ Pi then e0 , . . . , ei−1 , f0 exist such that Pi =⇒• If P0 =⇒cf0

Pi+j −→ for some Pi+j .
• The action sequence (38) is admissible only if i = j.
adadi−1 be

bej−1

cf0

0
0
P0 =⇒
. . . =⇒ =⇒. . . =⇒ Pi+j −→ .

(38)

• P0 can never ever perform an action dd such that d 6∈ {a, b, c}.
For such a P0 , notice that in (37) the set of the object names {d0 , d1 , . . . , di , . . .}could be infinite. But (37) corresponds to an infinite sequence
ad0

ad0

ad0

0
1
i
P0 ≡ P00 =⇒P10 =⇒. . . Pi0 =⇒
...

(39)

where {d00 , d01 , . . . , d0i , . . .} is finite. The claim is based on two observations:• A subexpression a(z).A of Pi can be activated only if a ∈ {a, b, c}. A
subexpression az.A of Pi can be activated only if a ∈ {a, b, c}. Consequently if a(z).A is a subexpression of Pi and z(x).B (or zy.B) is a subexpression of A, then z(x).B (or zy.B) is not fireable unless z is instantiatedby a name that appears in a, b, c.
• Suppose there are k distinct match or mismatch operators in P0 . In addition to gn(P0 ), we only need a set B of 2k + 1 fresh names. Without lossof generality, we may always assume thatB ∩ {d0 , d1 , . . . , di , . . .} = ∅.
Now we replace the object names in (37) inductively. If ad0 is an output
action or d0 ∈ gn(P0 ) ∪ B then do nothing, otherwise choose a name d00
in B that does not change the validity of the conditions in the immediate
descendent of the action ad0 . This is possible since there are only k distinct
matches and/or mismatches. Let P10 be P1 {d00 /d0 }. We then continue with
P10

ad1 {d00 /d0 }=⇒P2 {d00 /d0 }ad2 {d00 /d0 }=⇒. . . Pi {d00 /d0 }In this way we obtain an action sequence like (39).
81

adi {d00 /d0 }

=⇒

....

By extending the definition of the concurrent subexpression to take into accountof the conditionals, we can modify Lemma 44 to show that (39) is well quasiordered with Compatibility Property. Consequently Pi0  Pj0 for some i < j.
Therefore the following action sequencead0

ad0j−100
ad00
i−1 be

ad00

00
be00
i−1 cf00
0
0
P00 =⇒. . . =⇒ Pj0 =⇒. . . =⇒ =⇒. . . =⇒ −→is admissible, which contradicts (38).
Without localization operator, we cannot even define the counter in πcalculus. We conclude that there is no encoding from π-calculus to π −L -calculusthat preserves interactability.
The crux of the matter is that the standard localization operator provides
a mechanism to generate new names. This is the essential difference between
π-calculus and the value-passing calculus based on CCS. In the framework of
π-calculus, it is the localization operator that gives rise to Turing computability.
Proposition 20. π −L -calculus is not Turing complete.
Proof. The termination property in π −L -calculus is decidable. An algorithm
that checks this property works as follows: Given a π −L -process P , the numberof the immediate τ -actions P may perform is finite. Using this finite branchingproperty we can generate the τ -action tree of P in a breadth first fashion.
The nodes of the tree are processes and the edges are labeled by τ . Uponthe generation of a node B, it is checked if there is an ancestor A of B suchthat A  B. It is easy to see that there is a recursive algorithm to decide
. The generation of the tree terminates with two outcomes. If the tree isfinite, the algorithm terminates with answer “yes”. Otherwise a node B mustbe found such that A  B for some ancestor A of B. In this case the algorithm
terminates with answer “no”. The correctness of the algorithm is guaranteed by
the fact that an infinite τ -action sequence in π −L -calculus is well quasi-orderedby Lemma 44.
If π −L -calculus were Turing complete, then according to the condition (5)given after Definition 6 there would have been an algorithm that translates
every Deterministic Turing Machine to a π −L -process. By the conditions (3,4)
after Definition 6, the translation satisfies the property that a Deterministic
Turing Machine is terminating if and only if its interpretation in π −L -calculus
is terminating, the latter being decidable. It follows that one could design analgorithm for the halting problem.

4.2

Model Assessment

A theory of expressiveness should help us in finding an appropriate form ofa process calculus among all of its variants. Since we have investigated theexpressiveness of CCS-variants and π-variants, we can say something about
their candidacies.

82

4.2.1

CCS with Sufficient Computing Power

Lemma 36 implies some decidability results for CCS. The decidability of the termination property of CCS! is established in [7]. That result can be strengthened
significantly.
Proposition 21. In CCS it is decidable to check if a process admits an infinite
action sequence.
Proof. The expansion order for CCS is a well quasi-order that satisfies the compatibility property. So a proof of the proposition is essentially given in the proofof Proposition 20. Given a CCS process P , the algorithm traverses the action
tree of I ! (Ia (P )), where a is fresh. Upon generating a node P 0 the algorithm
checks if there is an ancestor P 00 of P 0 such that the path from P 00 to P 0 consistsof only a-actions and the number of the consecutive a’s is Na (P 00 ). If the answer
is yes, then P 0 is marked and the algorithm will overlook all the derivatives of
P 0.
A practical implication of Proposition 21 is that none of CCSm , CCS! andCCS can code up all Turing machines. The proof of this fact is the same as thatof Proposition 20.
Theorem 6. None of CCS! , CCSm and CCS is Turing complete.
For both theoretical and practical reasons, a process calculus that is not Turing complete is undesirable. It follows that CCSdef and CCSmdef are preferable
to any of CCS! , CCSm and CCS. Interactively CCSdef and CCSmdef are equivalent. The latter has an edge over the former since the bisimilarity of CCSmdef
is a congruence. We conclude that CCS with constant definitions and guarded
choices should be chosen in practice.
4.2.2

Pi with Simple Semantics

Now what do our results on the expressiveness of π-variants tell us about candidacy? Theorem 3 assures us that each of the nine variants can be chosen
without losing expressive power. But the diagram in Figure 8 says somethingmore.
• It is more convenient to program in the variants with mixed choice than in
the ones with separated choice. A simple program like counter is naturally
designed using mixed choice.
• The convenience offered by the variants with unrestricted choice is mainly
to do with infinite branching. Theoretically finite branching is preferred.
Practically infinite choice can be simulated by mixed choice anyway. Moreover the unrestricted choice operator is not always a congruence operator.
Mixed choice does not have that problem.

83

It seems that having mixed choice in π is a good choice. Which of the threevariants with mixed choice do we prefer? Well if we do not go into the higher
order scenario, we should prefer π m! since it is a purely first order calculus.
In both theory and practice, match operator is frequently necessary. It allows
one to write if then commands in π-calculus and makes it possible to state
an expansion law for π-calculus. If we put match operator in the repertoire of
π-calculus, we get nine variants with match combinator. In view of Theorem 5,
the operator strictly increases the expressive power. An interesting question is
if Theorem 3 and Theorem 4 hold for the nine new variants. Our preliminary
investigation seems affirmative. But details remain to be checked. Let π != be π !
extended with match operator. In π != the following structural equalities hold:
X
X
[p=q]
λi .Pi ∼[p=q]λi .Pi ,
i∈I

i∈I

[p=q](P | P 0 ) ∼ [p=q]P | [p=q]P 0 ,[p=q](a)P ∼ (a)[p=q]P,[p=q]!P ∼ ![p=q]P.
These equalities strongly suggest the following alternative syntax of π != -calculus:XP :=ϕi λi .Pi | P | P 0 | (a)P | !P,
(40)
i∈I

where ϕi is a finite conjunction of matches. Now actions are conditioned; but
programs are not. Let π if denote this variant. The following fact is obvious.
Proposition 22. π if vπ↓ π != vπ↓ π if .
Proof. π if vπ↓ π != is obvious. The proof of Lemma 37 can be carried out in the!=present
to a π m= -process of the
P setting. A π -process is structurally bisimilar
ifform i∈I ϕi λi .Pi , which can be bisimulated by a π -process. So we also have
π != vπ↓ π if .
If π if -calculus is further promoted with if then else capacity, it need to incorporate mismatch operator. But how should the combinator be incorporated?
The answer is to stick to the syntax of (40). Let π case be this calculus. Let π !cbe π ! -calculus extended with the conditionals. The following fact is assuring.
Proposition 23. π case vπ↓ π !c vπ↓ π case .
Proof. The proof is the same as that of Proposition 22.
The above proposition suggests that we may as well choose π case as the
π-calculus.
The exercises carried out in this and previous subsections intend to convey
the following picture: When designing a process calculus, we are often given a
lot of candidates. We should evaluate the candidates according to some criteria.
The criteria may concern pragmatics, algebraic beauty, programming style etc..
Formal expressiveness results should play a key role in some design decisions.
The final design should also be evaluated in terms of expressiveness.
845More Subbisimilarities

In this section we apply the technique of subbisimilarity to study expressivenessfor some π-related calculi. The π-calculus with dynamic binding has a localization operator that behaves like a physical ambient. The value-passing CCS
is closer to CCS than to π-calculus. The asynchronous π-calculus has a quite
different observational theory from π-calculus. The internal π-calculus stays
right in between CCS and π-calculus.

5.1

Name Escape Communication

An alternative to the name extrusion ruleac

E −→ E 0a(c)(c)E −→ E 0
is the following name escape rule.
ac

E −→ E 0ac(c)E −→ (c)E 0
Let π d be π-calculus with the name escape. In π d -calculus one has typicallyfollowing communicationτa(z).P | (c)(R | ac.Q) −→ P {c/z} | (c)(R | Q).
It is clear from the above communication that α-conversion must be bannedin π d . One of its implications is that in π d -calculus name capture must be
admissible. So we should haveτ(c)(R | a(z).P ) | ac.Q −→ (c)(R | P {c/z}) | Q.
A further consequence is that in π d -calculus fixpoint operator is dynamic. A
minute’s thought would lead the reader to conclude that π d -calculus is strictly
more powerful than π d! -calculus, where π d! stands for the π d -calculus with replication instead of dynamic fixpoint operator.
In π d -calculus as well as π d! -calculus there is no bound output. We leave thedefinition of the subbisimilarity vd to the reader.
Proposition 24. π d! vd↓ π d 6vd π d! .
Proof. In π-calculus with dynamic binding, localization operator is never relod!
cated. We could define an expansion order π in the standard manner. If theinfinite action sequence
λ

λ

λ

0
1
2
P0 −→
P1 −→
P2 −→
...

85

(41)

in π d! -calculus satisfies the condition that the set{c | ∃i≥0.∃a∈N .λi = ac}(42)

is finite, then the conditions of Lemma 44 are met. In this case (41) is wellquasi-ordered. If the condition (42) does not hold, we can obtain an infinite
action sequence from (41), as we have done in the proof of Theorem 5, suchthat (42) is satisfied by the new action sequence. In either case we can showthat no π d! -process satisfies Counting Property. On the other hand CCSdef canbe embedded in π d -calculus. So the counter can be defined in π d -calculus.
The following corollary is implied by the above proof.
Corollary 8. π d! -calculus is not Turing complete.
It follows that π d! -calculus has to be abandoned. However π d -calculus is anatural extension of CCSdef and is quite interesting.

5.2

Value-Passing CCS

In π-calculus the content of a communication is nothing but names, whereas
in value-passing CCS the content of a communication may contain anything
but names. The value-passing CCS [39, 33, 36], CCSvp for short, makes use of
two oracles, a data algebra D and a boolean algebra B. The algebra B is the
propositional logic with the equality judgment = on data expressions of D. The
set of the data expressions Dexp, ranged over by e, e0 , . . . is constructed from D
and the set of the data variables Dvar. The set Bexp of the boolean expressions,ranged over by φ, φ0 , . . . is constructed from B and the set Bvar of the boolean
variables.
The following is the BNF grammar of CCSvp expressions
E:= 0 | X | λ.E | E | E 0 | (a)E | if φ then E | E+E 0 | µX.E,

where λ ∈ {a(x), a(e) | x ∈ Dvar, e ∈ Dexp} ∪ {τ } and φ ∈ Bexp. Depending on
how we deal with data and boolean expressions, the operational semantics of
CCSvp can be classified into two types. The symbolic semantics [33, 36] is basedon a proof theory of data and boolean domains. The concrete semantics [39] isbuilt on a model theory of data and boolean domains. The evaluation function
J K returns the value of an expression e (or φ) whenever e (or φ) contains neither
domain variables nor boolean variables. The concrete semantics of CCSvp isdefined by the following rules.
Prefixa(v)ττ.E −→ E

a(x).E −→ E{v/x}

JeK = va(v)a(e).E −→ E

Composition
λE −→ E 0λ

E | F −→ E 0 | F

a(v)

a(v)

E −→ E 0
F −→ F 0τ
E | F −→ E 0 | F 086Restriction
λE −→ E 0

a does not appear in λλ(a)E −→ (a)E 0
Condition
λE −→ E 0

JφK = >
λif φ then E −→ E 0
ChoiceλE −→ E 0λ

E+F −→ E 0
Recursion
λE{µX.E/X} −→ E 0
λµX.E −→ E 0
Without assuming too much on the domain and boolean algebras, one may
define in CCSvp the counter as follows:
Cvp
Zvp
Ovp
Ivp
Dvp

def

=

def

(c)(c0 | µX.c(x).(Zvp + Ovp )),=if x>0 then (Ivp + Dvp ),def=

if x=0 then (Ivp + zero(0).(X | c0)),def=

inc(1).(X | c(x+1)),

def

dec(1).(X | c(x−1)).

=

The counter can increment by performing inc(1), decrement by performingdec(1), and indicate that the current value is zero by performing zero(0). Noticethat this example can be defined using replication.
We shall define subbisimilarities between CCSvp variants in the style of concrete semantics.
Definition 17. A subbisimilarity R from CCS1vp to CCS2vp is a total relation
R from PCCS1vp to PCCS2vp such that the following statements are valid.
bλλ

1. If QR−1 P −→1 P 0 then Q =⇒2 Q0 R−1 P 0 for some Q0 .
λbλ

2. If P RQ −→2 Q0 then P =⇒1 P 0 RQ0 for some P 0 .
We write CCS1vp vvp CCS2vp if there is a subbisimilarity from CCS1vp to CCS2vp .
The notation vvp↓ is defined accordingly.
As in the case of CCS, we can define the eight variants of CCSvp . For instance
CCS!vp is CCSvp with replication operator rather than fixpoint operator. We
shall not investigate in detail the relative expressiveness of the nine variants ofvalue-passing CCS. But it suffices to say that the theory of value-passing CCS
parallels that of CCS to a great extent.
87

vp
The proof of Proposition 1 can be used to show that CCSm
CCSsvp . The
vp v
vp
vp
s
mdef
negative results CCSm
6v↓ CCSsdef
vp 6v↓ CCSvp and CCSvp
vp can be proved as
mdef
in the proof of Proposition 3. Using the proof of CCS 6vccs
CCSof Fact 3, we↓
vp
m
can prove CCSvp 6v↓ CCSvp with the help of the process µX.(a(0) + b(0) | X).
The properties established in Section 2.3.2 do not depend on the particularforms of prefix operations. They are all valid for value-passing CCS. The proof
of Lemma 37 can also be transplanted to the value-passingPsetting. A process in
CCS!vp is structurally bisimilar to a process of the form i∈I if ϕi then λi .Pi
vp!
in CCSgm
vp , using the expansion law for value-passing CCS. Hence CCSvp v↓
vp
vp
vp
!
s
s!
s
CCSm
vp v↓ CCSvp . Similarly CCSvp v↓ CCSvp v↓ CCSvp . The proof of
def
mdef
sdef
Proposition 10 shows that CCSvp vvp CCSvp vvp CCSvp .
Suppose that P0 is a CCSvp -process that does not use any operators of thedata algebra D and that the boolean expressions appeared in P0 contain only
the propositional logic operators and the syntactical equality ≡ judgement. If
P0 induces an infinite action sequence
λ

λ

λ

0
1
i
P0 −→
P1 −→
. . . Pi −→
...

(43)

then using the idea explained in the proof of Theorem 5, one could easily modify
the sequence (43) in such a way that a new infinite sequence
λ0

λ0

λ0

0
1
i
P0 −→
P1 −→
. . . Pi −→
...

(44)

is obtained that validates the proposition “{vi | λ0i = ai (vi )} is finite”. Consequently (44) is well quasi-ordered with respect to . This leads immediately tothe following proposition.
Proposition 25. CCSvp is not Turing complete without using the domain
knowledge of D.
If the data algebra D is equipped with enough structure, value-passing CCS
would be Turing complete. If this happens, the method we have used to tellapart CCSdef , CCS and CCS! fails in the value-passing framework. The issue!
of the relationships among CCSdef
vp , CCSvp and CCSvp has to be investigated inanother occasion.

5.3

Asynchronous Pi

Asynchronous communications are those in which the parties that release messages immediately go ahead without waiting for any acknowledgements fromthe receiving parties. In the setting of π-calculus the asynchronous output canbe defined by the following semantic rules.
τacac −→ 0ac.P −→ ac | P

It is apparent that ac.P is bisimilar to ac | P under this semantics. This fact
tells us that if we want to study asynchronous communications in π-calculus,
88we might as well focus on the following syntax:
P:= 0 | n(x).P | nm | P | P | (a)P | !P.

This is the so-called asynchronous π-calculus, often denoted by π a . A form of
restricted output prefixing is definable in the asynchronous calculus using the
concurrent composition operator:
defa(c).c(x).P = (c)(ac | c(x).P ).
The variants of π a -calculus include the followings:
P• π i is π a -calculus plus input choice i∈I ai (x).Pi , where I is finite;ais π a -calculus plus match conditional prefix ϕa(x).P ;
• π=
P
i
• π=
is π a -calculus plus match conditional choice i∈I ϕi ai (x).Pi ;a• π6=is π a -calculus plus mismatch conditional prefix ϕa(x).P ;
P
i
• π6=
is π a -calculus plus mismatch conditional choice i∈I ϕi ai (x).Pi ;• πca is π a -calculus plus conditional prefix ϕa(x).P ;P• πci is π a -calculus plus conditional choice i∈I ϕi ai (x).Pi .
In the asynchronous calculi, ac is a message that has been sent out by someprocess but has not yet been received by any process. It does not really makesense to place any condition right in front of ac.
The algebraic theory of π a -calculus has been studied by several researchers [6,34, 3, 46, 49, 47]. These researchers have reached to a consensus on how theasynchronous processes can be observed. An asynchronous observer differs in
observing power from a synchronous one in that the former cannot really see
any input actions performed by observees. Consequently the subbisimilarity relationships between two π a -variants do not explicitly bisimulate input actions.
The abilities to perform input actions are compared by the effects they exert onneighboring processes. A typical equality valid in π a -calculus isa(x).ax ≈ 0.

(45)

Equality (45) is characteristic of the observational theory of the asynchronous
calculi. It also underlies most encodings between asynchronous calculi.
The exclusive observability of output actions does not mean that input actions can be ignored. The simple process a(x) for example may consume theprocess ac as it were. So the presence of a fireable input prefix could be detected in a roundabout way. An observational equivalence for asynchronous
calculi need to take that into account. In [3] the authors offer basically two
approaches to deal with input actions. One is to work out how the input actions are explicitly simulated in a labeled transition semantics. The other is toleave the simulation of input actions implicit but to impose the condition that89

the observational equivalence is closed under composition. The former is more
tractable whereas the latter is more robust. In this paper we opt for the second
approach. This is because we will compare π a -calculus against the synchronous
calculus π s . Only the latter approach provides a uniform tool to carry out thecomparison.
Definition 18. Suppose π1 and π2 are two π-variants. An asynchronous subbisimilarity from π1 to π2 is a total relation R from Pπ1 to Pπ2 such that thefollowing statements are valid.
(i) If P1 RQ1 and P2 RQ2 then P1 | P2 R Q1 | Q2 .
(ii) The following bisimulation property holds whenever P RQ.
λ

b
λ

λ

b
λ

• If P −→1 P 0 for some λ ∈ {ac, a(c) | a, c ∈ N } ∪ {τ }, then Q =⇒2 Q0 forsome Q0 such that P 0 RQ0 .
• If Q −→2 Q0 for some λ ∈ {ac, a(c) | a, c ∈ N } ∪ {τ }, then P =⇒1 P 0 forsome P 0 such that P 0 RQ0 .
We say that π1 is asynchronously subbisimilar to π2 , notation π1 vasy π2 , ifthere is some asynchronous subbisimilarity from the former to the latter. The
asynotations @asy , vasy
are defined accordingly.
↓ , @↓
Definition 18 is formulated to reconcile the asynchrony with the synchrony.
The following proposition explains.
Proposition 26. Suppose π 1 and π 2 are two synchronous π-variants. The
following statements are valid.
(i) π 1 vasy π 2 if and only if π 1 vπ π 2 .
(ii) π 1 vasy
π 2 if and only if π 1 vπ↓ π 2 .
↓Proof. Suppose π 1 and π 2 are two synchronous π-variants. Let R be a subbisimilarity from π 1 to π 2 in the sense of Definition 16. We define an infinite
sequence of relations from π 1 to π 2 by the following induction.
def• v0 = R;
P1 vi P2 , def• vi+1 =((a)P1 , (a)P2 ), (P1 | P10 , P2 | P20 ) P10 vi P20 ,.
and a ∈ NS
Now let v∞ be i∈ω vi . It is a standard exercise to show that v∞ satisfies
the bisimulation property of Definition 18. By construction it is closed undercomposition. Hence π 1 vasy π 2 . If R satisfies the codivergence condition, thenit follows from the bisimulation property that v∞ also satisfies the codivergencecondition.
ae
Let A be an asynchronous subbisimilarity from π 1 to π 2 . Suppose P AQ −→Q0 . For names b, c that appear neither in P nor Q, there must be some processaebc

B in π 2 such that ae.bc A B. It should not be difficult to see that B =⇒=⇒∼ 0.
90

τ

bc

Consequently P | ae.bc A Q | B =⇒=⇒∼ Q0 | 0. It follows from the bisimulationaeproperty that P =⇒ P 0 and P 0 | 0 A Q0 | 0. We conclude that ∼ A ∼ isa subbisimilarity from π 1 to π 2 in the sense of Definition 16. Obviously ∼A ∼ satisfies the codivergent condition if and only if A satisfies the codivergent
condition.
Proposition 26 asserts that asynchronous subbisimilarity provides a uniform
criterion for comparing the interactability of both asynchronous π-calculi aswell as the synchronous π-calculi. In the rest of this subsection we use the asynchronous subbisimilarity to characterize interactability. The next theorem saysthat the conditionals also add substantial expressive power in the asynchronous
setting.
Proposition 27. The following statements are valid.
aa@asy πca .
@asy πca ; π a @asy π6=(i) π a @asy π=
i
asy i
asy i
i
asy i
π6= @asy πci .
πc ; π @(ii) π @π= @Proof. The inclusion maps are all asynchronous subbisimilarities. The proa
cesses a(x).(c)(cc | [x=d]c(z).bb) and a(x).(c)(cc | [x6=d]c(z).bb) are in π=-calculusaand π6= -calculus respectively. They can be used to show that there are no
asynchronous subbisimilarities in the opposite directions. Suppose there wereaan asynchronous subbisimilarity R from π=-calculus to π a -calculus and thata(x).(c)(cc | [x=d]c(z).bb) R P for some P in π a -calculus. Suppose further that
adRA and aeRB. Since R is closed under composition, one must havead | a(x).(c)(cc | [x=d]c(z).bb) R A | P,
ae | a(x).(c)(cc | [x=d]c(z).bb) R B | P.

(46)
(47)

By definition the only observable action A can do is ad. For the same reason B
cannot do any observable actions apart from ae. It follows from (46) and (47)thatae

P 0 ←−⇐= P

ad

bb

=⇒=⇒

(48)

for some P 0 that cannot do bb. As in the proof of Proposition 19, the twosequences of actions in (48) contradict each other.
The relationship between π a -calculus and π i -calculus has been studied by
Nestmann and Pierce in [46]. They proved a remarkable result that these two
calculi are interactively equivalent from the point of view of asynchronous communication.
Fact 5 (Nestmann, Pierce [46]). π i vasy π a .
Proof. The encoding from π i -calculus to π a -calculus is homomorphic
on all butP
the input choice P
operator. Nestmann and Pierce’s encoding J i∈I ai (x).Pi K of
the input choice i∈I ai (x).Pi is defined byY!ai (x).c(y, z).T esti (y, z))(c)(c(e, f ).e |i∈I91where T esti (y, z) stands fory.(c(e, f ).f | Pi ) | y.(c(e, f ).e | ai x) | z.(c(e, f ).f | ai x)
and c(y, z).P , c(e, f ).Q are defined respectively as follows:c(y, z).Pc(e, f ).Q

def=c(u).u(v).v(y).u(z).P,

defc(u).u(v).(e)(f )(ve | uf | Q).

=

The basic idea is that no input action is prohibited. But once some input has
been committed, all the other input actions must be undone. The trick is to
use the flag c(e, f ).e to indicate that no input has been committed and the flagc(e, f ).f that some input has been committed. The component y.(c(e, f ).e | ai x)of T esti (y, z) is indispensable. Without it internal loops would break down.
The technique used to prove the above fact can be easily adapted to a proofof the following fact.
i
a
a
i
; π6=
vasy π6=; πci vasy πca .
vasy π=Fact 6. π=

However the above equivalences fail if computational factor is taken into
account. It is conjectured in [46] that there is no termination preserving fully
abstract encoding from π i -calculus to π a -calculus. The next proposition confirms the conjecture.
aaii
Proposition 28. π a @asy
@asy
; π6=
@asy
π i ; π=π=π6=; πca @asy
πci .
↓
↓
↓
↓

Proof. If π i vasy
π a were true, there would be an asynchronous subbisimilarity↓i
R from π -calculus to π a -calculus that satisfies the codivergence condition. Then
there would be some π a -process C such that a(z)+b(z) R C. Since a(z)+b(z)cannot do any τ -action, it follows from the codivergence condition that we may
as well assume that the next action of C cannot be τ . Similarly A and B
exist such that aaRA and bbRB. Again we assume that the next action of
A (B) can only be aa (bb). Since R is closed under composition, one would
have that aa | bb | (a(z)+b(z)) R A | B | C, from which it follows that C could do
immediately an input action on a and an input action on b. But then C could
do an input action on a followed by an input action on b, which would lead toa contradiction.
Nestmann has looked at the encodings from π s -calculus to π a -calculus [47].
The adequacy of the encodings is established for some equivalences considerably
weaker than asynchronous bisimilarity. As a matter of fact there is little room
for improvement.
Proposition 29. π a @asy π − ; π i @asy π s .
Proof. Suppose A is in π a -calculus. There is no asynchronous subbisimilarity
R from π − -calculus to π a -calculus to which (ae.bf, A) belongs. This can be
92

πs
π−

πi
πa

Figure 9: Asynchronous Subbisimilarities
argued as follows: Suppose there were an asynchronous subbisimilarity R suchaebfthat (ae.bf, A) ∈ R. Now the two consecutive actions ae.bf −→ bf −→ 0 had
bfae

to be simulated by A =⇒ A1 −→ A2 =⇒ A3 −→=⇒ A0 . By the definition ofaeasynchrony, the action A1 −→ A2 can be delayed until all the internal actions
from A2 to A3 have been executed. In other words, there is an A02 such thataeA1 =⇒ A02 −→ A3 . Using the asynchronous property again, one would havebfae

A02 −→−→. This action sequence is impossible for ae.bf to simulate.
The argument for the strictness of π i vasy π s is the same.
Proposition 29 can be interpreted as saying that the asynchronous variantsof π are strictly less expressive than the synchronous counterparts from theviewpoint of interaction.
Finally we state some results that tighten up the remaining loose ends.
Proposition 30. π − 6vasy π i ; π s 6vasy π − ; π i 6vasy
π− .
↓Proof. The arguments used in the proof of Proposition 29 are good for π − 6vasy
π i . The arguments for Proposition 1 can be modified to prove π s 6vasy π − andπ i 6vasyπ− .
↓We have clarified some issues on the relative expressive power of π a -variants.
The relationships are summarized in Figure 9. In the diagram, the tailed arrowasy is vasy; and 9 indicates 6vasy . The↓ ; the plain arrow → represents v
picture of Figure 9 is not compatible with that of Figure 1. For example there
is an arrow from π s -calculus to π a -calculus in Figure 1. In Figure 9 there isdefinitely not a plain arrow from π s -calculus to π a -calculus for otherwise it
would contradict to π s 9 π − . As a matter of fact in Figure 1 there is an arrowfrom π s -calculus to π − -calculus by composing two arrows.

5.4

Internal Communication

Sangiorgi’s πI-calculus [54] is interesting in that it appears to enjoy much of
the expressiveness of π-calculus while retaining the simplicity of the semantics
of CCS. The syntax of πI-calculus is as follows:E:= 0 | X | n(x).E | n(c).E | E | E 0 | (c)E | E+E 0 | µX.E.

93

The calculus has two prefix rules and two communication rules formulated asfollows.
a(c)aca(x).E −→ E
a(c).E −→ E
ac

a(c)

a(c)

E −→ E 0 F −→ F 0
τ
E | F −→ (c)(E 0 | F 0 )ac

E −→ E 0 F −→ F 0
τ
E | F −→ (c)(E 0 | F 0 )The other rules are the same as those of π-calculus. Without further ado, let’s
see the definition of bisimulation equivalence.
Definition 19 (Sangiorgi). A symmetric relation R on the set of πI processes
is a πI-bisimulation if the following condition is met.
λb
λIf P RQ −→ Q0 then P =⇒ P 0 RQ0 for some P 0 .
The πI-bisimilarity ≈I is the largest πI-bisimulation. The structural bisimilarity∼ for πI is defined accordingly.
Let πI def be the πI-calculus with parametric definition, πI ! be the πIcalculus with replication, and πI m be the πI-calculus with mixed choice. In
the spirit of Definition 19, we may define subbisimilarities, notation vπI , andcodivergent subbisimilarities, notation vπI↓ , for πI-variants.
def
Sangiorgi showed in [54] that πI -calculus is more expressive than πI ! calculus. The interactive behaviour of the following πI def -processdef

D(x) = x(c).D(c)is different from any πI ! -process. For a counter example, the process D(c) can
engage in the following infinite sequence of actionsc(c1 )c1 (c2 )c2 (c3 )D(c) −→ −→ −→ . . .
which cannot be simulated by any πI ! -process.
Proposition 31. The following statements are valid.
def(i) (Sangiorgi) πI def 6vπI πI, πI vπI
.
↓ πI
πI
m
πI
!
πI
(ii) πI v↓ πI v↓ πI v↓ πI.
Proof. (i) The counter example given above serves as a proof. (ii) The investigations carried out in Section 2.3.2 can be redone for πI-calculus. The conclusion
is that πI-calculus, πI m -calculus and π ! -calculus are equivalent. The details
can be safely omitted.

6Effective Subbisimilarity

In Section 2.2.2 we have remarked on the relationship between Church-Turing
Thesis and the subbisimilarity approach. In present section we take anotherlook at the relationship by considering Turing completeness.
94Turing completeness is a basic criterion for the expressiveness of a process
calculus. Intuitively a process calculus is Turing complete if it is capable ofencoding all computable functions. According to Church-Turing Thesis, we
may investigate Turing completeness property using the following reductional
approach.
A process calculus is Turing complete if there is a translation froma known model of computation to the process calculus.
The above statement immediately suggests a key question. What counts as alegitimate translation from a known model of computation to a process calculus?
The answer should be straightforward once the following view is accepted.
A process calculus is Turing complete if it is a model of computation.
Since we think of a τ -action as an atomic computation step, the properties
stated in Section 2.2.2 can be repeated in the present setting.
A translation T from a model (M, →) of computation to a process
calculus L is a total relation from the set of the computing objectsof M to PL that validates at least the following statements.
1. If M TP and M → M 0 then P =⇒ P 0 T−1 M 0 for some P 0 .
τ

2. If M TP −→ P 0 then M →∗ M 0 TP 0 for some M 0 .
3. If M0 TP and M0 → M1 → . . . Mi → . . . is an infinite compuτ
tation, then P =⇒ P 0 T−1 Mk for some P 0 and some k ≥ 1.
ττ

τ

4. If M TP0 and P0 −→ P1 −→ . . . Pi −→ . . . is an infinite τ -action
sequence, then M →+ M 0 TPk for some M 0 and some k ≥ 1.
5. Effectiveness Condition: T is effective.
Due to space limitation we will refrain from giving a formulation of Turing
completeness. But the above properties will serve our purpose.
A number of Turing completeness results have been reported in literature.
These results are established with varying strength. Consult [42] for a comparison of different approaches to Turing completeness and [38] for an interpretationof Turing completeness that is very weak from the point of view of interaction.
Busi, Gabbrielli and Zavattaro’s proof can be easily modified to a total relationfrom the set of RARM’s to PCCSmdef that satisfies the above five conditions [7].
Milner has essentially demonstrated in [40] that there is a total relation fromthe set of the closed λ-terms [5] to Pπ! that satisfies the five conditions, where
the operational semantics of the λ-terms is given by that of the lazy λ-calculusof Abramsky [1]. The construction is based on an encoding that makes use of a
global pointer name e, a countable set {f, . . .} of local pointer names, a countable set {c, . . .} of resource names, a countable set {v, . . .} of name variables,
and an injective map from the countable set of the λ-variables {x, . . .} to theset of name variables. For simplicity we assume that the injective map is an95

identical function. We also assume that there is an effective bijection between{x, . . .} and {c, . . .}. The encoding is formally defined as follows:
def

=

JxKp

def

Jλx.M Kp

def

JM N Kp==

xp,
p(x).p(v).JM Kv ,(f )(JM Kf | f (c).f p.!c(v).JN Kv ).

A standard interpretation of a closed λ-term M is of the following shape:(c0 . . . cn )(O | !c0 (v0 ).JN0 Kv0 {c1 /x1 , . . . , cn /xn } | . . . | !cn (vn ).JNn Kvn )where O can be in one of the two forms:• O ≡ JF Kp {c0 /x0 , . . . , cn /xn } such that M ≡ F [x0 := N0 ] . . . [xn := Nn ];• O is the process(f0 . . . fm )(c0 )(f 0 (v).JF Kv| f 0 f 1 .!c0 (v0 ).JN 0 Kv0| f 1 (c1 ).f 1 f 2 .!c1 (v1 ).JN 1 Kv1..
.
| f m (cm ).f m p.!cm (vm ).JN m Kvm )such that M ≡ (F N 0 · · · N m )[x0 := N0 ] . . . [xn := Nn ].
τ

Now suppose JM Ke =⇒ Q. Then Q might contain some occurrences of 0 thatcan be safely omitted without affecting the semantics of Q. Using equalities(11) and(12) and the following equality
P | (a)Q =(a)(P | Q), if a 6∈ gn(P )we can design a converting algorithm A that transforms Q to a standard interpretation form and then from the standard interpretation form to the corresponding
λ-term M . Notice that a standard interpretation form contains enough information from which a λ-term can be constructed. The algorithm A reports “no”
if Q cannot be converted to a standard interpretation form. Now let A be thealgorithm that, upon receiving a program M , runs the enumeration algorithm
for the expressions of L and checks every expression if it can be converted to
M using the algorithm A. If the answer is “yes” then output the expression;otherwise check the next expression. Using this algorithm we can define T by
the following relation
L is a closed λ term;(L, P ).
and P is in the enumeration set of A(L)The proofs of Milner [40] can be summarized by saying that the total relation
T satisfies the five conditions of Turing completeness.
96

Let’s see what is missing in the statements 1-5. A computable function isa procedure that when given an input number, it outputs a number after some
calculation. The function may deliver different results in response to different
inputs. From the point of view of process theory, an input is picked up at an
input channel, whereas an output is delivered at an output channel. Now let
F be a process that encodes a computable function. It inputs a number at thechannel a and output the result number at the channel b. Let Ia be the processthat outputs a number, say i, at channel a. Then the function with the input
value i can be coded up by (a)(Ia | Fa,b ). In similar fashion one could code up
a Deterministic Turing Machine together with a value on the input tape by aprocess of the form (a)(Ia | T Ma,b ). These observations strongly suggest thata translation from a model of computation to a process calculus that proves
Turing completeness of the latter is more or less like a subbisimilarity. The
effectiveness of Church-Turing Thesis means that we might as well work withthe effective subbisimilarities. Let’s see what we can say about the effective
subbisimilarities between CCS variants.
Definition 20. A codivergent subbisimilarity R from CCS1 to CCS2 is aneffective subbisimilarity if it satisfies Effectiveness Condition. We will write
2
1
2
CCS1 vccs
e CCS if there is an effective subbisimilarity from CCS to CCS .
For Definition 20 to make sense, effective subbisimilarities must compose.
3
3
1
2
ccs
ccs
Proposition 32. If CCS1 vccs
e CCS ve CCS then CCS ve CCS .

Proof. The composition of two effective relations is effective.
In completely the same manner we can effectivise as it were the other codivergent subbisimilarities studied in this paper. The question that has to be
asked is this: Do all the positive results, obtained in the previous sections, concerning the codivergent subbisimilarities still hold? Our trust on Church-Turing
Thesis would inevitably lead us to believe that the answer is affirmative. In thepresent paper we have neither the time nor the space to pursue this issue further.
It seems necessary though to give a simple example to exhibit the effectivenessof subbisimilarity that is not codivergent.
Proposition 33. There is a subbisimilarity R from CCSm to CCSs that satisfies Effectiveness Condition.
Pn
Proof. The encoding J K from CCSm to CCSs translates i=1 λi .Pi toµZ.(λ1 .JP1 K + τ.(λ2 .JP2 K + τ.(. . . τ.(λn .JPn K + τ.Z) . . .))).
In
to the structures of λ1 .JP1 K, λ1 .JP2 K, . . . , λn .JPn K, the encoding
Padditionn
J i=1 λi .Pi K introduces a finite state loop structure. Now expand the decidable
relationdef
S = {(P, JP K) | P ∈PCCSm }
(49)

97

in the following manner: If P ≡Pn

i=1 λi .Pi then add the following pairs(P, λ1 .JP1 K + τ.(λ2 .JP2 K + . . . τ.(λn .JPn K + τ.µP ) . . .)),
(P, λ2 .JP2 K + τ.(. . . τ.(λn .JPn K + τ.µP ) . . .)),..
.
(P, λn .JPn K + τ.µP )Pn
to the relation, where µP is J i=1 λi .Pi K. The relation S + so generated satisfies
Effectiveness Condition.
The prime motivation for introducing the effective subbisimilarities is toinvestigate the idea of reduction for calculi of interaction. Such reductions both
extend and formalize the reductions among the familiar computational models.
The running theme of this paper is to use the effective subbisimilarities toclassify the expressiveness of both the interaction models and the computation
models in a single framework. For comparison of the interaction models, ourslogan is this:A model L is at least as expressive as another model L0 if and only
if there is an effective subbisimilarity from L to L0 .
For the computation models we hope to talk about a “subbisimilarity” fromone model of computation to another (Church-Turing Thesis) and a “subbisimilarity” from a model of computation to a model of interaction (Turing completeness). No matter how these formalizations turn out to be, the following
statement really should be valid.
Suppose L is Turing complete. If there is an effective subbisimilarity
from L to L0 then L0 is Turing complete.
So we have an indirect way of proving Turing completeness results.
Our second round discussion has got ourselves into a situation where we are
obliged to looking for a universal expressiveness relationship for all models ofinteraction. This is a much more challenging goal than what has been achievedin this paper. The first author is currently developing a general model theory
that addresses this issue [20].

7

Towards a Model Independent Theory

Compared to previous works [48], what is reported in this paper emphasizes
more on the unifying framework and model independent approach. We haveaimed at constructing a single platform in which we may discuss Church-Turing
Thesis, Turing completeness and relative expressiveness of process calculi. Thisis partly motivated by the belief that, since all of them are essentially about theexpressive power of computation/interaction models, they ought to be addressedby similar methodologies. The technicalities and the approaches of this paper
have been driven by the mission to search for a model-independent theory of98expressiveness. The use of the labeled semantics may have blurred the central
theme of this paper, since the reductional semantics has been advocated as an
approach that is less dependent on a particular model. While we fully agree
that a model-independent theory would be built on the notion of reduction
rather than on the interaction labels, we would not play down the significanceof the labeled approach. For a set of variants of a particular model, the labeledsemantics offers alternative yet more tractable means of study. From the pointof view of proof methodology, we could introduce the equivalence relation andthe expressive relationships on top of a reduction semantics, and then work out
the equivalent characterization in the labeled semantics. What we have done inthis paper is to use the latter semantics from the very outset, bypassing the stepfrom the reductional semantics to the equivalent labeled semantics. A positive
result of this paper can be easily transferred to a positive result in a reductionalframework. Similarly the counter examples given in this paper can be modified
to give the same separation results in terms of the reduction semantics.
The subbisimilarities studied in this paper are all between similar models.
The relative expressiveness between two quite different models is often far morechallenging. One such result is given in [19], where a fully abstract encoding of
π-calculus in Calculus of Fair Ambients is defined. This encoding gives rise to a
codivergent subbisimilarity in an appropriate sense. Another famous encoding
proves that the higher order π-calculus [61, 56] is no more expressive than the(first order) π-calculus. The syntax of the (minimal) higher order π-calculus isdefined by the following BNF:
E := X | a(X).E | a[E] | E | E 0 | (a)E.
Here a(X).E is the higher order input term and a[E] is the higher order output
term. The reason we have left out the continuation in the output term is to makethe point that this particular calculus is nothing but the interactive version of
the lazy λ-calculus [1]. The term (a)(a(X).E | a[F ]) for example is, waving hand,the λ-term (λx.E)F . Sangiorgi-Thomsen’s encoding makes use of an injective
map from the set of the process variables to Nv . The core of the encoding isgiven by the following definition:
def

Ja(X).EKst

Ja[F ]Kst=

a(x).JEKst ,def(c)(ac. | !c.JF Kst ).

=It is easy to see that the encoding gives rise to a codivergent subbisimilarity
in an appropriate sense. For yet another example, let’s see how to embed say
CCSmdef in π m -calculus. A subbisimilarity R from the former to the latter isalmost a homomorphic map except that it associates every CCSmdef prefix term
a.T to every element of the set{a(c).T 0 | F RT 0 and c is not a global name in T 0 }and the term a.T to every element of the set{a(x).T 0 | F RT 0 and x is not a free name variable in T 0 }.
99

Under this interpretation a single CCS action is simulated by an infinite number of π-actions. This is a simple example of subbisimilarity whose legitimacy
is best justified in a reductional framework. It is also an example that indicatesthe complexity of the issue. A point worth making is that for π-calculus to be
an extension of CCS, which we all believe should be the case, a line between
the names and the name variables must be drawn. A consistent understandingof the name-hood is crucial for a model-independent theory of interaction. If
the names used by two models have quite different interpretations, it raises thequestion that if it is really sensible to compare them. This remark suggests
the methodological assumption that a model-independent theory of interaction
should start with something common to all models in the sense that their semantic interpretations remain the same in all models.
After the submission of the first version of the paper, the first author has
been working on a general theory of interaction that intends to provide a uniform
treatment of both computation models and interaction models [20]. To give a
glimpse of the power of the theory, we point out that the three subbisimilarities
indicated in the previous paragraph are all particular instances of the modelindependent definition of the subbisimilarities. By applying this general theory,
one may streamline part of the process theory. The theory of name-passing calculus for example can be developed as an application of the model-independent
theory [23]. The theory of value-passing calculus can be investigated in thesame way [21]. The model-independent approach helps address the fundamental issues of interaction models. Some progress has been made along the line.
Examples include an interpretation of the full λ-calculus in π-calculus [11] andan extensional Petri Net theory that resolves the problem of compositionality [15]. It is in the light of an emerging picture of a general model-independent
theory that the significance of this work can be duly appreciated.

Acknowledgement
The first author is supported by The National 973 Project (2003CB317005)
and The National Nature Science Foundation of China (60473006 and 60573002).
Both authors would like to extend their appreciations to Xiaojuan Cai, Yuxin
Deng, Xiaoju Dong, Caodong He, Ying Jiang, Nicole Kwoh, Xinxin Liu, HuanLong, Jianxin Xue, and Han Zhu for their discussions about this paper. They
are indebted to the two anonymous referees for their detailed comments on aprevious version of the paper. Their criticisms, questions and suggestions have
led to a significant improvement of the paper.

A

Proof of Proposition 10

Suppose E is a CCSdef expression and that F, F 0 are two elements of Drv(JEK),
where JEK is the encoding defined in the proof of Proposition 10. We shall write
τ0
τ
F −→
F 0 if F −→ F 0 such that the τ -action is either caused by the explicit τ
prefix introduced by the encoding in Figure 2, or by a communication between
100the local names e> , e⊥ or h introduced by the encoding in Figure 2. In otherτ0F 0 indicates that F internally reduces to F 0 in one step. We
words, F −→τ0
τ0 ∗for the reflexive and transitive closure of −→,use the standard notation −→τ0τ0 n
and −→ for a sequence of n copies of −→’s concatenated one after another.
Technically we are using indexed labeled transition semantics. But we shall not
go into that level of details.
Using the notations introduced above, one could define a relation R by thefollowing set
)
(
τ0 ∗
ϕ
−→
T
,
for each i ∈ {1, .., n}, (eϕ )CEii.
(E1 | . . . | En , T1 | . . . | Tn )
τ0 ∗
τ0 ∗
Ti
Ti , or (h)WEϕ | Ei −→or (h)VEϕi | E −→We are about to prove that R ∼ is a subbisimilarity from CCSdef to CCSmdef .
We need to prove several technical lemmas. First observe that it is impossibleϕfor a derivative of CE
to perform a eϕ action or an h (h) action. Similarly it is
impossible for a derivative of VEϕ1 | E2 to do a e> or e⊥ action. These facts canbe stated in the form of the following lemma.
Lemma 46. The following statements are valid.
ϕϕϕ(i) (eϕ )CE∼ (h)CE∼ CE.
ϕϕ(ii) (e> )VE1 | E2 ∼ (e⊥ )VE1 | E2 ∼ VEϕ1 | E2 .
(iii) (e> )WEϕ1 | E2 ∼ (e⊥ )WEϕ1 | E2 ∼ WEϕ1 | E2 .
ϕ
Proof. The equivalences are obvious due to the following facts: In CE, VEϕ1 | E2
ϕϕ
and WEϕ1 | E2 , every occurrence of CE
0 or eϕ is restricted by (eϕ ); and in CE ,every occurrence of VEϕ1 | E2 or WEϕ1 | E2 is restricted by (h).

The next lemma is about similar properties.
τ

∗

τ

∗

τ

ϕ
0
0
0
Lemma 47. If either (eϕ )CE−→T , or (h)VEϕ1 | E2 −→T or (h)WEϕ1 | E2 −→T , then (e> )T ∼ (e⊥ )T ∼ (h)T ∼ T .

∗Proof. This is straightforward from the definition. Notice that every occurrenceϕof CE
in VEϕ1 | E2 is prefixed by h.
1 | E2ϕ
It should be clear from the definition of the encoding that once CE, orϕϕ
VE1 | E2 or WE1 | E2 departs from an internal looping, it throws away all global

occurrences of e> , e⊥ , h.
τ

∗ λ

ϕ
0
Lemma 48. Let F be either CE, or VEϕ1 | E2 or WEϕ1 | E2 . If F −→−→ F 0 forsome λ 6∈ {e> , e⊥ , h, τ0 }, then none of e> , e⊥ , h occurs as global names in F 0 .
ϕ
The above three lemmas are about what CE, VEϕ1 | E2 , WEϕ1 | E2 cannot do.
The next simple lemma is about what they can do. For the sake of stating thefollowing lemmas, we call a process inactive if it is composed of localization,
composition and 0. Clearly an inactive process is structurally bisimilar to 0.

101

An inactive context I[ ] is an inactive process with a hole. If I[ ] is an inactive
context then I[E] is structurally bisimilar to E whenever none of the global
names of E gets localized by I[ ].
Lemma 49. The following statements are valid.
eϕϕ(i) CE−→ I for some inactive process I.
hϕ(ii) VEϕ1 | E2 −→ CE.
1 | E2h(iii) WEϕ1 | E2 −→ 0.
ϕ
The definition of CE
makes sure that after it performs an eϕ action aftersome internal looping, it must turn into some process equivalent to 0. Similar
properties hold of VEϕ1 | E2 and WEϕ1 | E2 . Hence the following lemma.

Lemma 50. The following statements are valid.
τ

∗

eϕ

ϕ
ϕ
0
(i) If CE−→
F −→ then F ≡ I[CE] for some inactive context I[ ].
τ0 ∗h(ii) If VEϕ1 | E2 −→ F −→ then F ≡ I[VEϕ1 | E2 ] for some inactive context I[ ].
τ

∗

h

0
F −→ then F ≡ I[WEϕ1 | E2 ] for some inactive context I[ ].
(iii) If WEϕ1 | E2 −→ϕ, or VEϕ1 | E2 or WEϕ1 | E2 . We prove the lemma by
Proof. Let F0 be either CEτn0mutual induction on n, the length of F0 −→F . The case n = 0 is obvious.
Suppose that the lemma is true for all n < k, we show that it is true for n = k.

ϕ
• F0 ≡ C0ϕ or F0 ≡ Cλ.E
: These cases are impossible.
1
ϕϕ• F0 ≡ C(c)E
0 : In this case we continue the induction with CE 0 .
ϕ• F0 ≡ CE: Suppose the first step looping is
1 +E2
τ

ϕ
ϕ
ϕ
0
−→
(eϕ )(CECE).
| eϕ .CE
1 +E2
1 +E2
1
τ

∗ eϕ

ϕ
ϕ
ϕ
0
Since CE−→∼ (eϕ )CEby Lemma 46, it must be the case that CE
6−→,
1
1
1
ϕ
meaning that it is impossible for CE
to
do
a
e
actionafter
someinternal
ϕ
1
τ

n0

eϕ

ϕ
0
looping. So it has to be that CE−→
G −→ for some G and some n1
1
ϕless than k. By induction G ≡ I1 [CE]for some inactive context I1 [ ].
1Consequently

F0

τ

0
−→

(n0 +1)
τ

0
−→

τ

0
−→

(k−n0 −2)ϕϕ
] | eϕ .CE)(eϕ )(I1 [CE
1
1 +E2
ϕ
(eϕ )(I1 [R] | CE
)
1 +E2

F

for some inactive process R. It is obvious that F ≡ (eϕ )(I1 [R] | F 0 )τ(k−n0 −2)eϕϕ
0
for some F 0 such that CE−→
F 0 −→. By induction hy1 +E2
ϕ0pothesis, F ≡ I2 [CE1 +E2 ] for some inactive context I2 [ ]. ConsequentlyϕF ≡ (eϕ )(I1 [R] | I2 [CE
]).
1 +E2

102

τ

ϕ
ϕ
ϕ
0
−→
(eϕ )(CEIf CE| eϕ .CE) is the first internal looping step, the
1 +E2
2
1 +E2
argument is the same.
ϕ• F0 ≡ CE: The first internal looping step must be
1 | E2τϕ0−→(h)(VEϕ1 | E2 | WEϕ1 | E2 ).
CE
1 | E2

By Lemma 46, neither VEϕ1 | E2 nor WEϕ1 | E2 can ever do a eϕ action. No
matter how VEϕ1 | E2 and WEϕ1 | E2 loop, they must synchronize at h at somepoint before reaching F . In other words,
τ

n1

τ

n2

0
VEϕ1 | E2 −→

h

G1 −→

and
0
WEϕ1 | E2 −→

h

G2 −→

for some G1 , G2 and some n1 , n2 less than k. By induction G1 ≡ I1 [VEϕ1 | E2 ]and G2 ≡ I2 [WEϕ1 | E2 ] for some inactive contexts I1 [ ], I2 [ ]. Consequently
τ

ϕ
0
CE
−→
1 | E2n1 +n2 +2

ϕ] | I2 [0]).
(h)(I1 [CE
1 | E2

As in the previous case, we can now proceed by applying the induction
hypothesis to the rest of the internal looping.
• F0 ≡ VEϕ1 | E2 or F0 ≡ WEϕ1 | E2 : The proof is similar.
We are done.
ϕAnother important property of CE
is that whatever internal looping it has
ϕengaged, it retains the possibility to go back to CE. Similar property holds ofϕϕ
VE1 | E2 and WE1 | E2 .
τ

∗

ϕ
0
F thenLemma 51. Let F0 be either CE, or VEϕ1 | E2 or WEϕ1 | E2 . If F0 −→
τ

∗

0
F −→
A ∼ F0 for some A.

Proof. We prove the lemma by induction on n, the length of the internal looping
τ0 n
F0 −→
F . The case of n = 0 is trivial. Suppose the lemma is true for all n < k,we show that it is true for n = k as well.
ϕ• F0 ≡ C0ϕ or F0 ≡ Cλ.E
: In this case there is nothing to prove.
ϕϕ• F0 ≡ C(c)E: In this case we continue with CE.
1
1
ϕ• F0 ≡ CE: Suppose the first internal looping step is
1 +E2
τ

ϕ
ϕ
ϕ
0
| eϕ .CE).
CE−→(eϕ )(CE
1 +E2
1
1 +E2

There are two subcases.
103

τ

j eϕ

ϕ
0
– If CE−→−→ G for some G ∼ 0 and some j < k, then
1
τ

0
F0 −→

j+2

τ

ϕ
0
(eϕ )(G | CE
) −→
1 +E2
τ

ϕ
0
−→
for some F 0 such that CE
1 +E2

n−j−2

n−j−2

(eϕ )(G | F 0 ) ≡ F

F 0 . By induction hypothesis,

τ0 ∗

τ

∗

ϕ
0
(eϕ )(G | A0 ) ∼ F0 .
for some A0 . Thus F −→F 0 −→ A0 ∼ CE
1 +E2
τ

ϕ
0
– If CE
−→
1

n−1

ϕ
H for some H such that (eϕ )(H | eϕ .CE) ≡ F,
1 +E2
∗

τ

ϕ
0
A0 ∼ CEfor some A0 . By Lemma 49,
then by induction H 0 −→1eϕsome A00 exists such that A0 −→ A00 ∼ 0. But then
τ

∗

τ

ϕ
ϕ
0
0
(eϕ )(A00 | CE(eϕ )(A0 | eϕ .CE) −→) ∼ F0 .
F −→
1 +E2
1 +E2
τ

ϕ
ϕ
0
• F0 ≡ CE: Obviously CE−→(h)(VEϕ1 | E2 | WEϕ1 | E2 ). Suppose
1 | E2
1 | E2
τ

0
VEϕ1 | E2 −→

n1

τ0 n

τ

0
G and WEϕ1 | E2 −→n2

H are maximal internal looping in

F0 −→ F . There are two subcases.
τ∗0– n1 + n2 = n − 1. By induction hypothesis, G −→A0 ∼ VEϕ1 | E2 and

τ

∗

0
H −→
B 0 ∼ WEϕ1 | E2 for some A0 , B 0 . It follows from Lemma 49hhϕthat A0 −→ A00 ∼ CE
and B 0 −→ B 00 ∼ 0 for some A00 , B 00 .
1 | E2
Consequently
τ

∗

τ

ϕ
0
0
F −→
(h)(A0 | B 0 ) −→(h)(A00 | B 00 ) ∼ CE.
1 | E2– n1 + n2 < n − 1. The next internal looping is an interaction between
G and H at u. By Lemma 50, there are inactive contexts I1 [ ], I1 [ ]such thatG≡ I1 [VEϕ1 | E2 ],H≡ I2 [WEϕ1 | E2 ].

It follows thatϕCE
1 | E2τ0−→(h)(VEϕ1 | E2 | WEϕ1 | E2 )τ∗(h)(I1 [VEϕ1 | E2 ] | I2 [WEϕ1 | E2 ])τ∗ϕ(h)(I1 [CE] | I2 [0]).
1 | E2

0
−→
0
−→

τ

ϕ
0
Clearly F ≡ (h)(I1 [F 0 ] | I2 [0]) and CE−→
1 | E2
τ0 ∗n0

F 0 for some n0 < n.

ϕ
By induction hypothesis, F 0 −→ A0 ∼ CE
for some A0 . So
1 | E2
τ

∗

ϕ
0
F −→
(h)(I1 [A0 ] | I2 [0]) ∼ CE.
1 | E2104

• F0 ≡ VEϕ1 | E2 or F0 ≡ WEϕ1 | E2 : The proof is similar.
We are done.
The next lemma shows that the encoding defined in Figure 2 is faithful withrespect to the operational semantics.
λLemma 52. The following statements are valid whenever E −→ E 0 .
ϕ τ0 ∗ λ−→ −→ T 0 for some T 0 such that E 0 R ∼ T 0 .
(i) CE∗ λτ0(ii) VEϕ| F −→−→ T 0 for some T 0 such that E 0 R ∼ T 0 .

τ

∗ λ

0
(iii) WEϕ | F −→−→ T 0 for some T 0 such that E 0 R ∼ T 0 .

Proof. The following is a mutual induction on the height of the inference tree
λof E −→ E 0 :
λ

λ

ϕ
ϕ
ϕ
• λ.E −→ E: Then Cλ.E−→ (eϕ )CE. It is obvious that ER(eϕ )CE
.
λ

τ

λ

∗ λ

ϕ
0
• E −→ E 0 ⇒ (c)E −→ (c)E 0 : By induction we have CE−→−→ T 00 and
τ

∗ λ

ϕ
ϕ
ϕ
0
E 0 R ∼ T 00 for some T 00 . Since C(c)E≡ (c)CE, we must have C(c)E
−→
−→
00
0
00
(c)T . It is easy to see that (c)E R ∼ (c)T .
λ

τ

λ

∗ λ

ϕ
0
−→
−→ T10 and• E1 −→ E10 ⇒ E1 + E2 −→ E10 : By induction we have CE
1
τ

∗ λ

ϕ
ϕ
0
−→
−→ (eϕ )(T10 | eϕ .CE
E10 R ∼ T10 for some T10 . But then CE
)∼
1 +E2
1 +E2
0
T1 by Lemma 48.
λ

τ

λ

∗ λ

ϕ
0
−→
−→
• E1 −→ E10 ⇒ E1 | E2 −→ E10 | E2 : By induction we have that CE
1
0
0
0
0
T1 and E1 R ∼ T1 for some T1 . It follows from Lemma 48 that
τ

∗ λ

0
−→ (eϕ )(T10 | eϕ .VEϕ1 | E2 ) ∼ T10 .
VEϕ1 | E2 −→

τ

τ

∗ λ

ϕ
0
0
So CE
−→
(h)(VEϕ1 | E2 | WEϕ1 | E2 ) −→−→∼ (h)(T10 | WEϕ1 | E2 ) ∼1 | E2
ϕT10 | (h)WE1 | E2 by Lemma 48. It is clear that E10 | E2 R ∼ T10 | (h)WEϕ1 | E2 .
aaτ• E1 −→ E10 ∧ E2 −→ E20 ⇒ E1 | E2 −→ E10 | E20 : By induction we have
τ0 ∗ aτ0 ∗ aVEϕ1 | E2 −→−→ T10 and E10 R ∼ T10 for some T10 , and WEϕ1 | E2 −→−→ T20and E20 R ∼ T20 for some T20 . Consequently
τ

τ

∗ τ

ϕ
0
0
CE
−→
(h)(VEϕ1 | E2 | WEϕ1 | E2 ) −→−→ (h)(T10 | T20 ) ∼ T10 | T20
1 | E2by Lemma 48. Obviously E10 | E20 R ∼ T10 | T20 .
τ

∗ λ

0
• VEϕ| F −→−→ T 0 : By Lemma 50, some inactive context I[ ] and some0
process T1 exist such thatτ

VEϕ| F

0
−→

τ

∗

ϕ
I[(eϕ )(CE| eϕ .VEϕ| F )]

∗ λ

0
−→
−→ I[(eϕ )(T10 | eϕ .VEϕ| F )] ≡ T 0

105

∗ λ

τ

ϕ
0
−→
−→ T10 . By induction, E 0 R ∼ T10 ∼ T 0 .
and CEτ∗ λ

0−→ T 0 : The proof is similar.
• WFϕ | E −→This completes the induction.
Actually the encoding defined in Figure 2 is more than faithful. It reflects
the operational semantics in the sense of the following lemma.
Lemma 53. The following statements are valid if λ 6∈ {eϕ , u, u, τ0 }.
τ

∗

λ

λ

ϕ
0
−→
T −→ T 0 , then E −→ E 0 and E 0 R ∼ T 0 for some E 0 .
(i) If CE
τ0 ∗

λ

λ

(ii) If VEϕ1 | E2 −→ T −→ T 0 , then E1 −→ E 0 and E 0 R ∼ T 0 for some E 0 .
∗

τ

λ

λ

0
T −→ T 0 , then E2 −→ E 0 and E 0 R ∼ T 0 for some E 0 .
(iii) If WEϕ1 | E2 −→ϕ
Proof. Let F0 be either CE, or VEϕ1 | E2 or WEϕ1 | E2 . We prove the lemma byτ∗0
induction on n, the length of F0 −→T . When n = 0, the only possibility is
λ
λ
ϕ
ϕ
ϕ
ϕ
F0 ≡ Cλ.E . In this case Cλ.E −→ (eϕ )CE. Clearly λ.E −→ E and E R (eϕ )CEby the definition of R. Suppose that the lemma is true for n < k, we prove that
it is also true for n = k. We carry out an induction as follows:ϕϕ• F0 ≡ C(c)E: In this case we continue the structural induction on CE.
1
1
ϕ• F0 ≡ CE: Assume that the first internal looping step is
1 +E2
τ

ϕ
ϕ
ϕ
0
CE
−→
(eϕ )(CE).
| eϕ .CE
1 +E2
1 +E2
1

There are two possibilities:
τ

ϕ
0
– CE
−→
1

n−1

λ

T1 −→ T10 . By induction hypothesis, there exists someλλE10 such that E1 −→ E10 and E10 R ∼ T10 . Hence E1 +E2 −→ E10 R ∼ϕ) by Lemma 48.
T 0 ≡ (eϕ )(T10 | eϕ .CE
1 +E2
τ

ϕ
0
– CE
−→
1

n1

eϕ

T1 −→ T10 for some n1 less than k. By Lemma 50, T10
τ

n2

λ

ϕ
0
is an inactive process. It follows that CE−→
T2 −→ T20
1 +E2
0
for some T2 , T2 and some n2 less than k. By induction hypothesis,
λE1 +E2 −→ E10 R ∼ T20 ≡ (eϕ )(T10 | T20 ).
ϕ• F0 ≡ CE: The first internal looping step is
1 | E2τϕ0CE−→(h)(VEϕ1 | E2 | WEϕ1 | E2 ).
1 | E2

There are several subcases.
τ

n−1

λ

λ

0
– VEϕ1 | E2 −→T1 −→ T10 . By induction hypothesis, E1 −→ E10 R ∼T10 for some E10 . It follows that

λE1 | E2 −→ E10 | E2 R ∼ T10 | (h)WEϕ1 | E2 ∼ (h)(T10 | WEϕ1 | E2 ).
106

τ

0
– WEϕ1 | E2 −→n−1

λT2 −→ T20 . This is symmetric to the previous case.
τ0– λ = τ , and the tau action is caused by VEϕ1 | E2 −→τ

0and WEϕ1 | E2 −→hypothesis,

n2

n1

a

T1 −→ T10a

T2 −→ T20 with n1 + n2 = n − 1. By inductionaE1 −→ E10 R ∼ T10
anda

E2 −→ E20 R ∼ T20 .
τHence E1 | E2 −→ E10 | E20 R ∼ T10 | T20 ∼ (h)(T10 | T20 ).
τ

n1

τ

h

n2

h

0
0
T2 −→ T20 with n1 +n2 <T1 −→ T10 and WEϕ1 | E2 −→– VEϕ1 | E2 −→ϕ
00
k. By Lemma 50, T1 ≡ I1 [CE1 | E2 ] and T2 ≡ I2 [0] for some inactive

τ

∗

ϕ
ϕ
0
contexts I1 [ ], I2 [ ]. Therefore CE−→(h)(I1 [CE] | I2 [0]).
1 | E2
1 | E2
So we may continue with the induction.

• F0 ≡ VEϕ1 | E2 . The first internal looping step must beτϕ
0| eϕ .VEϕ1 |E2 ).
VEϕ1 | E2 −→(eϕ )(CE1

There are two subcase:
τ

n−1

τ

n2

ϕ
0
−→
– CE
1

λ

T1 −→ T10 . In this case we resort to induction hypothesis.
eϕ

ϕ
0
−→
T2 −→ T20 for some n2 less than k. By Lemma 50, T20 is– CE
1
an inactive process. Thereforeτ

VEϕ1 | E2

0
−→

τ

0
−→

n2 +2

n−n2 −2(eϕ )(T20 | VEϕ1 |E2 )(eϕ )(T20 | T200 )τ

0for some T200 . Therefore we may proceed with VEϕ1 |E2 −→n−n2 −2

T200 .

• F0 ≡ WEϕ1 | E2 . This case is symmetric to the previous one.
We are done.
The faithful and reflection properties allow us to prove the claim we madein the beginning of the section.
Proposition 34. R ∼ is a subbisimilarity.
Proof. Assume E1 | E2 | · · · | Ek R T1 | T2 | · · · | Tk ∼ T .
λ• Suppose E1 | E2 | · · · | Ek −→ E 0 for some E 0 . Without loss of generality
there are basically two cases: either
λE1 | E2 | · · · | Ek −→ E10 | E2 | ... | Ek107

λis caused by E1 −→ E10 , or
τE1 | E2 | · · · | Ek −→ E10 | E20 | ... | Ek
is caused by an interaction between E1 and E2 . Consider the first case.
τ0 ∗ϕWe have by definition that F1 −→T1 , where F1 is either (eϕ )CE
, or
1
τ

∗

0
∼ F1 . By(h)VEϕ1 | E or (h)WEϕ | E1 for some E. By Lemma 51, T1 −→

τ

∗ λ

0
Lemma 52, we have that F1 −→−→ T10 and E10 R ∼ T10 for some T10 . Thus

λT =⇒−→ T 0 for some T 0 such that
E10 | E2 | · · · | Ek R ∼ T10 | T2 | · · · | Tk ∼ T 0 .
aa

For the second case, suppose E1 −→ E10 and E2 −→ E20 . By Lemma 51
and Lemma 52, there exist some T10 , T20 and some l1 , l2 ≥ 0 such that
τ

∗

τ

∗ a

τ

∗

τ

∗ a

0
0
T1 −→
∼ F1 −→−→ T10 ∼ R−1 E10

and

0
0
T2 −→
∼ F2 −→−→ T20 ∼ R−1 E20

ϕwhere Fi , for i ∈ {1, 2}, is either (eϕ )CE, or (h)VEϕi | E or (h)WEϕ | Ei . Itiτshould be then clear that T =⇒∼ T10 | T20 | ... | Tk ∼ R−1 E10 | E20 | ... | Ek .
λ• If T −→ T 0 then by the definition of structural bisimilarity, we have
without loss of generality that either
λT1 | T2 | · · · | Tk −→ T10 | T2 | · · · | Tk ∼ T 0
λis caused by T1 −→ T10 , or
τ

T1 | T2 | · · · | Tk −→ T10 | T20 | · · · | Tk ∼ T 0aa

is caused by T1 −→ T10 and T2 −→ T20 , orτ0T1 | T2 | · · · | Tk −→T10 | T2 | · · · | Tk ∼ T 0τ0
is caused by T1 −→T10 . For the first case we have by definition that

τ0 ∗

λ

ϕ
F1 −→ T1 −→ T10 where F1 is either (eϕ )CE, or (h)VEϕ1 | E or (h)WEϕ | E1
1
for some E. According to Lemma 53, there exists some E10 such thatλE1 −→ E10 R ∼ T10 . Thus E10 | E2 | · · · | Ek R ∼ T10 | T2 | · · · | Tk ∼ T 0 . For
τ0 ∗
τ0 ∗
a
a
the second case, we have F1 −→T1 −→ T10 and F2 −→T2 −→ T20aafor some T10 , T20 . By Lemma 53, we have E1 −→ E10 R ∼ T10 and E2 −→E20 R ∼ T20 for some E10 , E20 . Thus
τ

E1 | E2 | · · · | Ek −→ E10 | E20 | · · · | Ek R ∼ T10 | T20 | · · · | Tk ∼ T 0 .
For the third case, it suffices to notice that
E1 | E2 | · · · | Ek R T10 | T2 | · · · | Tk .
This completes the proof.
108

References[1] S. Abramsky. The Lazy Lambda Calculus. D. Turner (eds.): Declarative
Programming, 65-116, Addison-Wesley, 1988.
[2] M. Alsuwaiyel. Algorithm Design Techniques and Analysis. World Scientific, 1999.
[3] R. Amadio, I. Castellani and D. Sangiorgi. On Bisimulations for the Asynchronous π-calculus. U. Montanari, V. Sassone (eds.): CONCUR 1996 ,Lecture Notes in Computer Science 1119: 147-162, 1996.
[4] J. Baeten and W. Weijland. Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, CUP, 1990.
[5] H. Barendregt. The Lambda Calculus: Its Syntax and Semantics, Studies
in Logic and Foundations of Mathematics, North-Holland, 1984.
[6] G. Boudol. Asynchrony and the π-calculus. Technical Report RR-1702,
INRIA Sophia-Antipolis, 1992.
[7] N. Busi, M. Gabbrielli and G. Zavattaro. Replication vs Recursive Definitions in Channel Based Calculi. ICALP 2003 , Lecture Notes in Computer
Science 2719: 133-144, 2003.
[8] N. Busi, M. Gabbrielli and G. Zavattaro. Comparing Recursion, Replication
and Iteration in Process Calculi. ICALP 2004 , Lecture Notes in Computer
Science 3142: 307-319, 2004.
[9] N. Busi and G. Zavattaro. On the Expressive Power of Movement andRestriction in Pure Mobile Ambients. Theoretical Computer Science, 322:
477-515, 2004.
[10] D. Cacciagrano, F. Corradini, J. Aranda and F. Valencia. Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus. ENTCS
194: 59-84, 2008.
[11] X. Cai and Y. Fu. The λ-Calculus in the π-Calculus, 2009. The paper isdownloadable at http://basics.sjtu.edu.cn/~ yuxi/papers.
[12] L. Cardelli and A. Gordon. Mobile Ambients. Theoretical Computer Science, 240: 177-213, 2000.
[13] B. Davey and H. Priestley. Introduction to Lattices and Order . Cambridge
University Press, 1990.
[14] R. De Nicola, M. Hennessy. Testing Equivalence for Processes. TheoreticalComputer Science, 34: 83-133, 1984.
[15] X. Dong and Y. Fu. Extensional Net Theory. 2009.

109

[16] P. van Emde Boas. Machine Models and Simulaitons. In Handbook of Theoretical Computer Science: Algorithm and Complexity, volume A, ed. by J.
van Leeuwen, Elservier, 1990.
[17] A. Finkel and Ph. Schnoebelen. Well-Structured Transition System Everywhere. Theoretical Computer Science, 256: 63-92, 2001.
[18] Y. Fu. On Quasi Open Bisimulation. Theoretical Computer Science, 338:
96-126, 2005.
[19] Y. Fu. Fair Ambients. Acta Informatica, 43: 535-594, 2007.
[20] Y. Fu. Theory of Interaction. Working paper, 2009.
[21] Y. Fu. Theory of Value Passing Calculus. Working paper, 2009.
[22] Y. Fu and Z. Yang, Tau Laws for Pi Calculus, Theoretical Computer Science, 308: 55-130, 2003.
[23] Y. Fu, H. Zhu. Theory of Name Passing Calculus. Working paper, 2009.
[24] J. Girard, Linear Logic, Theoretical Computer Science, 50: 1-102, 1987.
[25] R. van Galbbeek. Linear Time – Branching Time Spectrum II. CONCUR’93, Lecture Notes in Computer Science 715: 66-81, 1993.
[26] R. van Glabbeek and W. Weijland. Branching Time and Abstraction in
Bisimulation Semantics. Information Processing’89, North-Holland, 613618, 1989.
[27] P. Giambiagi, G. Schneider and F. Valencia. On the Expressiveness of Infinite Behavior and Name Scoping in Process Calculi. FOSSACS 2004 ,Lecture Notes in Computer Science 2987: 226-240, 2004.
[28] D. Gorla. Towards a Unified Approach to Encodability and Separation
Results for Process Calculi. CONCUR 2008 , Lecture Notes in Computer
Science 5201, 492-507, 2008.
[29] D. Gorla. Comparing Communication Primitives via their Relative Expressive Power, Information and Computation 206: 931-952, 2008.
[30] D. Gorla. On the Relative Power of Ambient-based Calculi. TGC’08, Lecture Notes in Computer Science 5474: 141-156, 2009.
[31] D. Gorla. On the Relative Power of Calculi for Mobility. 25th International Conference on Mathematical Foundation of Programming Semantics,
ENTCS, Elsevier, 2009.
[32] M. Hennessy. An Algebraic Theory of Processes. MIT Press, Cambridge,
MA, 1988.

110[33] M. Hennessy, H. Lin, Symbolic Bisimulations. Theoretical Computer Science, 138: 137-161, 1995.
[34] K. Honda and M. Tokoro. An Object Calculus for Asynchronous Communications. M. Tokoro, O. Nierstrasz, P. Wegner and A. Yonezawa (eds.),
ECOOP 1991, Geneva, Switzerland, Lecture Notes in Computer Science
512: 133-147, 1991.
[35] J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages
and Computation, Addison-Wesley Publishing Company, 1979.
[36] A. Ingolfsdottir and H. Lin. A Symbolic Approach to Value-passing Processes, Chapter 7 of Handbook of Processes Algebra, Elsevier, 2001.
[37] J. Kruskal. The Theory of Well Ordering: A Frequently Discovered Concept, Journal of Combinatorial Theory, Series A, 13: 297-305, 1972.
[38] I. Lanese, J. Perez, D. Sangiorgi and A. Schmitt. On the Expressivenessand Decidability of Higher-Order Process Calculi. LICS’08 , 145-155, 2008.
[39] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[40] R. Milner. Functions as Processes. Mathematical Structures in Computer
Science, 2: 119-146, 1992.
[41] R. Milner. Elements of Interaction. Communication of the ACM: 7889,1993.
[42] S. Maffeis and I. Phillips. On the Computational Strength of Pure Ambient
Calculi. Theoretical Computer Science, 330: 501-551, 2005.
[43] R. Milner, J. Parrow and D. Walker. A Calculus of Mobile Processes. Information and Computation, 100: 1-40 (Part I), 41-77 (Part II), Academic
Press, 1992.
[44] R. Milner, The Polyadic π-Calculus: a Tutorial, Proceedings of the 1991
Marktoberdorf Summer School on Logic and Algebra of Specification, NATO
ASI, Series F, Springer-Verlag, 1993.
[45] R. Milner and D. Sangiorgi, Barbed Bisimulation, ICALP 1992, Lecture
Notes in Computer Science 623, 685-695, 1992.
[46] U. Nestmann and B. Pierce. Decoding Choice Encodings. In: U. Montanari,
V. Sassone (eds.): CONCUR 1996 , Lecture Notes in Computer Science
1119: 179-194, 1996.
[47] U. Nestmann. What is a Good Encoding of Guarded Choices? Informationand computation, 156: 287-319, 2000.
[48] U. Nestmann. Welcome to the Jungle: A Subjective Guide to Mobile Process Calculi, In: C. Baier and H. Hermanns (eds.): CONCUR 2006 , Lecture
Notes in Computer Science 4137: 52-63, 2006.
111

[49] C. Palamidessi. Comparing the Expressive Power of the Synchronous andthe Asynchronous π-calculus. Mathematical Structures in Computer Science, 13: 685-719, 2003.
[50] D. Park. Concurrency and Automata on Infinite Sequences. Proceedings of
the 5th GI-Conference on Theoretical Computer Science, Lecture Notes in
Computer Science 104: 167-183, Springer, 1981.
[51] I. Phillips and M. Vigliotti. Leader Election in Rings of Ambient Processes,
Theoretical Computer Science, 356: 468-494, 2006.
[52] L. Priese. On the Concept of Simulation in Asynchronous, Concurrent
Systems. Progress in Cybernatics and Systems Research, vol.VII, 85-92,
Hemisohere, Dubl. Corp., 1978.
[53] C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS
2006, 59-68, 2006.
[54] D. Sangiorgi. π-calculus, Internal Mobility and Agent-Passing Calculi. Theoretical Computer Science, 167: 235-274, 1996.
[55] D. Sangiorgi, A Theory of Bisimulation for π-Calculus, Acta Informatica,
3: 69-97, 1996.
[56] D. Sangiorgi. Bisimulation for Higher Order Process Calculi. Information
and Comptation, 131: 141-178, 1996.
[57] D. Sangiorgi. On the Origin of Bisimulation and Coinduction. ACM Transactions on Programming Languages and Systems, 31, 2009.
[58] M. Sipser. Introduction to Theory of Computation. PWS Publishing Company, 1997.
[59] D. Sangiorgi and D. Walker. On Barbed Equivalence in π-Calculus, In: K.
Larsen and M. Nielsen (eds.): CONCUR 2001 , Lecture Notes in Computer
Science 2154: 292-304, 2001.
[60] D. Sangiorgi and D. Walker. The Pi Calculus–A Theory of Mobile Processes, CUP, 2001.
[61] B. Thomsen. A Theory of Higher Order Communicating Systems. Information and Computation, 116: 38-57, 1995.
[62] M. Vigliotti, I. Phillips and C. Palamidessi. Tutorial on Separation Resultsin Process Calculi via Leader Election. Theoretical Computer Science, 388:
267-289, 2007.
[63] D. Walker. Bisimulation and Divergence. Information and Computation,
85: 202-241, 1990.
[64] I. Wegener. Complexity Theory, Spronger-Verlag, 2005.

112