Acta Informatica (2007) 43:535–594
DOI 10.1007/s00236-007-0038-z
O R I G I NA L A RT I C L E

Fair ambients
Yuxi Fu

Received: 9 May 2006 / Accepted: 10 January 2007 /Published online: 28 February 2007
© Springer-Verlag 2007

Abstract Based on an analysis of the capability operators of the Calculus of Mobile
Ambients, three fairness principles are proposed to safeguard the interactions of theambients. The Calculus of Fair Ambient is designed to meet these fairness principles.
A labeled transition semantics for the calculus is defined to support structural investigation. The bisimulation theory of the fair ambients is studied and two coincidence
results are established. An expressiveness result of the calculus is formally establishedby proving that it contains the pi calculus as a sub-calculus.

1 Capability, anonymity and mobility
The Calculus of Mobile Ambients, MA for short, was introduced and studied in [8–11]
by Cardelli and Gordon as a language that formalizes the mobility of computing [6].
The central notion of the calculus is that of ambient, a piece of program residing in a
specified location. The introduction of the ambients captures several features in distributed/mobile computing. The first is that computations are scattered over spatiallydistributed locations. The second is that computations happen in a parallel fashion in
the sense that each program at a location can be executed on its own. The third is thatcomputations are mobile, meaning that a piece of program might migrate from one
place to another and that programs can be executed in transit. In MA the syntax for
an ambient is as follows:a[P]where a is the ambient name indicating the location, and P is the ambient body specifying the computation. To define mobility the Calculus of Mobile Ambients must be
equipped with operators that define how a piece of program migrates from a source

Y. Fu (B)BASICS, Department of Computer Science,
Shanghai Jiaotong University, Shanghai 200030, Chinae-mail: fu-yx@cs.sjtu.edu.cn

536

Y. Fu

ambient to a target ambient. So computations look like this:τa[P] | b[Q] −→ a[P ] | b[M | Q ]Here the idea is that the program M has moved from the ambient a to the ambient b.
It is clear that the above interaction is between two ambients. The authors of MA havemade an important design decision that the above transportation is broken down to
two more primitive actions:ττ

a[P] | b[Q] −→ a[P ] | M | b[Q] −→ a[P ] | b[M | Q ]Here the ambient a[P] emits to the environment the process M , and then M enters
the ambient b[Q]. In these two step actions M , the program in transit, can be observed
by other ambients in the environment. If one thinks of the ambients as first class citizens, it is natural that an observable migrating program, like the M above, should be
an ambient. This requirement is also conducive to the idea that a moving object must
be somehow protected. The updated view on the decomposition is then as follows:ττ

a[P] | b[Q] −→ a[P ] | c[M ] | b[Q] −→ a[P ] | b[c[M] | Q ]In terms of the ambient operators, this means that there should be at least two combinators, one induces an exit operation and the other an entrance operation. For that
purpose Cardelli and Gordon introduced two action primitives in and out, the capabilities. In what follows we take a detailed look at the two primitives.
1.1 Capability
Using the in and out primitives, Cardelli and Gordon defined the semantics of MA by
the following reductions:τb[in a.Q | N] | a[P] −→ a[b[Q | N] | P]
τa[b[out a.Q | N] | P] −→ b[Q | N] | a[P]

(1)
(2)

There are two observations concerning (1) and (2). One is that the entrance operations
are symmetric to the exit operations. Notice that both an entrance and an exit haveeffect on the ambient and the environment. In (1) the ambient b[in a.Q | N] is part ofthe environment that is consumed by the ambient a[P], whereas in (2) the ambienta[b[out a.Q | N] | P] releases b[Q | N] onto the environment. The transportation of theambient in (1) and that in (2) goes in the opposite directions. The second observationis that the movement of an ambient is activated by itself. This is called Subjective
Movement in [11]. In (1) the ambient b[in a.Q | N] injects itself into a[P]. The action
is caused from within b[in a.Q | N]. The target ambient can only accept. In (2) the
ambient b[out a.Q | N] escapes from an ambient at a. The action is triggered by theformer, the latter can only let go, and the environment can only accept.
There is an obvious reciprocal to Subjective Movement: The movement of an ambient is activated by the environment (Objective Movement). By Objective Movement,
one could define the operational semantics as follows:τb[Q] | a[in b.P | L] −→ a[b[Q] | P | L]
τ

a[b[Q] | out b.P | L] −→ b[Q] | a[P | L]

(3)
(4)

Fair ambients537

In (3) the ambient a[in b.P | L] imports an ambient named b, whereas in (4) the
ambient a[b[Q] | out b.P | L] exports an ambient named b. In both occasions the ambient b[Q] acts passively. The movement is triggered from outside b[Q]. The Ambient
Calculus with the operational semantics defined by (3) and (4) is essentially the PAC
studied by Phillips and Vigliotti in [31]. In PAC the operators in and out are denoted
respectively by pull and push.
Subjective Movement, and its duality, is subject to debates. In literature some discussions on MA have focused on the lack of controlling power over interactions. In (1)the entrance is made without any permission from the target ambient a[P]. In (2) the
release is granted with no regards to the environment. Variants of MA have been proposed to increase the controls over interactions. Let’s take a look at some measuresthat have been put forth. All of them exercise some degree of access control.
–

One way is to limit the number of entrances to an ambient as well as the numberof release from an ambient. This is achieved by adding the capabilities in and out
and define the operational semantics as follows:τb[in a.Q | N] | a[in.P | L] −→ a[b[Q | N] | P | L]

(5)

and
τ

a[b[out a.Q | N] | out.P | L] −→ b[Q | N] | a[P | L]

(6)

In (5) the entrance of b[Q | N] into a is permitted since a[in.P | L] has more roomto accept ambients. Similarly the prefix out says that a[b[out a.Q | N] | out.P | L]
has the potential to release ambients. So an ambient a[P] may specify the numberof entrance and exit it allows. This variant is basically Levi and Sangiorgi’s Calculus of Safe Ambients (SA) studied in [20]. In Levi and Sangiorgi’s notations, thenew primitives take the forms in a.P and out a.P respectively. But the following
operational semantics points out that the difference is largely syntactical.
τb[in a.Q | N] | a[in a.P | L] −→ a[b[Q | N] | P | L]

(7)

and
τ

a[b[out a.Q | N] | out a.P | L] −→ b[Q | N] | a[P | L]

(8)

In the notations of Levi and Sangiorgi, the programs b[out a.P | c[out b.Q]] andb[in a.P], for a  = b, could be regarded as containing design errors.
The control on the number of times an ambient’s boundary may be crossed canalso be exerted dually:τb[in.Q | N] | a[in b.P | L] −→ a[b[Q | N] | P | L]

(9)

and
τ

a[b[out.Q | N] | out b.P | L] −→ b[Q | N] | a[P | L]

(10)

The computation defined in (9) makes good sense from a resource sensitive viewpoint. Consider the ambient !a[in.L]. If we think of a[L] as a resource that mostambients depend on, then !a[in.L] provides a way for ambients with different
names to import the resource a[L]. We will denote by SAd the Ambient Calculus
with the operational semantics defined by (9) and (10).

538

–

Y. Fu

We mention that MA can be seen as a sub-calculus of SA. A structural translation from MA to SA interprets a[P] as a[P | !in | !out]. Similarly PAC can be seen
as a sub-calculus of SAd by translating a[P] to a[P | !in | !out].
Another way to control the access to ambients is to combine the mechanisms of
Subjective Movement and Objective Movement. Now the two parties involved in
an interaction must both warrant the interaction as in the following semantics:
τb[in a.Q | N] | a[in b.P | L] −→ a[b[Q | N] | P | L]

(11)

and
τ

a[b[out a.Q | N] | out b.P | L] −→ b[Q | N] | a[P | L]

–

(12)

In (11) the ambient b[in a.Q] is capable of entering the ambient a, the latter iswilling to give its permission. So the interaction happens. In (12) the ambientb[out a.Q] wants to get out of a, and a lets go. The release then happens. This is
the ROAM, the Calculus of Robust Ambients, of Guan [18].
From the point of view of symmetry of interaction the access controls definedin (11) and (12) do not match. In (11) the environment b[in a.N | Q] enters a after
it obtains a permission from a. But in (12) the ambient b[out a.N | Q] tries to get
out of a must get a permission from within a. The environment still has no say
over the event. In [22] Merro and Hennessy propose the following operational
rule for the semantics of the out capability:τa[c[out a.Q | N] | L] | out a.P −→ c[Q | N] | a[L] | P(13)

The process out a.P in (13), the environment, has issued a visa to an ambientfrom a. In our view (13) is more compatible with (11) than (12). In both rules theaccepting sides, the ambient in (11) and the environment in (13), have the final
say.
Merro and Hennessy’s SAP, the Calculus of Safe Ambients with Passwords,
studied in the aforementioned paper adopts the semantics of (5) and (13) withadditional gadgets called the passwords.
There is still some incompatibility between (11) and (13). The rule (11) suggeststhat an environment is a bunch of ambients. The rule (13) says otherwise. This raises
the question concerning the citizenship of ambients:
Question 1: Do all interactions happen between ambients?
If we really believe that ambients are first class citizens, it is reasonable for us toassume that all interactions are between ambients. This brings us to the following
semantic rule:τa[c[out a.Q | O] | L] | b[out a.P | N] −→ a[L] | c[Q | O] | b[P | N]

(14)

Comparing (14) to (11), one immediately sees that the pair in, in is less error prone
than the pair out, out. For example the two sub-ambients named a in
a[in b.L1 ] | a[in c.L2 ] | b[in a.L3 ]does not cause ambiguity. On the other hand, there is no control over the next interaction in the following systema[c[out a.N1 ] | d[out a.N2 ]] | b[out a.N3 ]Fair ambients539

To remedy this we propose that an ambient leaving a host ambient must specify thereason to do that. In other words, it must specify the name of the ambient that calls
upon it. This can be formulated by the following ruleτa[c[out b.Q | O] | L] | b[out a.P | N] −→ a[L] | c[Q | O] | b[P | N]

(15)

Now the ambient c[out b.Q | O] specifies for whom it may move out of a.
Let’s now go back to the original motivation, that is to describe a situation in which
an ambient moves from one ambient to another. Using the semantics prescribed in(11) and (15) we have the following reductions:τa[c[out b.in b.M] | P] | b[out a.in c.Q] −→ a[P] | c[in b.M] | b[in c.Q]τ−→ a[P] | b[c[M] | Q]
For ambient B to import ambient A from ambient A, the ambient B needs to knowboth the name of A and the name of A . It is our intuition that (11) and (15) support a more streamlined semantics, both operationally and observationally. They also
provide a reasonable answers to questions about anonymity.
1.2 Anonymity
For mobile ambients anonymity is an important issue. Consider the ambient(n)n[P]
This is an anonymous ambient since its name is a secret to the outside world. For
anonymity there is a basic question on Anonymous-Entrance/Anonymous-Exit:
Question 2: To what extent may an anonymous ambient cross the border ofanother ambient?
Anonymous Entrance is the entrance of an anonymous ambient into another ambient. Anonymous Exit refers to the action in the opposite direction. It is clear fromthe following reductions that MA and SA admit both Anonymous-Entrance andAnonymous-Exit:τ(b)b[in a.Q] | a[P] −→ a[(b)b[Q] | P]
τa[(b)b[out a.Q] | P] −→ (b)b[Q] | a[P]τ(b)b[in a.Q] | a[in.P] −→ a[(b)b[Q] | P]
τa[(b)b[out a.Q] | out.P] −→ (b)b[Q] | a[P]In MA an ambient may sneak in or out of an ambient without any consent of thelatter. In SA an ambient would notice that someone has got in or out but wouldn’tknow who. PAC and SAd support Anonymous-Exit, as can be seen from the following
reductions:τa[(b)(b[Q] | out b) | P] −→ (b)b[Q] | a[P]τ

a[(b)(b[out.Q] | out b) | P] −→ (b)b[Q] | a[P]Similarly ROAM admits Anonymous-Exit. SAP admits Anonymous-Entrance andAnonymous-Exit.

540

Y. Fu

The anonymity is relevant to the extent that the following question should be
addressed: If the entrance/exit of an anonymous ambient can not be detected or
stopped, how can the entrance/exit of a vicious ambient be detected or stopped?
From the viewpoint of the algebraic theory, an anonymous ambient may or may
not be observable. It depends not only on whether the calculus admits Anonymous
Entarance/Anonymous Exit, but also on whether an anonymous ambient can be
broken from outside and/or from within. This brings us to another issue.
One can think of (a)a[P] as setting up a firewall around P. This view adds anotherdimension to anonymity. We say that a firewall is protective if it does not let any bad
things in; it is preventive if it does not let any good things out. A perfect firewall is bothprotective and preventive. A further question that can be asked about the anonymity
is concerned with Breaking-In-Firewall/Breaking-Out-Of-Firewall:
Question 3: To what degree may an ambient cross the border of an anonymous
ambient?
If the firewall of (a)a[P] can be broken in, then (a)a[P] looks like a ‘black hole’ thatsucks ambients. If the firewall of (a)a[P] can be broken out, then (a)a[P] appears as a‘white hole’ that produces ambients.
MA, SA and ROAM admit Breaking-Out-Of-Firewall. PAC and SAd support
Breaking-In-Firewall and Breaking-Out-Of-Firewall.
If all firewalls are perfect then Anonymous Entarnce/Anonymous Exit does noharm. On the other hand a system of the form(a1 ) · · · (an )(a1 [P1 ] | · · · | an [Pn ])with perfect firewalls is rather uninteresting, and very unreal in practice, if it does notproduce any ambients that interacts with environments. An interesting scenario arises
when a computational system takes the following standard form:(a1 ) · · · (an )(b1 [P1 ] | · · · | bm [Pm ])Here some bi [Pi ]’s are locally protected, some are not. The protected ambients canstill interact with the outside world through the unprotected ambients. The exchanged
messages have to be evaluated by a third party, which acts as a gateway between theprotected ambients and the outside world.
In this paper we focus on the ambients with perfect firewalls for systems of ambients. In other words the following proposition holds, where ≈ is an observational
equivalence.
Proposition 1.1 (System firewall) (a)a[n1 [N1 ] | · · · | nm [Nm ]] ≈ 0.
Notice that in most variants of MA the above proposition fails. In MA for instance
one has, assuming a  ∈ n(N), thatτ(a)a[n[out a.N]] −→ (a)a[0] | n[N]Notice also that Proposition 1.1, as well as other propositions on ambient firewalls, isconcerned with the observational theory of the ambients in a calculus. It is not about
the expressiveness of the calculus.

Fair ambients541

1.3 Three principles
We study in this paper the Calculus of Fair Ambients (FA for short). FA satisfies threeprinciples. The first is about the ambient citizenship:
First Class Citizenship: All actions are interactions. All interactions are between
ambients.
This principle rules out the reduction rules (2), (4), (6), (8), (10) and (12), since they do
not define interactions between ambients. It also disowns the rule (13) as it introduces
interactions between an ambient and a non-ambient. The second principle is about
the fair play between a client and a server:
Authorization: The two ambients involved in an interaction must obtain theauthorizations from each other.
This means that, apart from actions, there should be co-actions. One of the two interacting ambients authorizes a request from the other, the latter authorizes the service
by the former. According to the above principle the reduction rules (1) and (3) arebanned for no authorizations are given to the entrance. The third principle is aboutauthentication:
Authentication: The two ambients involved in an interaction must know eachother’s identities.
It means that two interacting ambients know each other’s names. If one thinks of it,
this is also about fair play. The rules (5), (7) and (9) do not meet this principle. Thisis because the ambient a[in a.P | L], for example, is not aware of the identity of theambient that enters it. For similar reason the rule (14) falls short of the requirement.
These principles can be regarded as a set of answers to Questions 1-3 put forth in theprevious subsections. They leave with us only one choice for the operational semantics
of FA: the one defined by (11) and (15). Notice that FA disowns Breaking-In-Firewall,
Breaking-Out-Of-Firewall and Anonymous-Entrance. In the absence of these, thepresence of Anonymous-Exit is harmless.
1.4 Mobility
Why do ambients migrate? They migrate because they are the computational
resources. In distributed computing, resources are bought and sold. The in and out
operators make for the bargaining of resources.
Now let’s take a look at the open operator from these perspectives. In MA thesemantics for the open capability is defined as follows:τ

open a.Q | a[P] −→ Q | P(16)The reduction (16) could be criticized in several accounts. To start with the ambient
a[P] should have the right to authorize the action. In SA this is taken into consideration. Levi and Sangiorgi have proposed in [20] a secure version of (16):τopen a.Q | a[open a.P | O] −→ Q | P | O

(17)

542

Y. Fu

Like in (13), the interaction in (17) violates the First-Class-Citizenship Principle. If
all interactions are between ambients, then (17) should really be replaced by thefollowing:τb[open a.Q | N] | a[open a.P | L] −→ b[Q | N] | P | L(18)

According to the the Authorization Principle, (18) can be improved as follows:τb[open a.Q | N] | a[open b.P | L] −→ b[Q | N] | P | L(19)

The open capabilities defined in (16) through (19) are quite different from the in andout capabilities. The in and out operations are about mobility, whereas open has little
to do with mobility. From the point of view of a buyer (19) is not a very economic wayof purchasing resources because everybody can make use of P | L.
Another reason to reject the present open capabilities is that an ambient mightevolve into a non-ambient. A system consisting of ambients could turn into anomaly
with ambients and non-ambients. Take for instanceb[open a | in a.N] | a[open b | in b.L | in c.L ] | c[in a.O]τ−→ b[in a.N] | in b.L | in c.L | c[in a.O]
Here the open action is more a destruction, or grave interference as termed in [20],than a competition for resources. In the literature this use of the open capabilities has
always been avoided of course. The following scenario, couched in the original MA,
seems to be the norm in many applications:ττu[open a.N | P] | a[in u.L | Q] −→ u[a[L | Q] | open a.N | P] −→ u[L | Q | N | P]
The ambient u imports the ambient a, and then immediately opens up a. Several points
are worth making about this example. First of all the ambient u opens up a for its own
use. It doesn’t do that for anybody else. This is supported by the fact that the open
operation is applied to the ambient a within u. Second the content of the ambient a
has moved into u. So mobility is present if an ambient opens up some resource for its
own purpose.
The Calculus of Mobile Ambient is a model for distributed and mobile computing.
It is reasonable to expect that all the operators of the ambients define mobility. In
this paper we propose an open operator that not only satisfies the three principles but
also introduces a kind of mobility and a kind of resource relocation. The semantics of
our open operator is prescribed by the following reduction:τb[open a.Q | N] | a[open b.P | L] −→ b[P | L | Q | N]

(20)

In other words, an open operation is an interaction of two ambients who know eachother’s names and authorize each other’s actions. The ambient b[open a.Q | N] terminates the ambient a[open b.P | L] by exhausting the entire internal resources of a for
its own use.
Comparing (20) and (19), one notices that the former is a local version of the latter.
The global open can simulate the local one. But the local open enjoys the subject

Fair ambients543
τ

reduction property: If M is a system of ambients and M −→ N then N is a system ofambients.
FA is equipped with the local open operator.
1.5 Contribution
The paper makes the following contributions:–––

Based on the analysis of the capability operators, we propose an operationalsemantics for the ambients that is defined purely in terms of a labeled transition
system. By exploiting the labeled transition system, we investigate four bisimulation congruence relations. The bisimilarity intends to make the least reference tocontexts. The barbed bisimilarity follows the standard definition. The observablebisimilarity and the weak observable bisimilarity are stronger and respectively
weaker than the barbed bisimilarity by definition. We prove that the four bisimilarities coincide. These results improve upon those of Merro and Hennessy inthat there is no use of passwords. The coincidence results are supported by the
Local Observability property stating that the equivalences are for processes thesame way as they are for ambients.
We propose a new operational semantics for communication that conforms to thethree principles. The presence of the communication forces all congruence relations to be closed under substitutions of names. We work out the algebraic theory
for FA with communication. In particular we prove that the four bisimilarities,
tailored to take into account of the communications, coincide.
We formally prove that the π-calculus is a sub-calculus of FA with communication.
We construct a translation from π to FA that not only preserves and reflects theoperational semantics but also preserves and reflects the observational semantics.
This result reveals the close relationship between π and MA, two well known
frameworks of mobile computing.

The approach advocated in this paper is general enough to help understand the observational theories of the other variants of the Ambient Calculus.
The rest of the paper is organized as follows: Sect. 2 defines the operational semantics of FA. Section 3 gives some examples to illustrate the expressiveness of FA.
Section 4 introduces the bisimilarity. Section 5 explains the Bisimulation Lemma crucial to the later proofs. Section 6 reinforces the role of the bisimilarity by showingthat it is the same as the observable bisimilarity. Section 7 proves that the bisimilarity
coincides with the barbed bisimilarity as well as the weak observable bisimilarity.
Section 8 studies the communication mechanism for FA. Section 9 establishes the factthat the π-calculus is a sub-calculus of FA. Section 10 highlights some major points.
The appendix reviews some definitions and carries out some proofs.

2 Labeled semantics
The semantics of FA is defined purely in terms of a labeled transition system. No
structural congruence is preordained. Let N be the set of names, ranged over by
a, b, c, . . .. A finite sequence x1 , . . . , xn of names, as well as the set {x1 , . . . , xn }, will beabbreviated to x. The abstract syntax of process is defined by the following abstract

544

Y. Fu

grammar:
P := 0
κ.P
P|P
a[P]
(a)P
!P
where
κ := in a
in a
out a
out a
open aopen aHere κ stands for a capability. If κ is in a (in a, out a, out a, open a, open a), we call a thetarget name of κ and is denoted by n(κ). The capabilities have the following readings:
–
–
–
–
–
–

“in a” reads “get into a”.
“in a” reads “get a”.
“out a” reads “get out to reach a”.
“out a” reads “get someone from a”.
“open a” reads “open up a”.
“open a” reads “be opened up by a”.

Processes of the form a[P] or (a)a[P] are called ambients, where a is the name of theambient. Sometimes we say “ambient a”, or even “a”, to refer to the ambient a[P]when no confusion arises. A process consisting of a collection of ambients is called asystem. Formally systems are defined by the following grammar:
S := 0
S|S
a[P]
(a)S
!S
Throughout the paper we stick to the following notational convention:–––

L, M, N, O, P, Q, L , M , N  , O , P , Q , . . . stand for processes;
S, T, S , T  , . . . stand for systems;
A, B, A , B , . . . stand for ambients.

Interactions between ambients are higher order. In order not to introduce higher
order action labels in the operational semantics, one uses concretions and contexts.
The grammar of the concretions is as follows:
D := PP | (x)DFair ambients545

To define the structural semantics, it is convenient to extend the scope of the composition and the restriction operators to cover also the concretions. Suppose D is (m)OPand P is not 0. Then the extension is defined as follows:def ∩ fn(Q) = ∅
if m

def

 ∩ fn(Q) = ∅if m

D | Q = (m)O(P | Q)
Q | D = (m)O(Q | P)
def(x)(O0) = (x)O0
def

if x ∈ fn(O)def

if x  ∈ fn(O)m)OP(x)D = (x)(
(x)D = (m)O(x)PContexts are environments that can make finite observations. This simple statement
suggests two things: (i) There is no need for the replication operator, or recursion, inthe contexts; and (ii) There need be only one hole in a context.
Definition 2.1 Static contexts are defined as follows:––[_] is a static context;
if C[_] is a static context then C[_] | A, A | C[_], (x)C[_] are static contexts.

Contexts are defined as follows:––a static context is a context;
if C[_] is a context then a[C[_]] is a context.

An ambient context at a is a context of the form C [a[C [_]]] where C [_] is a context
and C [_] is a static context. A standard ambient context at a is an ambient context
of the form a[_ | O]. An ambient context is an ambient context at some name.
We will let U, U  , . . . to range over the set of processes, concretions and contexts.
In the rules defining the operational semantics λ ranges over the action labels
defined below:
λ := κ
a[κ], if κ  = out b for every b[out b]a[[out b]]τ
An action could be a process action of the form κ, invoked by the capability κ. It
could be the τ action indicating an interaction. It could also be an action performedby ambients. The intuition behind the ambient actions is this:
–
–
–
–
–
–
–

“a[in b]” reads “ambient a moves into ambient b”.
“a[in b]” reads “ambient a imports ambient b”.
“[out b]” reads “the surrounding ambient moves out to reach ambient b”.
“a[out b]” reads “ambient a extracts an ambient out of ambient b”.
“a[open b]” reads “ambient a opens up ambient b for its internal resource”.
“a[open b]” reads “ambient a is opened up by ambient b and donates its resource
to ambient b”.
“a[[out b]]” reads “an ambient moves out of ambient a to reach ambient b”.

546

Y. Fu

Fig. 1 The operational semantics of FA

The labeled transition system is defined in Fig. 1. Notice that all symmetric rules areomitted. Most of the rules are self-explanatory. We only make a couple of comments:––

There are three groups of rules. The first explains how the process actions persist
through the structural composition. The second introduces the ambient actions.
The third defines the interactions between ambients.
λThere are three kinds of transitions. One is of the form P −→ P for a process
λP ; the second is of the form P −→ D for a concretion D; and the third is of theλform P −→ C[_] for a context C[_]. Here the context plays a role similar to thatof abstraction. In [22] the authors use concretions instead of contexts. We use
contexts because we do not impose a structural congruence on the syntax of theprocesses.
–

λA transition P −→ U emphasizes two things: One is that P performs an action
denoted by λ. The other is that the action achieves the effect codified by U. Intuλitively the transition P −→ (m)MP indicates the followings: (i) P is able toinvoke a higher order interaction; (ii) M, the dynamic, is the part to move; (iii) . MoreP , the residual, is the part to stay; (iv) M and P share the local names ma[in b]specifically P −→ (m)AP means that A is to move into an ambient b; and[out b]––m)AP that A is to move out to reach ambient b.
P −→ (Our concretions is different from those in [22]. Merro and Hennessy have transiλtions like P −→ (m)P n P . It indicates that after the interaction, not necessarily
before the interaction, P is in ambient n and P is outside the ambient n. Here thestructural aspect of the resulting process is emphasized. Our concretions stressmore on the dynamic aspect.
We have chosen the action label [out b] instead of a[out b]. This is because anambient can not see inside another ambient. In c[L] | b[a[M]] for example c[L]Fair ambients547

can see b but not a. Using the label a[out b] would suggest that a was observable,
which was not true.
We will use some common notations and abbreviations. For instance we will writeτλλ⇒ for the reflexive and transitive closure of −→, and ⇒ for ⇒−→ ⇒. We will
leave out ambients like 0, a[0] and a[b[0] | c[0]], etc. to improve readability.
Let’s take a look at a couple of examples of derivations using the operational rules:
One hasout a

out a.B −→ Bb[out a]b[out a.B] −→ b[B]
and
out b

out b.A −→ A
[out b]c[out b.A] −→ c[A]0[out b](c)c[out b.A] −→ (c)c[A]0[out b]

N | (c)c[out b.A] −→ (c)c[A]N[out b](x)(N | (c)c[out b.A]) −→ (x)(c)c[A]Na[[out b]]a[(x)(N | (c)c[out b.A])] −→ (x)((c)c[A] | a[N])where we have assumed that x ∈ fn(A). We can then apply the second interaction rule
to obtain the following transition
τa[(x)(N | (c)c[out b.A])] | b[out a.B] −→ (x)((c)c[A] | a[N]) | b[B]This example shows why the label [out b] is preferred over the label c[out b]. It also
helps to understand the restriction operation on concretions.
In the rest of the paper we will occasionally say something like “let x be a freshname” or “for a fresh name x”, by which we mean that x does not occur in any
syntactical objects under consideration.
Before ending this section we state some simple properties to be used later on.
Lemma 1 The following properties hold:a[in b](i)

If P −→ U then U is an ambient context at a.

(ii)

If P −→ U then U is an ambient context at a.

a[open b]

3 Examples
This section serves to demonstrate some of the expressive power of FA by giving several examples. Without communication mechanism FA, like MA, is good to express
mobility, but not very convenient to code up functional computation. We will see howcommunications help to promote FA to accommodate the functional computing stylein later sections. We make use of the strong bisimilarity ∼, defined in Appendix A, inthe following examples.

548

Y. Fu

Example 1 (Renaming) The open capability provides an easy way of renaming an
ambient. An ambient whose behavior is the same as a[P] could be renamed to b[P]as the following reduction demonstrates:τb[open a] | a[open b | P] −→ b[P]This property is explored in the following reductions
τb[Q | (n)(n[open a] | a[open n.P] | a[open n])] −→ b[Q | (n)(n[P] | a[open n])]⇒ b[Q | (n)(n[open a.P ] | a[open n])]τ−→ b[Q | a[P ]]The ambient a is made anonymous and is then restored to the original name later on.
In the anonymous state the process P carries out computations with full protection. 
Example 2 (Unknown resource and target) Let S be the system(m)(a[in m.Q] | m[in a.open b] | b[open m.P])
Then one has the following reduction:τS −→ (m)(m[a[Q] | open b] | b[open m.P])τ−→ b[a[Q] | P]
The ambient a[in m.Q] enters a transfer m[in a.open b]. It is then shipped to a place it
doesn’t know. The target does not know the name of a[in m.Q] either. Both a and bknow that they are doing business with a trusted party m.

Example 3 (Out) Using the out capability one could define a[b[out.B] | A] by the following system (d)(a[b[out d.B] | A] | d[out a]), where d is fresh. The following reductionis admissibleτa[b[out.B] | A] −→ b[B] | (d)a[A] ∼ b[B] | a[A]Notice that the ambient b[out d.B] might move to another ambient caused by aco-open action of A. But b[out d.B] retains the ability to move out.
In the following examples, out will be used as a primitive. When this derived operator is used, it should be understood that the necessary co-out operators are inserted
in the right place.
Example 4 (Universal resource) Let N be n[A | open a.P] | R, where A is the ambient
a[out.open r.open n] and R is the resource defined by !r[open a.M]. There is an obvious
reduction sequenceτN −→ a[open r.open n] | n[open a.P] | Rτ−→ a[M | open n] | n[open a.P] | Rτ−→ n[M | P] | R
Here R provides the universal resource M that can be accessed by ambients named
a. The ambient n[A | open a.P] sends out an envoy with name a whose mission is tofetch a piece of code from R. In FA mediators, or matchmakers, play a heavy role ingetting access to universal resources.
Fair ambients

549

Example 5 (Non-deterministic choice for ambients) Let d[open a] + d[open b] be(c)(c[open d.open a] | c[open d.open b] | d[open c])
Then clearlyτd[open a] + d[open b] −→∼ d[open a]τd[open a] + d[open b] −→∼ d[open b]
The nondeterministic choice a[P] + b[Q] is then defined by(d)((d[open a] + d[open b]) | a[open d.P] | b[open d.Q])
It should be remarked that these definable choices are all internal choices.



Example 6 (Numerals) We introduce the special names num, dec, op, zero for thenumerals and true for the booleans. The numerals are defined as follows:def

0 = num[!out zero | !out op | !in num]def

n+1 = num[n | !out op | !in num | open dec]
And the operations on the numerals are defined as follows:def+1 = num[in num.(!out op | !in num | open dec)]
def−1 = (x)(dec[open num.open x] | x[open dec] | op[out x])
def?0 = zero[true[out num. . . .]]The definition of the predecessor makes use of a local name to garbage collectunwanted codes. It is easy to check out the following properties:τn | +1 −→∼ n+1
τ

n+1 | −1 ⇒∼ n
τ

0 | ?0 −→∼ 0 | true[. . .]A system wants to test or operate on the numerals may send an envoy to do the job.
A better encoding of the numerals is possible using communications.

Example 7 (Facilitated diffusion) Facilitated diffusion is a process of diffusion wheremolecules diffuse across membranes with the assistance of transport proteins. Actually transport or transmembrane proteins form channels through the cell membranes.
The channel can be opened or closed and molecules pass down a concentration gradient. When the concentration of the molecules in the cell is lower than that in theenvironment, the channel is opened by the cell and molecules may enter into the cell.
This could be described by the following interaction:
τcell[in mol | P] | mol[in cell | out env | Q] −→ cell[P | mol[out env | Q]]
When the concentration of molecules in the environment is lower than that in the cell,
the channel is opened by the environment and the molecules exit from the cell. This
could be described by the following interaction:
τcell[P | mol[out env | Q]] | env[out cell | R] −→ cell[P] | mol[Q] | env[R]See for example [7,33] for more on the process approach to system biology.



550

Y. Fu

Example 8 (Text encryption) Suppose that the sender S wants to send a text T to thereceiver R. The text must be encrypted during transition. Let S bea[A | d[in k.out k.T] | k[in d.out b.in b]]
and R beb[B | out a.in k | k[out k]]
Thenτ(k)(S | R) −→ (k)(a[A | k[d[out k.T] | out b.in b]] | b[B | out a.in k | k[out k]])τ−→ (k)(a[A] | k[d[out k.T] | in b] | b[B | in k | k[out k]])τ−→ (k)(a[A] | b[B | k[d[out k.T]] | k[out k]])τ−→ (k)(a[A] | b[B | d[T]])The sender and the receiver share the key k. The sender first encrypts the text withthe key k. The encrypted text leaves the sender and is on its way to the receiver.
The receiver then accepts the encrypted text. It decrypts the encrypted text using the
key k.

Example 9 (Firewall) Cardelli and Gordan give in [11] an example of using MA tocode up a firewall protocol. We are now adapting the example to FA. The firewall Fw
and the Agent ag are defined as follows:def

Fw = (f )f [k[out.out ag.in r.open f ] | open k.M | P]
def

Ag = ag[r[out k.in k.R] | N]
The system Fw | Ag have the following operational behavior:τ

Ag | Fw −→ ag[r[out k.in k.R] | N] | (f )(k[out ag.in r.open f ] | f [open k.M | P])τ−→ ag[N] | r[in k.R] | (f )(k[in r.open f ] | f [open k.M | P])τ−→ ag[N] | (f )(k[open f | r[R]] | f [open k.M | P])τ−→ ag[N] | (f )f [r[R] | M | P]
The system Fw protected by a firewall intends to fetch a piece of resource r[R] fromthe agent ag. Since nobody is supposed to cross the border of the firewall, the systemFw sends out a legate k[out ag.in r.open f ]. The agent ag[r[out k.in k.R] | N] knows
the watchword of the legate, and is happy to pass the resource to the legate. The latterthen uploads the resource to the protected system.

Example 10 (Membrane fusion) Cellular membrane fusion is well known. It is one of
the most common ways for molecules to enter or exit cells in processes like fertilization and viral infection. When two cells fuse together, their membranes come together
at one location and create a connection between the cells that allows the exchange ofmaterials between them. Eventually the two membranes form one single, continuous
membrane surrounding the contents of both cells. We can describe for example thesituation when a virus enters a cell by the following reduction:
τcell[open virus | P] | virus[open cell | Q] −→ cell[P | Q]
This is an example of using the local open capability.

Fair ambients

551

4 Bisimulation
Process equivalences are observational in the sense that two processes are equivalent
if no context can detect any difference between them. When a process is put in a context, the latter observes the former by interacting with it. To establish the equivalenceof two processes one has to examine them in all contexts. The universal quantification implies that the observational equivalences are congruent. It also means thatreasoning about the observational equivalences is not easy. Bisimulation equivalences([26,28]) are proposed to approximate the observational equivalences with the aim
to reduce the reference to contexts.
In view of the above remark, it is clear that the challenge of a bisimulation approachis to define an equivalence relation that meets two goals: (i) its dependency on contexts
is minimal; (ii) it makes good sense from the observational point of view. What has tobe kept in mind is that ambient interactions are of higher order in nature. An ambient
action could send an ambient to the environment. It could also receive an ambientfrom the environment. When an ambient has left a host ambient, it still shares somelocal names with the ex-host. This means that from an observational point of view
it is wrong to consider the ambient and the ex-host in isolation. So bisimulations forambients can hardly be without any reference to contexts. But what kind of contexts
should we consider? When an ambient has emigrated to another ambient it will beplaced in an ambient context of the form a[C[_]]. When an ambient is importing an
ambient, the immigrant is to be put in an ambient context of the form a[C[_]]. In
both cases C[_] is a static context. Now the ambient context a[C[_]] is structurally
equivalent to (x)a[_ | O] for some O. With this observation in mind, it should not bedifficult to see that we only have to consider contexts of the form a[_ | O], the standard
ambient contexts.
We are now in a position to define the bisimulations for the ambients.
Definition 4.1 A symmetric relation R on processes is a bisimulation if the followings
hold whenever PRQ:
τ

1.
2.

If P −→ P then Q ⇒ Q RP for some Q .
κκ
If P −→ P then Q ⇒ Q RP for some Q .

3.

If P −→ P and λ ∈ {a[out b], a[[out b]] | a, b ∈ N } then Q ⇒ Q RP for some
Q .

4.

∩
If P −→ (m)AP then for every name d and every process O satisfying m

λ[out a]fn(O) = ∅ there exist some n, B, Q , Q such that Q(n)(B | d[Q | O]) ⇒ Q R (m)(A | d[P | O]).
5.

λ[out a]⇒ −→ (n)BQ anda[in b] ∩ fn(O) = ∅ there
If P −→ (m)AP then for every process O satisfying ma[in b]n)BQ and (n)(Q | b[B | O]) ⇒exist some n, B, Q , Q such that Q ⇒ −→ (Q R (
m)(P | b[A | O]).
6.

If P

a[open b]−→

 ∩ fn(O) = ∅ some(m)MP then for every process O satisfying mn, N, Q , Q exist such that Q
Q R (m)(P | b[M | O]).
7.

a[open b]⇒ −→(n)NQ and (n)(Q | b[N | O])a[in b]⇒If P −→ C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist somea[in b]C [_], Q such that Q ⇒ −→ C [_] and C [b[N]] ⇒ Q R C[b[N]].

552

8.

Y. Fu

If P

a[open b]−→

C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist
a[open b]

some C [_], Q such that Q ⇒ −→ C [_] and C [N] ⇒ Q R C[N].
The bisimilarity ≈ is the largest bisimulation.
Here are some explanations about the definition:
1.
2.

3.
4.

5.

6.
7.
8.

Clause (1) is standard for bisimulations.
Clause (2) discusses the case when P can perform a capability κ. A capability
invokes an ambient relocation. In FA all capabilities are exercised within ambients. A reasonable requirement is b[P | O]Rb[Q | O] for every name b and every
process O. We shall see that the weaker condition P RQ is sufficient.
Clause (3) implies that the effect of the a[out b] action or the a[[out b]] action is
local.
Clause (4) deals with the case where the ambient A is to emigrate from an ambient d. To account for all possible structures of the contexts, the ambient A must
be considered together with d[P | O].
Clause (5) describes the situation that an ambient A is capable of moving into an
ambient named b. Without losing generality one could take this ambient to beb[_ | O]. Then b[A | O] and P should be considered in combination in simulation.
Clause (6) is similar to clause (5) except that the process exported is not an
ambient but the internal resources of an ambient.
Clause (7) takes into account of the fact that if P can perform the action a[in b]then the ambients it may import must be of the form b[N].
Clause (8) is similar to clause (7) except that the process imported is not an
ambient but the internal resources of an ambient.

The bisimulations defined by Definition 4.1 is what one might call early bisimulations. This is clear from the clauses (4) through (8) of the definition. A late version of
the clause (8) for instance is this:a[open b]

If P −→ C[_] then there exists some C [_] such that Q
C [N] R C[N] for every N satisfying fn(N) ∩ bn(C[_]) = ∅.

a[open b]⇒

C [_] anda[open b]

We need to define the reductions of context to make sense of the notation Q⇒
C [_]. But it is intuitively clear. Late bisimulations are desirable since they are simpler.
We have not been able to show that the late bisimilarity coincides with the early one.
Let’s now see some examples:
–
–

–
–
–

–

a[0] ≈ c[a[0] | b[0]]. Both are equivalent to 0.
(a)a[out b.P]  ≈ 0 even if a  ∈ fn(P). When putting in an ambient context likec[_ | O], the ambient (a)a[out b.P] could move out of the context if environments
want it.
(a)a[n[N] | in b.M] ≈ 0.
(a)a[n[N] | out b.M] ≈ (a)a[out b.(n[N] | M)].
(c)a[b[out c.A]] ≈ 0 for fresh c. This is because all the ambient b[out c.A] can dois to move out of a. But this capability can not be invoked since no environment
knows c. In general (c)C[κ.P] ≈ C[0] if n(κ) = c and c does not occur in C[0].
The equivalence fails in the presence of communication.
[out a](d)b[out a.in d] ≈ c[out a]. This is because (d)b[out a.in d] −→ (d)b[in d]0 can[out a]be simulated by c[out a] −→ c[0]0, and vice versa.

Fair ambients553

It goes without saying that the observational equivalences must be equivalence
relations. So we need to state the following fact before going further.
Proposition 4.2 The bisimilarity ≈ is an equivalence.
A further justification of Definition 4.1 is the following congruence theorem, whose
proof is subsumed by the proof of Lemma 14.
Theorem 4.3 Suppose P ≈ Q. Then the following holds:(i)κ.P ≈ κ.Q;

(ii)

P | R ≈ Q | R;(iii)(x)P ≈ (x)Q;(iv)

a[P] ≈ a[Q];(v)!P ≈!Q.

An often used technique to prove equivalence makes use of the bisimulation-up-to
relations. Appendix A recalls two such relations relevant in this paper.

5 Bisimulation lemma
In the observational theory of the process calculi, processes are studied in terms of
their external interactional behaviors. The internal interactions, the tau actions, can
not be observed per se. But their effects can often be observed. Let’s take a look at
three situations. The first is when an internal action is of the form
τP0 −→ P1
such that P0 does not have any other actions. In this case it is clear that P0 ≈ P1 . The
second is the following situationλτP2 ←− P0 −→ P1
where P0 can perform at least one other action λ. In this case the difference between
P0 and P1 can normally be observed if there is a difference. The third situation is
τ

τ

τ

τ

τ

P0 −→ P1 −→ · · · −→ Pn−1 −→ Pn −→ P0
where Pi , for i ∈ {1, . . . , n}, may have other actions apart from the tau action. Thiscase is interesting because of the following fact.
τ

τ

τ

τ

τ

Lemma 2 (O-Lemma) If P0 −→ P1 −→ · · · −→ Pn−1 −→ Pn −→ P0 then P0 ≈P1 ≈ . . . ≈ Pn−1 ≈ Pn .
λτλWhy is Pi ≈ Pj ? Because C[Pi ] −→ U can be simulated by C[Pj ] ⇒ C[Pi ] −→ U if
Pi participates the action. The following is a consequence of the O-Lemma.
Corollary 5.1 Suppose P0 0 P1 1 · · · Pn−1 n−1 Pn n P0 where, for each i ∈ {1, . . . , n},
i is either ⇒ or ≈. Then P0 ≈ P1 ≈ . . . Pn−1 ≈ Pn .
A special form of Corollary 5.1 is what we call Bisimulation Lemma.

554

Y. Fu

Lemma 3 (Bisimulation lemma) If P ⇒ P ≈ Q and Q ⇒ Q ≈ P then P ≈ Q.
The above lemma says that P ≈ Q if P and Q are related in the following mannerP ⇒≈ Q
Q ⇒≈ P
We call it Bisimulation lemma because the statement of the lemma reminds one of
the bisimulation properties. It is a general result valid for all the equivalences we areaware of. Bisimulation lemma plays a crucial role in the studies of π and χ carriedout in [14] and [13,17] respectively. It also plays a crucial role in this paper.

6 Observable bisimulation
A widely studied bisimulation equivalence is the so called barbed bisimilarity [29],which is based on the notion of barbedness. For ambient calculi the question is how
to define the barbedness. There are two ways:–

One is the syntactical approach. This is often used when the underlying operational semantics is presented in a reductional style. In [22,24] for instance, it isdefined that P is barbed at a if
P ≡ (
x)(a[open a.P | R] | O)–

where a  ∈ 
x. Other definitions are possible.
The other is the observational approach. Barbs are defined in terms of the action
labels. This is preferred if a labeled transition system is available. In π-calculus,
a barb of a process is a channel through which the process may communicate. In
ambient calculi a barb is the name of an ambient that can act. Take for instance theprocess a[0]. From an observational point of view, a[0] is as good as the inactive
process 0. Therefore a[0] does not have any barb.

The two approaches are not always equivalent. In some variants of MA, say SA, thetwo ambients a[in n] and b[in n] are barbed equivalent according to the first definition.
They are not barbed equivalent according to the second definition. The point is thatdifferent process calculi and different variants of a process calculus may have different
barbedness.
In this paper we study a bisimulation equivalence that is similar to but more robust
than the barbed bisimilarity. The equivalence emphasizes the observable actions aprocess is able to perform at a particular state.
λDefinition 6.1 A process P is observable at a non tau action λ, noted P⇓λ, if P ⇒−→U for some U. A process P is observable, notation P⇓, if P⇓λ for some λ. P  ⇓ if not P⇓.
Definition 6.2 A relation R is observable if PRQ ⇒ ∀λ.(P⇓λ ⇔ Q⇓λ).
With these definitions we may define observable bisimulations as in the next
definition.

Fair ambients

555

Definition 6.3 A symmetric relation R on processes is an observable bisimulation if
the following properties hold:
(i)
(ii)

It is observable and is closed under context;
τIf QRP −→ P then Q ⇒ Q RP for some Q .

The observable bisimilarity ≈obs is the largest observable bisimulation.
It should be clear that the bisimilarity ≈ is an observable bisimulation. The restof the section is devoted to the proof that ≈obs is a bisimulation. First we prove atechnical lemma.
Lemma 4 Suppose c is fresh. Then a[P | O] ≈obs a[Q | O] if either a[P | in c.O] ≈obs
a[Q | in c.O] or a[P | out c.O] ≈obs a[Q | out c.O] or a[P | open c.O] ≈obs a[Q | open c.O].
τ

Proof It is clear that the following reduction a[P | in c.O] | c[in a] −→ a[P | O] must
be matched up by
a[Q | in c.O] | c[in a]⇒ a[Q1 | in c.O] | c[in a]τ−→ a[Q1 | O]
⇒ a[Q | O ]≈obs a[P | O]
A crucial observation is that the above reduction sequence can be rearranged asfollows:τa[Q | in c.O] | c[in a] −→ a[Q | O]
⇒ a[Q | O ]≈obs a[P | O]
Consequently
a[Q | O] ⇒≈obs a[P | O]

(21)a[P | O] ⇒≈obs a[Q | O]

(22)

Symmetrically
It follows from (21), (22) and the Bisimulation lemma (Lemma 3) that a[P | O] ≈obs
a[Q | O].
The observable bisimulations are not very tractable. Results like the one given
below are always useful.
Lemma 5 If a[P | open b] ≈obs a[Q | open b] for a fresh b then C[P] ≈obs C[Q] forevery ambient context C[_].
Proof For arbitrary x and O let C [_] be the context
a[_ | open b] | b[open a.open c] | c[open b.open x.out c] | x[open c.O] | c[c[out x]]
where c is fresh. Then clearlyτC [P] −→ b[P | open c] | c[open b.open x.out c] | x[open c.O] | c[c[out x]]τ−→ c[P | open x.out c] | x[open c.O] | c[c[out x]]τ−→ x[P | out c | O] | c[c[out x]]τ−→ x[P | O]

556

Y. Fu

Since C [P] ≈obs C [Q], the above reduction sequence must be simulated by
τC [Q] ⇒ x[Q | O] ⇒ Q
for some Q , which could be rearranged asτ

C [Q] ⇒ x[Q | O] ⇒ x[Q | O] ⇒ Q
Therefore x[Q | O] ⇒ Q ≈obs x[P | O]. Similarly one has x[P | O] ⇒ P ≈obs
x[Q | O]. Thus x[P | O] ≈obs x[Q | O] by Lemma 3. It is then easy to prove that
C[P] ≈obs C[Q].

We now come to the major result of this section. It relates the bisimilarity of two
processes to the observable bisimilarity of the processes.
Theorem 6.4 P ≈obs Q if and only if P ≈ Q.
Proof Let R be the following relation{(P, Q) | c[P | open d] ≈obs c[Q | open d] for fresh d}
We shall prove that R is a bisimulation. Suppose that Q R P and P does a λ action. It
follows from the assumption c[P | open d] ≈obs c[Q | open d] and Lemma 5 that
C[P] ≈obs C[Q](23)

for every ambient context C[_]. We will make extensive use of (23) without explicitly
referring to it. The proof is a case analysis on λ.
–λ = τ . This case is simple.

–

λ = in b and P −→ P . Let C[_] be c[_ | out e.open d] | b[in c] | e[out b], where e isfresh. Then

in b

τ

C[P] −→ b[c[P | out e.open d]] | e[out b]τ−→ c[P | open d]
It follows that the above reduction must be matched up byτ

C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]in bHence Q ⇒ Q R P .
–in b

λ = in b and P −→ P . For a fresh e, let C[_] be the context
c[_ | open d] | b[in c.out e] | e[out c]Thenτ

C[P] −→ c[P | b[out e] | open d] | e[out c]τ−→ c[P | open d]τin b

The simulation must be C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]. Thus Q ⇒Q R P  .

Fair ambients

–

557
out b

λ = out b and P −→ P . For a fresh e, let C[_] be the context
c[_ | in e.open d] | e[in c] | b[out e]ThenτC[P] −→ e[c[P | open d]] | b[out e]τ−→ c[P | open d]
τ

out b

The simulation must be C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]. Thus Q ⇒Q R P  .
–

out b

λ = out b and P −→ P . For a fresh e, let C[_] bec[_ | open d] | b[e[out c.e[out e]]] | e[out e]ThenτC[P] −→ c[P | open d] | e[e[out e]] | e[out e]τ−→ c[P | open d]
τ

out b

The simulation must be C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]. Thus Q ⇒Q R P  .
–open bλ = open b and P −→ P . For a fresh e, let C[_] bec[_ | open d] | b[open c.open e] | e[open c]
Thenτ

C[P] −→ c[P | open e | open d] | e[open c]τ−→ c[P | open d]τ

The simulation must be C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]. Thus Q
Q R P  .
–open b⇒open bλ = open b and P −→ P . For a fresh e, let C[_] bee[_] | b[open e.open c.open d] | c[open b.out e] | e[e[out c]]Thenτ

C[P] −→ b[P | open c.open d] | c[open b.out e] | e[e[out c]]τ−→ c[P | open d | out e] | e[e[out c]]τ−→ c[P | open d]τ

The simulation must be C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]. Thus Q
Q R P  .
–a[out b]λ = a[out b] and P −→ P . For a fresh e, let C[_] bec[_ | b[d[out a.out e]] | open d] | e[out c]Thenτ

C[P] −→ c[P | d[out e] | open d] | e[out c]τ−→ c[P | open d]

open b

⇒

558

Y. Fu
τ

The simulation must be C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]. Thus Q
Q R P  .
–a[out b]⇒a[[out b]]

λ = a[[out b]] and P −→ P . For a fresh e, let C[_] bec[_ | b[out a.out e] | open d] | e[out c]Thenτ

C[P] −→ c[P | b[out e] | open d] | e[out c]τ−→ c[P | open d]τ

The simulation must be C[Q] ⇒ c[Q | open d] ≈obs c[P | open d]. So Q
Q R P  .
–a[[out b]]⇒[out a]λ = [out a] and P −→ (m)AP . Let e be fresh and O be a process such that{m} ∩ fn(O) = ∅. Define the context C[_] by
c[d[_ | out a.O] | a[out d.d[out d.out e]] | open d] | e[out c]
It is clear that
τ

C[P] −→ c[(m)(A | d[P | out a.O]) | a[d[out d.out e]] | open d] | e[out c]τ−→ c[(m)(A | d[P | O]) | d[out e] | open d] | e[out c]τ−→ c[(m)(A | d[P | O]) | open d]
The simulation of the above reduction sequence can be rearranged as follows:
C[Q] ⇒ C[Q ]τ−→ c[(n)(B | d[Q | out a.O]) | a[d[out d.out e]] | open d] | e[out c]τ−→ c[(n)(B | d[Q | O]) | d[out e] | open d] | e[out c]τ−→ c[(n)(B | d[Q | O]) | open d]⇒ c[Q | open d][out a]n)BQ and
It then follows that Q ⇒ −→ ((n)(B | d[Q | O]) ⇒ Q R (m)(A | d[P | O])–a[in b]λ = a[in b] and P −→ (m)AP . For process O and fresh e, let C[_] be thecontextc[_ | b[in a.out d.O] | d[d[out b.out e]] | open d] | e[out c]
Now clearly the reduction sequenceτm)(P | b[A | out d.O]) | d[d[out b.out e]] | open d] | e[out c]
C[P] −→ c[(τ−→ c[(m)(P | b[A | O]) | d[out e] | open d] | e[out c]τ−→ c[(m)(P | b[A | O]) | open d]Fair ambients

559

must be matched up by C[Q]follows:τ⇒ c[Q | open d], which can be rearranged as

C[Q] ⇒ C[Q1 ]τ−→ c[(n)(Q | b[B | out d.O]) | d[d[out b.out e]] | open d] | e[out c]τ−→ c[(n)(Q | b[B | O]) | d[out e] | open d] | e[out c]τ−→ c[(n)(Q | b[B | O]) | open d]⇒ c[Q | open d]a[in b]

It should be clear that Q ⇒ −→ (n)BQ andm)(P | b[A | O])(n)(Q | b[B | O]) ⇒ Q R (–a[open b]

λ = a[open b] and P −→ (m)MP . For process O and fresh e, let the context
C[_] be C [_ | b[open a.out d.O]] where C [_] isc[_ | d[d[out b.out e]] | open d] | e[out c]
The rest of the argument is completely the same as in the previous case.

–a[open b]

λ = a[open b] and P −→ C1 [_]. For process N and fresh e, let the context C[_]bec[_ | b[open a.out d.N] | d[d[out a.out e]] | open d] | e[out c]Thenτ

C[P] −→ c[C1 [out d.N] | d[d[out a.out e]] | open d] | e[out c]τ−→ c[C1 [N] | d[out e] | open d] | e[out c]τ−→ c[C1 [N] | open d]which is simulated by C[Q] in the following mannerττ

C[Q] ⇒ c[C2 [N] | open d] ⇒ c[Q | open d]a[open b]

Thus Q ⇒ −→ C2 [_] and C2 [N] ⇒ Q RC1 [N].
–a[in b]λ = a[in b] and P −→ C1 [_]. For process N and fresh names e, f , g, let the context
C[_] be defined byc[_ | b[in a.(N | out f ) | open e.out e] | O]
where O is e[open b | out g] | open d. Then clearlyτC[P] −→ c[C1 [b[N | out f | open e.out e]] | O]
By Lemma 1, C1 [_] is an ambient context at a. The ambientb[N | out f | opene.out e] might get out of a. When it is out of a it could interact withthe ambient e[open b | out g]. Thus we have the following important observation:
Either c[C1 [b[N | out f | open e.out e]] | O] is observable at both c[[out e]] andc[[out f ]], or it is observable at neither c[[out e]] nor c[[out f ]].

560

Y. Fu

Suppose that the above action of C[P] is simulated by
C[Q] ⇒ A
It is impossible for A to take the form C[Q1 ] since one would then have thefollowing reduction
τA −→ c[Q1 | e[in a.(N | out f ) | out e | out g] | open d](24)

Here the component in a.(N | out f ) gets stuck since e does not appear in Q1 . Itshould be clear thatc[Q1 | e[in a.(N | out f ) | out e | out g] | open d]
is observable at c[[out e]]. It is however not observable at c[[out f ]]. It follows thatthe reduction (24) could not be matched up by any descendants of c[C1 [b[N | out f |open e.out e]] | O]. Based upon the above analysis one concludes that the simulation must take the following form for some contexts C2 [_], C3 [_]:
C[Q] ⇒ C[Q1 ]τ−→ c[C2 [b[N | out f | open e.out e]] | O]
⇒ c[C3 [out f | open e.out e] | O]
By composing with the context _ | g[out c] | b[open e], it follows easily from
Lemma 3 and the equivalence of the ambients c[C1 [b[N | out f | open e.out e]] | O]
and c[C3 [out f | open e.out e] | O] thatc[C1 [b[N | out f | open e.out e]] | open d](25)

is observable bisimilar toc[C3 [out f | open e.out e] | open d](26)

By applying the localization operator (e) and (f ) to (25) and (26) one immediately
sees that the ambient c[C1 [b[N]] | open d] is observable bisimilar to the ambient
a[in b]c[C3 [0] | open d]. We can now conclude that Q ⇒ −→ C2 [_] andC2 [b[N]] ⇒ C3 [0] R C1 [b[N]]
By using the closure property of ≈obs , it follows that P ≈obs Q implies P ≈ Q. The
implication of the other direction is straightforward by definition.

Theorem 6.4 is significant not only in that it supports the bisimulation equivalence,but also in that its proof implies a property of local observability.
Theorem 6.5 (Local observability) P ≈ Q if and only if C[P] ≈ C[Q] for every
ambient context C[_].
Two processes are bisimilar if and only if they induce bisimilar ambient actions. In
other words, the equivalence of two non-ambients is strong enough to be closed underambient contexts, but weak enough to be deducible from the equivalence on ambients.
The local observability is a strong support to Definition 4.1.

Fair ambients

561

In MA the local observability is a property too simple to be stated. As a matter offact in MA a very strong property is forced upon us by the global open operator:a[P] is equivalent to b[Q] if and only if a = b and P is equivalent to Q.
The above property is not at all a merit. It says that one can not determine the equivalence of two MA ambients by comparing their observable actions. One has to see
through the ambients as it were. For instance a[b[0]] and a[c[0]] are not equivalenteven though neither can perform any observable actions. In the spirit of the observational theory, MA is best seen as a sub-calculus of SA using the embedding mentioned
in Sect. 1.
In FA, a[P] ≈ a[Q] does not necessarily imply P ≈ Q and it may well be thata[P] ≈ b[Q] for a  = b.

7 Barbed bisimulation
By exploring the labeled transition system, one could define in our framework thebarbedness as follows:a[κ]Definition 7.1 P is barbed at a, notation P⇓a, if P ⇒−→ U for some κ and U ora[[out b]]

P ⇒ −→ V for some b and V. A relation R is barbed if PRQ implies P⇓a ⇔ Q⇓afor every a ∈ N .
The barbed bisimulations are then defined in the standard manner.
Definition 7.2 A symmetric relation R on processes is a barbed bisimulation if thefollowing properties hold:
(i)
(ii)

It is barbed and is closed under context;
τIf QRP −→ P then Q ⇒ Q RP for some Q .

The barbed bisimilarity ≈brb is the largest barbed bisimulation.
An observable relation is a barbed relation. It follows then that ≈obs ⊆≈brb . We willrender the studies of the barbed bisimilarity unnecessary by proving that the reverse
inclusion also holds. For that purpose we introduce a weaker form of the observablebisimilarity.
Definition 7.3 A relation R is weakly observable if PRQ ⇒ (P⇓ ⇔ Q⇓).
Definition 7.4 A symmetric binary relation R is a weak observable bisimulation if thefollowing properties hold:
(i)
(ii)

It is weakly observable and is closed under context;
τIf QRP −→ P then Q ⇒ Q RP for some Q .

The weak observable bisimilarity ≈wob is the largest weak observable bisimulation.
The barbed bisimilarity lies between the observable bisimilarity and the weakobservable bisimilarity.
Lemma 6 ≈obs ⊆≈brb ⊆≈wob .

562

Y. Fu

Proof Suppose P ≈brb Q and P⇓λ. If λ is a[κ] or a[[out b]] then P⇓a. If λ is κ or[out a] then c[P]⇓c. It follows from P ≈brb Q and c[P] ≈brb c[Q] that either Q⇓a orc[Q]⇓c. Hence Q⇓λ for some λ . So ≈brb is a weak observable bisimulation.

The lemma is not just formally interesting. For us it suggests that more attention
should be paid to ≈obs and ≈wob than to ≈brb . The equivalence ≈obs makes very good
sense in the observation theory. The relation ≈wob looks much weaker. However wehave the following result.
Theorem 7.5 ≈wob is the same as ≈obs .
λx be the free names in P | Q and let
Proof Suppose P ≈wob Q and P ⇒−→ U. Let d, e be fresh. The idea of the proof is to find a context C[_] of the form (x)(_ | O) suchthat the following conditions are met:––

C[P] ⇓ d[in e] and C[Q] ⇓ d[in e].
C[P] ⇒ P  ⇓ for some P where P has performed the λ action.

It follows from these two conditions and C[P] ≈wob C[Q] that C[Q] ⇒ Q  ⇓ forsome Q , from which one infers that Q must be able to perform a λ action. The proof
is carried out by case analysis:
–
–

a[κ]

λ = κ. Notice that a[P] ≈wob a[Q] by definition and a[P] ⇒−→ U  for some U  .
So this case is subsumed by the following cases.
λ = a[out b]. Let C[_] be the context defined by (x)(_ | b[e[out a.in d]] | d[in e]).
ττx)(U | e[in d] | d[in e]) −→ (x)U must be simuThen the reductions C[P] ⇒ (τ–a[out b]lated by C[Q] ⇒ (x)V for some V such that Q ⇒ V.
λ = a[[out b]]. Let C[_] be the context (x)(_ | b[out a.in d] | d[in b | in e]). Observeτthat C[P] ⇒ (x)(U | b[d[in e]])  ⇓. Thus
τ(x)(Q | b[out a.in d] | d[in b | in e]) ⇒ Q  ⇓–––for some Q . It is then clear that Q ⇓ a[[out b]].
λ = [out b]. This is subsumed by the previous case.
λ = a[in b]. Use the context C[_] defined below (x)(_ | b[in a.in d] | d[in b | in e]).
λ = a[open b]. Use the context C[_] defined below(x)(_ | b[open a.open d] | d[open b | in e])–

λ = a[in b]. Use the context C[_] defined below(x)(_ | b[in a.out e] | e[out a.in d] | d[in e])–

λ = a[open b]. Use the context C[_] defined below(x)(_ | b[open a.open d] | d[open a | in e])

We conclude that ≈wob is an observable bisimulation.



One interpretation of Theorem 7.5 is that there is very little overloading of semantics in the action labels. If two actions are different in syntax, they are different insemantics. In other words distinct actions have distinct impacts on the environments.
If P can perform λ while Q can not, then they would have different impacts on theenvironments and therefore can be distinguished by the environments.
Theorem 7.5 adds additional weight to the labeled transition semantics.

Fair ambients

563

8 Communication
MA was proposed as a model for mobility. As a computational model MA is Turing
complete. From a programming point of view, the capacity to express the Turing computability is one thing, the ability to support particular computing structures or evenprogramming methodologies is another issue. In MA all computations are interpreted
in terms of ambient mobility. This is fine if one thinks of MA as a basic model formobility. A different attitude is to regard MA as providing an open framework to
support the computing mobility of all shapes and forms. The open-ended view is whata programming practitioner tends to adopt.
A well studied programming paradigm is the functional one. Both the λ-terms andthe π-processes are functional programs reincarnated in different frameworks. Cardelli and Gordon have looked at the functional applications, or communications, in
MA. They introduced two new forms of processes. One is (x).P, which can instantiate
the bound name x by a received name, say y, and then evolves as P{y/x}. Another is xthat may release the name x to whoever wants it before terminating. Computations ofthese new processes are basically the functional applications in a concurrent fashion.
The reduction rule is the following:(x).P | y −→ P{y/x}(27)where P{y/x} is obtained from P by replacing x by y throughout P. One criticism to (27)is that there is no way to tie up the two interacting parties. In the process (x).P | y | z
for example it is completely nondeterministic which name (x).P is going to receive. In
λ-calculus the terms M, N in MN are tightly coupled. In π-calculus one could specify
a particular name to channel the interaction as in (a)(a(x).P | ay.Q). In MA the only
control over communications is that two communicating processes must be in one
ambient.
In this section we study the functional computation in the framework of FA. We
shall stick to the three principles advocated in Sect. 1. The reduction defined in (27)
has to be rejected since the interactions are not between two ambients. So we abandon
the view that communications are local actions. As alternatives we propose two newcapabilities that induce the interactions of ambients.
––

The input capability a(x) introduces processes of the form a(x).P. This is the process that is able to receive a name, say y, from ambient a, instantiates the boundname x by y, and then proceeds as P{y/x}.
The output capability ax introduces processes of the form ax.P. The process ax.P
is capable of releasing the name x to ambient a and then continues as P.

Like the other capability operators, the interactional behaviors of the new capability
operators can only be invoked from within ambients. The functional interactions they
define are as follows:τa[L | b(x).P] | b[N | ay.Q] −→ a[L | P{y/x}] | b[N | Q]
τa[b(x).P] | b[(y)ay.Q] −→ (y)(a[P{y/x}] | b[Q])
The syntax and the semantics of the functional aspects of FA are prescribed inFig. 2. The extended language will be called functional FA. In the rules the symbol α
ranges over the set N ∪ {a | a ∈ N }. The name x in a(x).P is bound. The input operator
a(x). introduces dummy names, whereas the restriction operator (x) introduces local

564

Y. Fu

Fig. 2 Functional FA

names. Both are bound names. The notation bn(P) stands for the set of bound names
in P; and fn(P) denotes the set of free, or non-bound, names in P. We shall abbreviate(x)ax.P to a(x).P. When x  ∈ fn(P), we write α.P for α(x).P.
The labeled transition system introduces six new kinds of labels. The intended
meanings of these labels are as follows:
–
–
–
–
–
–

“ax” reads “import the name x from a”.
“ax” reads “export the name x to a”.
“a(x)” reads “export the bound name x to a”.
“a[bx]” reads “ambient a imports the name x from ambient b”.
“a[bx]” reads “ambient a exports the name x to ambient b”.
“(x)a[bx]” reads “ambient a exports the bound name x to ambient b”.

The actions denoted by these new labels will be called functional actions. Accordingly
the new capabilities will be called functional capabilities.
The functional capability provides a simple mechanism to synchronize the concurrent computations of ambients in the following manner:τa[b.P] | b[a.Q] −→ a[P] | b[Q]A special case of the above synchronization isτ

a[a.P] | a[a.Q] −→ a[P] | a[Q]The ambient a[a.P] is almost like the CCS process a.P. It will be clear in the next
section that CCS can be embedded into the functional FA.
8.1 More examples
Three examples are given in this subsection to demonstrate the expressiveness ofthe communications between ambients. A more fundamental example illustrating theexpressive power of the functional FA will be given in the next section.

Fair ambients

565

Example 11 Using the functional capabilities, the transportation of resources fromone ambient to another ambient can be made more secure as in the following example:a[N | (v)bv.v[out b.open b.P]] | b[a(x).out a.open x.Q]τ−→ (v)(a[N | v[out b.open b.P]] | b[out a.open v.Q])τ−→ (v)(v[open b.P] | a[N] | b[open v.Q])τ−→ (v)(a[N] | b[P | Q])
The communication of a local name makes sure that an ambient will not choose awrong target in the middle of the movement from one ambient to another.

Example 12 Using the functional capability one could give a much better modelingof the firewall protocol defined in Example 9. An agent intends to upload a piece ofresource to a host. The host is protected by a firewall. The two are defined as follows:defFirewall = (fw)(b)fw[K0 | b(y).open y | F]
def

Agent = (kag )(c)ag[K1 | V | c(f ).open f | r[R]]
where
def

K0 = k0 [out.k1 (k).k[out.k1 (n).k1 (z).nz.out n.kag (c).X]]
def

X = b[out.fwn] | c[out.nfw]
def

K1 = k1 [out.k0 (k).kag.kkag .c[out.agk]]def

V = c(k).k(z).(v)(kag [v.out k.kc] | v[z])Let Sys be the system Firewall | Agent. The system Sys can engage in a sequence oftalks between its two subsystems:τSys −→∗ (fw)(b)(fw[. . .] | k0 [k1 (k). . . .]) | (kag )(c)(ag[. . .] | k1 [k0 (k). . . .])τ−→ (k)((fw)(b)(fw[. . .] | k0 [k[out. . . .]]) | (kag )(c)(ag[. . .] | k1 [kag. . . .]))τ−→ (k)((fw)(b)(fw[. . .] | k[k1 (n). . . .]) | (kag )(c)(ag[. . .] | k1 [kag. . . .]))τ−→ (k)((fw)(b)(fw[. . .] | k[k1 (z). . . .]) | (kag )(c)(ag[. . .] | k1 [kkag . . . .]))τ−→ (k)(kag )((fw)(b)(fw[. . .] | k[agkag . . . .]) | (c)(ag[. . .] | k1 [c[out.agk]]))τ−→ (k)(kag )((fw)(b)(fw[. . .] | k[agkag . . . .]) | (c)(ag[c(k). . . .] | c[agk]))τ−→ (k)(kag )((fw)(b)(fw[. . .] | k[agkag . . . .]) | (c)ag[k(z). . . .])τ−→ (k)(kag )(. . . | (c)(ag[(v)(kag [v.out k.kc] | v[kag ]) | . . .])τ−→ (k)(kag )((fw)(b)(fw[. . .] | k[out ag. . . .]) | (c)(ag[kag [out k.kc] | . . .])τ−→ (k)(kag )((fw)(b)(fw[. . .] | k[kag (c).X]) | (c)(kag [kc] | ag[. . .]))τ−→ (k)(fw)(b)(c)(fw[. . .] | k[b[out.fwag] | c[out.agfw]] | ag[. . .])τ−→∗ (fw)(b)(c)(fw[b(y).open y | F] | b[fwag] | c[agfw] | ag[c(f ).open f | r[R]])τ−→∗ (fw)(fw[open ag | F] | ag[open fw.r[R]])τ−→ (fw)fw[r[R] | F]

566

Y. Fu

For the agent to successfully upload the resource r[R] to the anonymous ambient, it
has to pass a sequence of authentications:
1.

2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.

The protected ambient fw releases an fw-envoy with the key k0 ; the agent ag
releases an ag-envoy with the key k1 ; The pair k0 , k1 of keys are used to initiate
an negotiation;
The envoys, who know each other’s keys, establish a link with a secret key k;
The fw-envoy starts to use the secret key k for further communication with theag-envoy;
The fw-envoy receives the name of the agent from the ag-envoy;
The fw-envoy receives a secret key kag of the agent from the ag-envoy;
The ag-envoy discards the key k1 ;The agent ag receives the secret key k;
The fw-envoy sends the secret key kag , received from the ag-envoy, back to theagent;
The agent verifies the received key kag ;After the successful verification, the agent signals this message to the fw-envoy;
Then the personal key of the agent is used to pass the password of the agent to
the fw-envoy;
The fw-envoy releases two subenvoys and dissolves itself;
The subenvoys establish a direct link between the protected host and the agent;
Finally the transmission of the resource can happen.

The purpose of this example is to explain how communications between ambients canbe explored to specify protocols.

Example 13 (Signal transduction) Signal transduction at the cellular level refers to
the movement of signals from outside the cell to inside. The movement of signals canbe simple. Upon ligand interaction, a cell would open a channel to allow signals to
be passed in the form of small ion movement, either into or out of the cell. Theseion movements result in changes in the electrical potential of the cells that, in turn,propagates the signal along the cell. The following describes a situation when an ion,as a signal, enters a cell:τEnv | Cell | Ion −→ env[P1 ] | cell[in ion.P2 | ligand[out env | P3 ] | P4 ] | ion[in cell | P5 ]τ−→ env[P1 ] | cell[P2 | ligand[out env | P3 ] | P4 | ion[P5 ]]
where
def

Env = env[celllingand.P1 ]Cell = cell[env(ligand).(in ion.P2 | ligand[out env | P3 ]) | P4 ]def
def

Ion = ion[in cell | P5 ]This example makes use of a global communication between two ambients.



8.2 Observational theory
In the rest of this section we shall focus on the observational theory of FA. Let κ range
over the extended set of capabilities and λ over the extended set of labels. If we simply

Fair ambients

567

modify Definition 4.1 by replacing the third clause by the following requirement:λIf P −→ P and λ is a label in the following set{a[out b], a[[out b]], a[bx], a[bx], (x)a[bx] | a, b ∈ N }λthen Q ⇒ Q RP for some Q .
We would get an equivalence relation for the functional ambients. But it fails to
be a congruence. This is obvious for people familiar with the π-calculus. The process (a)(a[in x] | b[in a.out x]) is bisimilar to 0 in the sense of Definition 4.1. Howeverd(x).(a)(a[in x] | b[in a.out x]) is not bisimilar to d(x).0. In the literature on π-calculus
several bisimulation congruence relations have been proposed. In our opinion themost attractive bisimulation congruence is the open bisimilarity of Sangiorgi [37].
For some special π-processes the open bisimilarity is too strong to be reasonablefrom an observational viewpoint. A rectified version, the quasi open bisimilarity, is
proposed by Sangiorgi and Walker [40] and further studied by Fu [15]. The reader
is advised to consult [40,15] for more information. Appendix C summarizes somerelevant definitions and results on the quasi open bisimulations of the π-calculus.
Before defining bisimulations for the functional FA, some notations have to be
fixed. A substitution σ of name, or simply substitution, is a map from N to N suchthat the set {x | x  = σ (x)} is finite. The set of substitutions will be ranged over by σ .
We write Pσ for the result of applying σ to P. The finite subset relation is denotedby ⊆f .
A well known difficulty for bisimulations on the π-processes is how to define thesimulations for the bound output actions. In functional FA, the question is how toa(x)(x)a[bx]

simulate P −→ P and P −→ P . The caution must be paid not to confuse thename x in P with any other free names. Now if bisimulations are closed under allenvironments, they must also be closed under substitution of names. That suggeststhat some mechanism should be designed that only admits substitutions that respect
local names. The motto is that we treat the local names as if they were free names, but
we have to respect them. This is why we need the following definition.
Definition 8.1 A substitution σ respects 
x if ∀x ∈ 
x.xσ = x and ∀y  ∈ x.yσ  ∈ x.
Another important issue is how to make sure that bisimulations for the functional
FA give rise to a congruence relation. A congruence is a relation closed under allcontexts. Now for functional FA the contexts are redefined to take into account thefunctional capability:––

A context defined in Definition 2.1 is an open context;
If C[_] is an open context then a(x).C[_] and ax.C[_] are open contexts.

The observable bisimilarity, the barbed bismilarity and the weak observable bisimilarity for the functional FA are defined by replacing the phrase “context” in Definition 6.3, Definition 7.2 and Definition 7.4 respectively by the phrase “open context”.
fff
We write ≈obs , ≈brb and ≈wob for the three respective bisimilarities on the functional
FA processes.
For the counterpart of Definition 4.1 in the functional FA one can not simply
require that bisimulations are closed under contexts since that would defeat the definition. Closure under the functional capabilities implies the closure of substitutionsof names. This brings us to Sangiorgi’s open approach.

568

Y. Fu

The above discussions lead us to combine Definition 4.1 with the definition of thequasi open bisimulations of the π-calculus for the purpose of defining a bisimulationequivalence for the functional FA.
Definition 8.2 A family of symmetric relations {Rz }z⊆f N on processes is an openz then Pσ Rz Qσ and the followings
bisimulation if whenever PRz Q and σ respects 
hold:
τ

1.
2.

If P −→ P then Q ⇒ Q Rz P for some Q .
κκ
If P −→ P and κ is not of the form a(x), then Q ⇒ Q Rz P for some Q .

3.

If P −→ P then Q ⇒ Q Rzx P for some Q .

4.

If P −→ P and λ is a label in the following set

a(x)

a(x)

λ

{a[out b], a[[out b]], a[bx], a[bx] | a, b ∈ N }λthen Q ⇒ Q Rz P for some Q .
5.
6.

(x)a[bx]

If P −→ P then Q[out a]If P −→(x)a[bx]⇒ Q Rzx P for some Q .

(m)AP then for every name d and every process O satisfying[out a]n)BQ and{
m} ∩ fn(O) = ∅ there exist some n, B, Q , Q such that Q ⇒ −→ (

z



(
n)(B | d[Q | O]) ⇒ Q R (m)(A | d[P | O]).
7.

a[in b]If P −→ (m)AP then for every process O satisfying {m} ∩ fn(O) = ∅ there
a[in b]n)BQ and (n)(Q | b[B | O]) ⇒exist some n, B, Q , Q such that Q ⇒ −→ (Q Rz (m)(P | b[A | O]).
8.

a[open b]

If P −→ (m)MP then for every process O satisfying {m} ∩ fn(O) = ∅ somen, N, Q , Q exist such that Q
Q Rz (m)(P | b[M | O]).

9.

a[open b]⇒ −→(n)NQ and (n)(Q | b[N | O])⇒a[in b]If P −→ C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist somea[in b]C [_], Q such that Q ⇒ −→ C [_] and C [b[N]] ⇒ Q Rz C[b[N]].
10.

If P

a[open b]−→

C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist

some C [_], Q such that Q

a[open b]⇒ −→ C [_] and C [N] ⇒ Q Rz C[N].

We write {≈z }z⊆f N for the largest open bisimulation and refer to ≈z as the openz-bisimilarity. The open bisimilarity ≈opn is the open ∅-bisimilarity ≈∅ .
f

In Definition 8.2 the clause 3 calls for a little explanation. Now PRz Q means that
P and Q are equivalent under the assumption that z are distinct names that must be
kept distinct from the other names. This is a reasonable assumption if z were local
names that have been opened up by restricted output actions. After both P and Q
open up the local name x, it must be kept distinct in further comparison since inreality environments can have absolutely no effects on x. That’s why we require thatP Rzx Q . The same intuition is behind clause 5.
The open bisimilarity is a congruent equivalence, the proof of which can be foundin Appendix B.
f

Proposition 8.3 The equivalence ≈opn is congruent.

Fair ambients569

The observational theory of the functional FA calls for some technical lemmas,
some of which are stated below. The proofs of these lemmas are straightforward
applications of the Bisimulation lemma.
fLemma 7 Suppose (x)(P | a[bx]) ≈obs (x)(Q | a[bx]) for distinct names a and b. If eitherfa or b is fresh then (x)(P | c[dx]) ≈obs (x)(Q | c[dx]) for arbitrarily distinct fresh namesc, d.
Proof For fresh c, d, one has that(x)(P | a[bx]) | b[a(z).cz] | c[b(z).dz] ⇒ (x)(P | c[dx])fNow (x)(P | c[dx]) ≈obs (x)(Q | c[dx]) follows by standard argument using Bisimulation lemma.
fLemma 8 If (x)(P | a[bx]) ≈obs (x)(Q | a[bx]) for distinct fresh names a and b, thenf(x)P ≈obs (x)Q.

Proof Use the context _ | b[a(z)] to consume the ambient a[bx].

Lemma 9 (x)(y)(P | a[bx] | c[dx] | e[f y]) and (x)(y)(Q | a[bx] | c[dy] | e[f y]) are notbisimilar if a, b, c, d, e, f are fresh and pairwise distinct.
Proof The context _ | d[c(z).f z] | f [e(z).d(v).(z | v.f )] is able to observe the difference
between the two processes.
Corollary 8.4 If a, b, c, d are fresh and pairwise distinct then (x)(Q | a[bx] | c[dx]) is notbisimilar to (x)(y)(P | a[bx] | c[dy]).
Proof The non-equivalence follows immediately from Lemmas 8 and 9.
fCorollary 8.5 (x)(P | a[bx])  ≈obs Q | a[by] if a, b are fresh and distinct.
ff

Proof Had (x)(P | a[bx]) ≈obs Q | a[by] been held, then (x)(y)(P | a[bx] | c[dy]) ≈obs(y)(Q | a[by] | c[dy]) would have been held for fresh c, d, which would contradict toCorollary 8.4.
The proof of the next result is omitted since it is similar to the proof of Lemma 5.
We remark that the property is stable under substitution of name.
Lemma 10 Suppose d, a1 , . . . , an , b1 , . . . , bn are fresh and pairwise distinct names. If
the ambient (x1 , . . . , xn )(c[P | open d] | a1 [b1 x1 ] | . . . | an [bn xn ]) is observable bisimilar
to the ambient (x1 , . . . , xn )(c[Q | open d] | a1 [b1 x1 ] | . . . | an [bn xn ]), then(x1 , . . . , xn )(C[P] | a1 [b1 x1 ] | . . . | an [bn xn ])is observable bisimilar to the ambient (x1 , . . . , xn )(C[Q] | a1 [b1 x1 ] | . . . | an [bn xn ]) for
every ambient context C[_] that does not contain a1 , . . . , an , b1 , . . . , bn .
We are now ready to prove that the bisimilarities we introduced for FA also coincidein the functional FA. The following theorem states a special Local Observability.

570

Y. Fu

Theorem 8.6 Suppose d, a1 , . . . , an , b1 , . . . , bn are fresh names that are pairwise distinct. If (x1 , . . . , xn )(c[P | open d] | a1 [b1 x1 ] | . . . | an [bn xn ]) is observable bisimilar tof(x1 , . . . , xn )(c[Q | open d] | a1 [b1 x1 ] | . . . | an [bn xn ]), then P ≈opn Q.
x = x1 , . . . , xn , is defined
Proof Let {Rx }x⊆f N be the family of relations where Rx , forby the following relation

⎫
⎧
 (
⎪
 x)(c[P | open d] | a1 [bf1 x1 ] | . . . | an [bn xn ]) ⎪
⎪
⎪
⎪
⎪

⎪
⎪
⎬
⎨
≈obs


(P, Q)  (x)(c[Q
|
open
d]
|
a
[b
x
]
|
.
.
.
|
a
[b
x
])
n
n
n
1
1
1
⎪
 where d, a , . . . , a , b , . . . , b are fresh ⎪
⎪
⎪
⎪
⎪

⎪
⎪
n 1
n
1
⎭
⎩
 and pairwise distinct, and x = x1 , . . . , xn
Using Lemma 7 it is easy to show that the family {Rx }x⊆f N is closed under substitutionsin the sense that if PRx Q and σ respects x then Pσ Rx Qσ . This observation reducesxthe complexity of the proof that {R }x⊆f N is an open bisimulation. Now supposeλQ Rx P −→ P . To avoid long expressions, we introduce the following abbreviations:defx)(c[P | open d] | a1 [b1 x1 ] | . . . | an [bn xn ])A = (
x)(c[P | open d] | a1 [b1 x1 ] | . . . | an [bn xn ])A = (def

defx)(c[Q | open d] | a1 [b1 x1 ] | . . . | an [bn xn ])B = (
It follows from Lemmas 7 and 10 and the fact A ≈obs B that C[P]Rx C[Q] for every
ambient context C[_]. We will carry out a case analysis for the functional actions.
f––

λ = ax. This case is simple.
λ = a(x). Then for fresh e, k, one has that
τA | a[c(z).out k.ez] | k[k[out a]] ⇒ (x)(A | a[ex])τThus B | a[c(z).out k.ez] | k[k[out a]] ⇒ N and N ≈obs (x)(A | a[ex]) for some N.
By Corollary 8.5, N can not be of the form B | a[ev] for some free v. So N is of
the form (x)(B | a[ex]) for some B . It follows from Lemma 7 thatf(x)(A | a [b x]) ≈obs (x)(B | a [b x])
f

a(x)

–
–

for fresh a , b . Thus Q ⇒ Q Rxx P .
λ = ax and x  ∈ 
x. The proof is similar.
λ = axi . Then for fresh e, k, one has that
τA | a[c(z).out k.ez] | k[k[out a]] ⇒ (xi )(A | a[exi ])By Corollary 8.5 the reductions can not be simulated by
B | a[c(z).out k.ez] | k[k[out a]] ⇒ L | a[ew]for some free w. By Corollary 8.4 the reductions can not be simulated by
B | a[c(z).out k.ez] | k[k[out a]]⇒ (y)(x)(c[Q1 | open d] | a1 [b1 x1 ] | . . . | an [bn xn ] | a[ey])Fair ambients571

for some local y. By Lemma 9 the reductions can not be simulated by
B | a[c(z).out k.ez] | k[k[out a]]⇒ (x)(c[Q2 | open d] | a1 [b1 x1 ] | . . . | an [bn xn ] | a[exj ])for some j  = i. It follows that the reductions can only be simulated by
B | a[c(z).out k.ez] | k[k[out a]]⇒ (x)(c[Q | open d] | a1 [b1 x1 ] | . . . | an [bn xn ] | a[exi ])ax–iQ Rx P .
for some Q . It then follows from Lemmas 7 and 8 that Q ⇒
λ = b[ax]. Let C[_] be the context (x)(C [_] | a1 [b1 x1 ] | . . . | an [bn xn ]) | e[out c],ττwhere C [_] is c[_ | a[bx.out e] | open d] and e is fresh. Now C[P] −→−→ A mustτ
be simulated by C[Q] ⇒ (x)(c[Q | open d] | a1 [b1 x1 ] | . . . | an [bn xn ]) in such a

b[ax]

–

way that Q ⇒ Q Rx P .
λ = b[ax] and x  ∈ 
x. Let C[_] be defined by(x)(C [_] | a1 [b1 x1 ] | . . . | an [bn xn ]) | e[out c.out a | x]
where C [_] is c[_ | a[b(z).out e.z[out e.e]] | open d] and e is fresh. Now
τC[P] −→ (x)(c[P | a[out e.x[out e.e]] | open d] | . . .
τ−→ (x)(c[P | open d] | a[x[out e.e]] | . . .) | e[out a | x]τ−→ (x)(c[P | open d] | x[e] | . . .) | e[x]τ−→ (x)(c[P | open d] | a1 [b1 x1 ] | . . . | an [bn xn ])τmust be simulated by C[Q] −→ (x)(c[Q | open d] | a1 [b1 x1 ] | . . . | an [bn xn ]). Thus
b[ax]

–

Q ⇒ Q Rx P .
λ = (y)b[ay]. Let the context C[_] be defined by(x)(C [_] | a1 [b1 x1 ] | . . . | an [bn xn ]) | e[out c | out a]
where C [_] is c[_ | a[b(z).out e.k[out e.hz]] | open d] and e, h, k are fresh. We havethe following similar reductions:τC[P] −→ (x)(y)(c[P | a[out e.k[out e.hy]] | open d] | . . .
τ−→ (x)(y)(c[P | open d] | a[k[out e.hy]] | . . .) | e[out a]τ−→ (x)(y)(c[P | open d] | k[hy] | a1 [b1 x1 ] | . . . | an [bn xn ])The reduction must take the following form
C[Q] ⇒ (x)(y)(c[Q | open d] | k[hy] | a1 [b1 x1 ] | . . . | an [bn xn ])–According to Corollary 8.4 the local name z is distinct from any of x1 , . . . , xn .
λ = b[axi ]. Let the context C[_] be defined by(x)(C [_] | a1 [b1 x1 ] | . . . | an [bn xn ]) | e[out c | out a]
where C [_] is c[_ | a[b(z).out e.k[out e.hz]] | open d] and e, h, k are fresh. Then theargument is similar to the one in the previous case.

We conclude that {Rx }x⊆f N is an open bisimulation.



572

Y. Fu

Theorem 8.6 is significant in that it justifies Definition 8.2 by supporting thefollowing result.
f

f

f

f

Theorem 8.7 In the functional FA the equivalence relations ≈opn , ≈obs , ≈brb and ≈wob
are the same.
ff

Proof The inclusion ≈opn ⊆≈obs follows from Proposition 8.3 and the inclusion

f
f
f
f
f
≈obs ⊆≈opn follows from Theorem 8.6. The proofs of ≈obs =≈brb =≈wob are almostfthe same as the ones given in Sect. 7. The idea is to show that ≈wob is contained inf≈obs . The extra work is to do with the functional capabilities. Suppose for examplea(x)f
x be the free names in P | Q and d, e be fresh names.
that Q ≈wob P −→ P . Let f
Let C[_] be (x)(a[_] | a[a(z).open e.dz] | e[open a.e] | e[e]). By the definition of ≈wob ,x)(x)(a[Q ] | e[dx])C[P] ⇒ (x)(x)(a[P ] | e[dx]) has to be simulated by C[Q] ⇒ (for some Q or by C[Q] ⇒ (x)(a[Q ] | e[dy]) for some Q and y ∈ 
x. Using similararguments as in the proofs of Corollaries 8.4 and 8.5, one can rule out the possibilityof the reductions C[Q] ⇒ (x)(a[Q ] | e[dy]) as a simulation. Thus Q ⇓ a(x).

f

f

f

f

We will write ≈f for any of ≈opn , ≈obs , ≈brb and ≈wob and we will simply read“P ≈f Q” as “P is bisimilar to Q”.
Corollary 8.8 (Local observability) For functional FA processes P, Q it holds thatP ≈f Q if and only if C[P] ≈f C[Q] for every ambient context C[_].

9 Pi as a subcalculus of FA
The λ-calculus [2] is an operational model of the functional programming. It has beenused as a test bed for the descriptive power of a computing model. Milner has given
in [27] a translation that relates the λ-calculus and the π-calculus. More precisely
Milner’s translation interprets the β-reduction of the lazy λ-calculus [1] by the communication of the π-calculus. At the semantic level, the force of the translation iswitnessed by the full abstraction result proved by Sangiorgi [36], which states that two
λ-terms are open applicative bisimilar if and only if their translations are bisimilar as
π-processes.
We prove in this section that the lazy λ-calculus can also be embedded in the functional FA. We shall establish this fact by showing that the π-calculus is a sub-calculusof the functional FA. The syntax and the semantics of the π-calculus is formulated
in Fig. 3. This variant of the π-calculus has all the machinery to code up the lazy
λ-calculus.
We need to define a map [[_]] that translates a π-process to an FA system. The cruxof the matter is how to interpret the π-processes with the input/output prefixes. Using
the terminologies of the functional FA, one can read the π-process a(x).P as ‘an ambient that receives a name from ambient a before continuing as P’, and the π-process
ay.Q as ‘an ambient that sends the name y to ambient a before continuing as Q’. Thissuggests to define [[a(x).P]] by a[a(x).[[P]]] and [[ay.Q]] by a[ay.[[Q]]]. Unfortunately
this straightforward translation does not work. The communication would have beenmodeled by the following reduction:
τa[a(x).[[P]]] | a[ay.[[Q]]] −→ a[[[P{y/x}]]] | a[[[Q]]]Fair ambients

573

Fig. 3 The π -calculus

It is clear that the system on the right hand side is wrong since the two translations
stay inside a. Ideally the right hand side should be [[P{y/x}]] | [[Q]]. The unsuccessfulattempt leads us to define the translation in such a way that things can be pulled out
after a communication has been simulated. We first define an auxiliary translation
relative to a fresh name u:def[[0]]u = 0
def[[a(x).P]]u = (v)(a[out u.v.a(x).[[P]]v ] | v[out u.a.!out a])def[[ay.Q]]u = (v)(a[out u.v.ay.[[Q]]v ] | v[out u.a.!out a])def[[P | Q]]u = [[P]]u | [[Q]]udef[[(x)P]]u = (x)[[P]]udef[[!a(x).P]]u = (v)(a[out u.v.!a(x).[[P]]v ] | v[out u.a.!out a])
Intuitively the name u in the above translation is a handle that can be used to pullout the translations as it were from the surrounding ambients. In the definition of[[a(x).P]]u the two ambients a[out u.v.a(x).[[P]]v ] and v[out u.a.!out a] must both bepulled out and synchronize before a[out u.v.a(x).[[P]]v ] can interact with anybody. The
translation would be correct, and even more concise, without the synchronization.
But the current translation is easy to reason about. Using the auxiliary definition, we
can formally define the translation as follows:def[[0]] = 0
def[[a(x).P]] = (v)(a[a(x).[[P]]v ] | v[!out a])def[[ay.Q]] = (v)(a[ay.[[Q]]v ] | v[!out a])def[[P | Q]] = [[P]] | [[Q]]def[[(x)P]] = (x)[[P]]def[[!a(x).P]] = (v)(a[!a(x).[[P]]v ] | v[!out a])
The encoding is not only structural, it is also stable in the sense of the following lemma,
the proof of which is a simple structural induction.
Lemma 11 [[P]]σ ≡ [[Pσ ]] and [[P]]v σ ≡ [[Pσ ]]v if v  ∈ n(σ ).

574

Y. Fu

The stability is a necessary condition for the translation to behave properly on the
input prefix processes.
Let’s see how to model communications in the functional FA. The interpretationof a(x).P | ay.Q simulates the π-communication in the very first step:τ[[a(x).P | ay.Q]] −→ (v)(a[[[P{y/x}]]v ] | v[!out a]) | (w)(a[[[Q]]w ] | w[!out a])
If P{y/x} can not perform any observable actions, then it is bisimilar to 0. In this case(v)(a[[[P{y/x}]]v ] | v[!out a]) is bisimilar to 0. If P{y/x} is of the form b(z).P thenτττ(v)(a[[[P{y/x}]]v ] | v[!out a]) −→−→−→∼ [[P{y/x}]]
In other words, [[P{y/x}]]v must come out of a before it can simulate b(z).P . This is
the general idea of the translation.
By definition the translation [[P]] of a π-process P, and all its descendants can only
perform four kinds of actions, the τ -actions, actions of the form a[ax], actions of theform a[ax], and actions of the form (x)a[ax]. These correspond respectively to the fourkinds of the actions of the π-calculus.
The first step to understand the translation is to prove the following lemmas.
Lemma 12 Suppose the only possible observable actions O can perform are either[out v] or functional actions. Then the two processes in the following reductionτ(v)(a[b[out v.P] | O] | v[!out a]) −→ (v)(b[P] | a[O] | v[!out a])are bisimilar. Moreover an action of (v)(a[b[out v.P] | O] | v[!out a]) can be simulatedby (v)(b[P] | a[O] | v[!out a]) in no more than one action step.
Proof By assumption it is clear thatτ(v)(a[b[out v.P] | O] | v[!out a]) −→ (v)(b[P] | a[O] | v[!out a])
Now there is no interactions between b[out v.P] and O. And every action of(v)(b[P] | a[O] | v[!out a])can be simulated by the same action of (v)(a[b[out v.P] | O] | v[!out a]). On the other
hand, if (v)(a[b[out v.P] | O] | v[!out a]) performs an action caused by b[out v.P], thenthe action can be simulated by (v)(b[P] | a[O] | v[!out a]) vacuously. If(v)(a[b[out v.P] | O] | v[!out a])performs an action caused by O then (v)(b[P] | a[O] | v[!out a]) can do the sameaction.

Lemma 13 Suppose P is a π-process and the only possible observable actions O canperform are either [out v] or functional actions. Then some P exists such that(v)(a[[[P]]v | O] | v[!out a]) ⇒ P ∼ [[P]] | (v)(a[O] | v[!out a])and (v)(a[[[P]]v | O] | v[!out a]) is bisimilar to [[P]] | (v)(a[O] | v[!out a]).
Proof The proof is carried out by structural induction.

Fair ambients

575

P is b(x).P . Then [[P]]v is (w)(b[out v.w.b(x).[[P ]]w ] | w[out v.b.!out b]). It is clear
that

–

τ

(v)(a[[[P]]v | O] | v[!out a])−→ (v)((w)(b[w.b(x).[[P ]]w ] | a[w[out v.b.!out b] | O]) | v[!out a])τ−→ (v)((w)(b[w.b(x).[[P ]]w ] | w[b.!out b]) | a[O] | v[!out a])τ−→ (v)((w)(b[b(x).[[P ]]w ] | w[!out b]) | a[O] | v[!out a])τ−→ [[P]] | (v)(a[O] | v[!out a])
One gets the equivalence between the first and the third processes by applying
Lemma 12 to the first two reductions. Notice that the only action the system(w)(b[w.b(x).[[P ]]w ] | w[b.!out b]) can perform is the tau action. Therefore it has
to be bisimilar to (w)(b[b(x).[[P ]]w ] | w[!out b]).
P is by.P or !b(x).P . The arguments are similar.
P is (x)P or P | P . In these cases we resort to the induction hypothesis.
P is 0. This case is easy.

–
–
–



This completes the proof.

Lemma 13 is useful since it relates [[P]]v to [[P]], both operationally and observationally.
The second step is to prove that the translation preserves the operational semantics.
Proposition 9.1 (Preservation) The translation [[_]] preserves the operational semantics
in the following sense:
τ

τ

ax

a[ax]

ax

a[ax]

a(x)

(x)a[ax](i)

If P −→ P then [[P]] −→ ⇒∼ [[P ]];(ii)

If P −→ P then [[P]] −→ ⇒∼ [[P ]];(iii)

If P −→ P then [[P]] −→ ⇒∼ [[P ]];(iv)

If P −→ P then [[P]] −→⇒∼ [[P ]].

Proof The proof is carried out by induction on the derivations of reduction. The basecase is when P is of the form a(x).P , or ax.P or !a(x).P . Take for instance the process!a(x).P . By Lemma 13[[!a(x).P ]]≡(v)(a[!a(x).[[P ]]v ] | v[!out a])a[ay]−→ (v)(a[[[P {y/x}]]v | !a(x).[[P ]]v ] | v[!out a])⇒∼ [[P {y/x}]] | [[!a(x).P ]]≡[[P {y/x} | !a(x).P ]]The other cases are also simple.



As a matter of fact the translation is better than what is stated in Proposition 9.1.
It actually reflects the operational semantics.
Proposition 9.2 (Reflection) The translation [[_]] reflects the operational semantics inthe following sense:

576

Y. Fu

(i)

If [[P]] −→ S then P −→ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]];(ii)

If [[P]] −→ S then P −→ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]];(iii)

If [[P]] −→ S then P −→ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]];(iv)

If [[P]] −→ S then P −→ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]].

τ

τ

a[ax]

ax

a[ax]

ax

(x)a[ax]a(x)τProof The proof is carried out by mutual structural induction. Suppose [[P]] −→ S.
Obviously P can be neither a prefix operation nor a replication. If P ≡ (x)P thenτS ≡ (x)S and [[P ]] −→ S . We are done by induction hypothesis on (i). If P ≡ P | Pthen there are three cases:τ[[P]] −→ S is caused by a tau action of [[P ]]. We are done by applying the induction
hypothesis on (i).
τ[[P]] −→ S is caused by a tau action of [[P ]]. We are done by applying the induction
hypothesis on (i).
τ[[P]] −→ S is caused by an interaction between [[P ]] and [[P ]]. In this case we canuse the induction hypothesis on (ii), (iii) and (iv).

–
–
–

a[ax]

For another example, suppose [[P]] −→ S. If P ≡ a(z).P thenS ≡ (v)(a[[[P {x/z}]]v ] | v[!out a])
and
a[ax]

[[P]] −→ (v)(a[[[P {x/z}]]v ] | v[!out a]) ⇒∼ [[P {x/z}]]and (v)(a[[[P {x/z}]]v ] | v[!out a]) ≈f [[P {x/z}]] by using Lemma 13. If P is in any otherform then we can simply resort to the induction hypothesis.
The proofs of the other cases are similar.

The next corollary is a more general statement of the reflection property that ismore useful in the reasoning of the bisimulations.
Corollary 9.3 The translation [[_]] reflects the operational semantics in the following
sense:
τ

τ

a[ax]

ax

a[ax]

ax

(x)a[ax]

a(x)

(i)

If [[P]] ⇒ S then P ⇒ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]];(ii)

If [[P]] ⇒ S then P ⇒ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]];(iii)

If [[P]] ⇒ S then P ⇒ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]];(iv)

If [[P]]⇒ S then P ⇒ P for some P such that S ⇒∼ [[P ]] and S ≈f [[P ]].
τProof Suppose [[P]] −→ S1 ⇒ S. By Proposition 9.2 some P exists such thatτP −→ P and S1 ≈f [[P ]]. It follows from Lemma 12 that S1 ⇒ S can be simulatedby [[P ]] ⇒ S ≈f S for some S in such a way that the length of [[P ]] ⇒ S is no
more than the length of S1 ⇒ S. So by induction hypothesis we must have some Pτsuch that P ⇒ P and S ≈f [[P ]]. Conclude that P ⇒ P and S ≈f [[P ]]. Thissuffices to give the general picture of the proof.
Fair ambients

577

The close correspondence between the two operational semantics is only half thestory. It is apparent that the operational correspondence should support an algebraic
correspondence. Therefore the third step is to establish a full abstraction result. In
the following theorem, ≈xπ denotes Sangiorgi and Walker’s quasi open 
x-bisimilarity.
Appendix C reviews some background materials on this equivalence.
Theorem 9.4 (Full abstraction) Suppose P, Q are π-processes. Then P ≈xπ Q if andonly if [[P]] ≈x [[Q]].
Proof Let {Rx }x⊆f N be the family of relations defined byRx = {([[P]], [[Q]]) | P ≈xπ Q in π}
def

Suppose S ≈x Rx ≈x T. Then [[P]], [[Q]] exist such thatS ≈x [[P]] Rx [[Q]] ≈x T(z)a[az]

If S −→ S then [[P]]exists such that P(z)a[az]⇒ L and S ≈xz L for some L. By Corollary 9.3 some Pa(z)⇒ [[P ]] and L ≈ [[P ]]. Since P ≈xπ Q, there must exist⇒ P , La(z)some Q such that Q ⇒ Q ≈xz
π P . By Proposition 9.1, [[Q]]some N. It then follows that TT(z)a[az](z)a[az]⇒ N ∼ [[Q ]] for⇒ T  ≈xz N for some T  . Thus(z)a[az]⇒ T  ≈xz Rxz ≈xz S

The proofs for the other three cases are similar. Conclude that {≈x Rx ≈x }x⊆N is an
open bisimulation. It is then clear that Rx ⊆≈x Rx ≈x ⊆≈x . Thus [[P]] ≈x [[Q]] follows
from P ≈xπ Q.
Let {Sx }x⊆f N be the family of relations defined bySx = {(P, Q) | [[P]] ≈x [[Q]] in functional FA}
def

a(z)

We show that it is a quasi open bisimulation. Suppose that P −→ P in the π-calculus.
(z)a[az]

By Proposition 9.1, one has [[P]] −→ P1⇒∼ [[P ]] and P1 ≈f [[P ]] for some FA

process P1 . It follows that some FA process Q1 exists such that [[Q]](z)a[az]⇒ Q1 ≈xz P1 .

a(z)By Corollary 9.3, some π-process Q exists such that Q ⇒ Q and Q1 ≈f [[Q ]]. Nowa(z)we have [[P ]] ≈xz [[Q ]]. Hence Q ⇒ Q Sxz P . Conclude that {Sx }x⊆f N is a quasiopen bisimulation, which means that P ≈xπ Q follows from [[P]] ≈x [[Q]].
In summary the π-calculus is a sub-calculus of the functional FA. As far as weknow this is the best result so far about the relationship between the π-calculus andthe ambient calculi.
The full abstraction result is established with respect to the open bisimilarity. To
our understanding there is no reason why it can not be proved for other bisimulationequivalences like for instance the early bisimilarity. The details however remain to beverified.
An interesting point about the translation is that, in addition to the functional
capabilities, only the out and co-out capabilities are used. That is to say that from thepoint of view of modeling the π-calculus the in and open capabilities are not necessary.
In our opinion the example shows that the out capability is essential for the ambient

578

Y. Fu

calculi. Without the operator all the ambients can do is to suck ambients, which would
reduce the observability of the ambients considerably.
The translation also suggests that the operational semantics we have chosen forthe out capability is reasonable. The local name u in the definitions of [[a(x).P]]u and[[a(x).P]] for example is crucial. It makes sure that [[P]] can not be interfered by theenvironment in an uncontrolled way. It only does what it is supposed to do. Had weused the semantics defined in (14) we would have haddef[[a(x).P]] = (v)(a[a(x).[[P]]a ] | v[!out a])(28)

The problem with (28) is that the component v[!out a] can interact with the environments, which has to be wrong. We have not been able to work out a sound translation
using (14).

10 Conclusion, related work and further research
The philosophy of FA is that computing with ambients is about transferring computing resources from one place to another. The resources could be anything inside anambient, like an ambient, a process or an interface. The role of the capability operators is to lay down the rules for the transportation of resources. These rules guarantee
the subject reduction property for ambients. The investigation of the paper has comeup with results that support our computing mechanism. Three aspects are particularly
worth mentioning:
1.

2.

3.

The operational semantics is cleanly defined by a pure labeled transition system
and is subject to the standard bisimulation studies. The simplicity of the operational semantics is largely due to the design principles we set up for FA. On theother hand, the operational simplicity reinforces the principles we proposed forthe ambients. The most crucial design decision of FA is concerned with the out
capability. It is this new semantics of the out operation that facilitates the niceproof of the congruence property and the coincidence results.
The observational theory is supported by the results characterizing the bisimilarity
in terms of the observational bisimilarity. It is also enforced by the Local Observability property. Local Observability is in our opinion a fundamental property ofambients that calls for more attention. We know with hindsight that the designof the variants of the ambient calculus has been driven by the desire to separate
the observational semantics from the syntax. The success of such an endeavor
is manifested by a Local Observability Theorem. The property essentially statesthat putting a syntactical entity in an ambient neither increases nor decreases its
interactive ability. It is a consequence of the well-definedness of the calculus aswell as the well-definedness of the observational equivalences. For FA it would beinteresting to investigate the validity of the Local Observability property in theabsence of the open capability. It is also interesting to see if the property holds
for the other variants of the MA when the open capability is ignored.
An expressiveness result is established by proving that the π-calculus is a subcalculus of FA. This is in our opinion a major contribution of the paper. It formally relates two well known frameworks of distributed mobile computing, the πframework and the ambient framework. This has enforced our intuition that the
π-calculus and the ambient calculi should have a close relationship. As a model forFair ambients

579

distributed mobile computing FA encompasses a broader picture of computing
than the π-calculus. The interpretation of π gives immediately an interpretationof the lazy λ-calculus in FA. It is our hope that the Full Abstraction Theorem will
invite more efforts to investigate the ambient calculi.
The proofs appeared in this paper are interesting not only in that they make extensive use of the Bisimulation lemma but also in that they substantiate our choice of thesemantics. Some of the proofs are facilitated by the particular computing mechanismof FA. The proof of Theorem 6.4 for instance depends crucially on the operationalsemantics we have chosen for the out capability. The proof of the Local Observability
property makes full use of the operational semantics of the open capability. Fromthe point of view of the observational semantics, these proofs have also exploited theproperties of the bisimulations in an essential way. It is with the help of the bisimilarities that we have been able to discover, and prove, the sub-model relationshipbetween π and FA. In summary the paper offers a proof technique whose prominent
feature is the heavy use of the Bisimulation lemma.
FA represents another step towards a better understanding of the calculi for mobile
computing. To cast more light on what have been achieved in this paper and what
aspects of FA remain to be investigated, we take a look at some related work andissues:––

The algebraic theory of MA has been studied in the framework of reductionalsemantics [11,19]. This approach is basically based on a reductional operationalsemantics, a structural congruence and a notion of successful test. Although intuitively straightforward, it is not comfortable to work with the reductional equivalences since one needs to consider all contexts of some form in order to test theequivalence of two ambients. The bisimulation approach to the semantics of theambient calculi has been studied by several researchers. The SAP of Merro andHennessy introduced a labeled transition semantics for a variant of SA in [22,23],
where the bisimulation theory of SAP was studied. FA appears more streamlined
than SAP. The congruence theorem in [22,23] relies on the fact that the capability
operators come with passwords. In [24,25] Merro and Zappa Nardelli study thebisimulation equivalence for MA using a two level semantics. The congruence isproved to be the same as the reduction barbed equivalence. It is worth remarking
that in the labeled transition semantics of MA the ambient a[0] can perform anaction! This is a clear indication that the ambients of MA are best seen as abbreviations of some variants of MA with co-actions. Vigliotti and Phillips have lookedat the barbed congruence in [43] for Safe Ambients. They proved that various
definitions of barbedness induce the same congruence. This result is added withmore weight by Theorem 7.5.
The relationship between the π-Calculus and the ambient calculi is a questionthat has to be settled [30]. Due to its significance, a lot of attentions have been
attracted to it. Results that have been obtained previously vary in shape andstrength. A minimal requirement for a translation from the π-Calculus to ambient calculi is that the reductional behavior of the former is simulated by that of
the latter. The translation in [11] falls in this category. The simulation of the operational semantics may also be required to preserve types [9,12,20]. A translation
meeting the minimal condition neither preserves nor reflects the observational
equalities between processes. A stronger but reasonable requirement is that thetranslation reflects the operational semantics. An important consequence of the

580

–

Y. Fu

stronger property is the full abstraction result about the translation. None of theprevious encodings of the (asynchronous) π-Calculus in the ambient calculi satisfies the stronger requirement. The full abstraction result about our translation ofthe π-Calculus into FA represents a significant progress in the comparative studyof the two models of mobile computing.
Analogously previous interpretations of the lazy λ-Calculus are weak in that they
do not relate the equivalence of the λ-terms to the equivalence of the interpretations of the λ-terms. Our translation and Milner’s encoding of the lazy λ-Calculus
immediately give rise to a translation from the lazy λ-Calculus to FA that preserves the β-conversion. In [36] Sangiorgi discovered that Milner’s encoding is
actually fully abstract with respect to the open applicative bisimilarity, an extension of the applicative bisimilarity of Abramsky [1] to the open λ-terms. It follows
that the encoding of the lazy λ-Calculus in FA is also fully abstract with regards
to the open applicative bisimilarity.
Apart from the calculi we have mentioned in the introduction, other variantsof MA have been discussed. The Boxed Ambients [4] of Bugliesi, Castagna andCrafa for instance abandon the open capability in favor of more flexible communications. The communications in Boxed Ambients could either be horizontal(between siblings) or vertical (between parents and children). In FA the verticalcommunications can be achieved by global communications. To get the idea ofthe encodings it suffices to give the following example:
defa[↓(x).P | c[↑y.C]] = (k)a[k(x).P | k[c(v).out.av] | c[ky.C]]τ−→ (k)a[k(x).P | k[out.ay] | c[C]]τ−→ (k)(k[ay] | a[k(x).P | c[C]])τ−→ a[P{y/x} | c[C]]where out is the derived operator defined in Example 3. This is an example of achild sending a message to its parent. Using similar idea one could express theother three forms of vertical communication as well as the local communicationsof Cardelli and Gordon.
The Controlled Ambients [42] of Teller, Zimmer and Hirschcoff impose the condition that the transmission of an ambient should be consented by both the senderand the receiver. Using the notations developed in this paper the semantics of theControlled Ambients can be described as follows:τa[in b.L | A] | b[in a.M | B] | c[letin a.N] −→ b[a[L | A] | M | B] | c[N]τa[c[out b.M | B] | letout c.L | A] | b[out a.N | C] −→ a[L | A] | c[M | B] | b[N | C]
These three-party interactions can be achieved in two phases: First the present
environment consents for an ambient to leave; and second the target environment
consents for the ambient to come. This can be done in FA as follows:τ

a[c.in b.L | A] | b[in a.M | B] | c[a.N] −→∗ b[a[L | A] | M | B] | c[N]τa[c[↑.out b.M | B] | ↓.L | A] | b[out a.N | C] −→∗ a[L | A] | c[M | B] | b[N | C]
where we have used the encodings of the vertical communications in FA explained
above. This example and the previous one are meant to illustrate how to achieve

Fair ambients–581

in FA the various enhancements of the controlling power of ambients proposedin literature.
Another way to harness the misbehavior of the ambients is to use types. Typesystems of almost all the variants of MA have been proposed. The philosophy oftypes is best explained by the following slogan:
Types = Interfaces = Protocols–

A type specifies the way a process may interact with the environments, which
can also be seen as a protocol between the process and the environments. It is abeneficial exercise to look at the type systems for FA.
There are a number of papers discussing the expressive power of the ambients.
The Turing completeness of the ambient calculi have been established in [44,45,
3,5,21]. Maffeis and Phillips proved in [21] that the ambients with only in andout capabilities but without restrictions are Turing complete. They also showedthat termination is a decidable property for the subcalculus with only the in (orout) capability. In [32] Phillips and Vigliotti showed that the Pure Ambient Calculus without restriction admits symmetric electoral systems. The Full Abstraction
Theorem implies that the subcalculus of FA consisting of the out capability andcommunications is Turing complete. It would be interesting to study the expressive
power of the subcalculi of FA in a systematic way.
A lot of interesting issues about FA await studies. We outline some of them below:

–

–

–

–

A fundamental question is how much more expressive FA is over π. In otherwords, is there an encoding from FA to π that preserves and reflects the interactability. The key problem is how to interpret the nested structures (the structure
in depth) of the ambients by the flat structure of the π-calculus. It is likely thoughthat the interactional ability of the ambients can not be fully captured by the
π-processes.
Another important question is how orthogonal the capability operators of FA
are and how much redundancy there is. To explain what we mean, let FA−indenote the subcalculus of FA that drops the in and co-in operators. If there is an
encoding from FA−in to FA, say the inclusion map, that preserves and reflects
the interactability, then the in and in operators are orthogonal to the other threepairs of operators in the sense that the presence of in and in does not increase theexpressiveness of the other three pairs of operators. If on the other hand there isan encoding from FA to FA−in that preserves and reflects the interactability, thenthe pair in, in are redundant in terms of the interactional behavior. In a larger
scale the characterizations of the expressiveness of the subcalculi of FA are also
important to better our understanding of the ambients. We are currently looking
at these issues.
At a technical level, the question of the coincidence of the late semantics with theearly semantics is nontrivial. Here the analogy with the higher order π-calculus[35,38,41] breaks down. The reason that the early semantics and the late semantics
coincide for the higher order π-calculus is that one can always prefix a transmitted
higher order variable to control its firing after it lands on the target places. On
the other hand there is no way to stop a transmitted ambient from action once it
is in position.
A question hard to answer is concerned with the axiomatization of ≈ for thefinite FA. Ambient calculi are of higher order. The Turing completeness of the

582

–

Y. Fu

higher order communications, like that in the higher order π-calculus, defeats
any attempt to obtain a (decidable) complete system. But if we restricts to linear higher order calculus, complete system can be achieved. In [16] a complete
equational system is constructed for the Linear Higher Order π. The ambientinteractions of FA are linear in the sense that a transmitting ambient is not duplicated when it arrives at the target ambient. Despite of the linearality though, theproblem remains untouched.
From a programming point of view, efforts are called for to see how FA, with orwithout syntactical sugars, can be used as a core language for web applications,
protocol designs, security related issues. In these applications it is extremely useful
to have the if _then_else construct. This construct does not really make sense in
the ambient calculi previously studied. But thanks to the global communications,
FA can be extended with the processes of the form
if ϕ then M else N
where ϕ is a conjunction of match x = y and mismatch x  = y. In this aspect FA
opens up a new avenue for applying the ambients to practical programming.

The reports on the progress of attacking some of the above issues would have to occur
elsewhere.
Acknowledgment The author is supported by The National Distinguished Young Scientist Fund of
NNSFC (60225012), The National 973 Project (2003CB317005) and The National Nature Science
Foundation of China (60473006 and 60573002). He wishes to thank X. Cai, X. Dong, H. Long and H.
Zhu for their proof reading. Examples 7, 10 and 13 were pointed to us by X. Dong. Example 8 waspointed to us by H. Lv. The author is grateful to the referees for their constructive comments andsuggestions.

Appendix A: Two auxiliary definitions
The “bisimulation up to” is a technique widely used in process theory [26]. This is theapproach to establish bisimulation equalities up to some known equivalence. In thissection we recall two well-known (bi)simulation-up-to relations used in the paper. We
first define the strong bisimilarity.
Definition A.1 A symmetric relation R on processes is a strong bisimulation if it isclosed under substitution and the followings hold whenever PRQ:
1.

λ

If P −→ P and λ is in the set {τ , κ} ∪ {a[out b], a[[out b]], a[bx], a[bx], (x)a[bx] |λa, b, x ∈ N } then Q −→ Q RP for some Q .
2.

[out a]∩m)AP then for every name d and every process O satisfying m
If P −→ (fn(O) = ∅ there exist some n, B, Q such that Q(n)(B | d[Q | O]) R (m)(A | d[P | O]).

3.

[out a]−→(n)BQ anda[in b] ∩ fn(O) = ∅ there
If P −→ (m)AP then for every process O satisfying ma[in b]n)BQ and (n)(Q | b[B | O]) R (m)exist some n, B, Q such that Q −→ ((P | b[A | O]).

Fair ambients

4.

If P

583

a[open b]−→

 ∩ fn(O) = ∅ there(m)MP then for every process O satisfying m

exist some n, N, Q such that Q(P | b[M | O]).

a[open b]−→(n)NQ and (n)(Q | b[N | O]) R (m)a[in b]If P −→ C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exists some5.

a[in b]C [_] such that Q −→ C [_] and C [b[N]] R C[b[N]].
6.

If P

a[open b]−→

C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exists

a[open b]
some C [_] such that Q −→ C [_] and C [N] R C[N].

The strong bisimilarity ∼ is the largest strong bisimulation.
The basic algebraic properties of ∼ are guaranteed by the following proposition.
Proposition A.2 The strong bisimilarity ∼ is a congruence.
In observational theories the equivalence ∼ will be explored to iron out the difference between structurally equivalent processes. Technically this is done by using theproof method of ‘bisimulation up to ∼’. The definition of the ‘bisimulation up to ∼’and the proof of the next lemma can be found in [26]. In our framework the definitionis as follows:
Definition A.3 A family of symmetric relations {Rz }z⊆f N on processes is an open simz then Pσ Rz Qσ and the followings
ulation up to ∼ if whenever PRz Q and σ respects 
hold:
τ

1.
2.

If P −→ P then Q ⇒ Q ∼ Rz ∼ P for some Q .
κκ
If P −→ P and κ is not of the form a(x), then Q ⇒ Q ∼ Rz ∼ P for some

Q.

3.

If P −→ P then Q ⇒ Q ∼ Rzx ∼ P for some Q .

4.

If P −→ P and λ is a label in the following set {a[out b], a[[out b]], a[bx], a[bx] |

a(x)

a(x)

λ

λ

a, b ∈ N } then Q ⇒ Q ∼ Rz ∼ P for some Q .
(x)a[bx](x)a[bx]⇒ Q ∼ Rzx ∼ P for some Q .

5.

If P −→ P then Q

6.

If P −→ (m)AP then for every name d and every process O satisfying[out a][out a] ∩ fn(O) = ∅ there exist some n)BQ andmn, B, Q , Q such that Q ⇒ −→ (

z



(
n)(B | d[Q | O]) ⇒ Q ∼ R ∼ (m)(A | d[P | O]).
7.

a[in b] ∩ fn(O) = ∅ some
If P −→ (m)AP then for every process O satisfying ma[in b]n)BQ and (n)(Q | b[B | O]) ⇒ Q ∼n, B, Q , Q exist such that Q ⇒ −→ (zR ∼ (
m)(P | b[A | O]).
8.

a[open b]

 ∩ fn(O) = ∅ some
If P −→ (m)MP then for every process O satisfying ma[open b]n, N, Q , Q exist such that Q ⇒ −→Q ∼ Rz ∼ (m)(P | b[M | O]).
9.

(n)NQ and (n)(Q | b[N | O])⇒a[in b]If P −→ C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist somea[in b]C [_], Q such that Q ⇒ −→ C [_] and C [b[N]] ⇒ Q ∼ Rz ∼ C[b[N]].
10.

If P

a[open b]−→

C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist

some C [_], Q such that Q

a[open b]⇒ −→ C [_] and C [N] ⇒ Q ∼ Rz ∼ C[N].

584

Y. Fu

Proposition A.4 If {Rz }z⊆f N is an open bisimulation up to ∼ then Rz ⊆≈z for all finite
sequences z of names.
As is pointed out in [39] (open) bisimulations up to ≈ fail a proposition like Proposition A.4. Many useful alternatives have been proposed though. The next definition
provides one such alternative.
Definition A.5 A family of symmetric relations {Rz }z⊆f N on processes is an openz then Pσ Rz Qσ and thesimulation up to {≈z }z⊆f N if whenever PRz Q and σ respects
followings hold:
τ

1.
2.

If P −→ P then Q ⇒ Q ≈z Rz P for some Q .
κκ
If P −→ P and κ is not of the form a(x), then Q ⇒ Q ≈z Rz P for some Q .

3.

If P −→ P then Q ⇒ Q ≈zx Rzx P for some Q .

4.

If P −→ P and λ is a label in the following set {a[out b], a[[out b]], a[bx], a[bx] |

a(x)

a(x)

λ

λ

a, b ∈ N } then Q ⇒ Q ≈z Rz P for some Q .
5.
6.

(x)a[bx]

If P −→ P then Q[out a]If P −→(x)a[bx]⇒ Q ≈zx Rzx P for some Q .

(m)AP then for every name d and every process O satisfying[out a] ∩ fn(O) = ∅ there exist some n)BQ andmn, B, Q , Q such that Q ⇒ −→ (


z
z



(
n)(B | d[Q | O]) ⇒ Q ≈ R (m)(A | d[P | O]).
7.

a[in b] ∩ fn(O) = ∅ some
If P −→ (m)AP then for every process O satisfying mn, B, Q , Q exist such that Q
Q ≈z Rz (m)(P | b[A | O]).

8.

⇒a[open b]

 ∩ fn(O) = ∅ some
If P −→ (m)MP then for every process O satisfying mn, N, Q , Q exist such that Q
Q ≈z Rz (m)(P | b[M | O]).

9.

a[in b]⇒ −→ (n)BQ and (n)(Q | b[B | O])a[open b]⇒ −→(n)NQ and (n)(Q | b[N | O])⇒a[in b]If P −→ C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist somea[in b]C [_], Q such that Q ⇒ −→ C [_] and C [b[N]] ⇒ Q ≈z Rz C[b[N]].
10.

If P

a[open b]−→

C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist

some C [_], Q such that Q

a[open b]⇒ −→ C [_] and C [N] ⇒ Q ≈z Rz C[N].

By using the following lemma, the above definition can be exploited to establish
bisimulation equalities.
Proposition A.6 If both {Rz }z⊆f N and {(Rz )−1 }z⊆f N are open simulations up toz of names.
{≈z }z⊆f N then Rz ⊆≈z for all finite sequences 
a[in b]

Proof Suppose for instance P ≈z Rz ≈z Q −→ (x̃)AN. By repeated use of thedefinitions of Rz and ≈z , it is not difficult to see that for every O some ỹ, B, M, P exist
a[in b]such that P ⇒ −→ (ỹ)BM andm)(N | b[A | O])(y)(M | b[B | O]) ⇒ P ≈z Rz ≈z (In this manner one could prove that {≈z Rz ≈z }z⊆f N is a bisimulation.

Fair ambients

585

Appendix B: The proof of Proposition 8.3
f

In this appendix we prove that ≈opn is a congruence equivalence. The idea of theproof is the same as the one in [22]. Before proving the result, we define an orderrelation on transitions.
Suppose t = (t1 , . . . , tn ) is a tree with subtrees t1 , . . . , tn and s is another tree. We
say that s is order less than t if either of the following properties hold:––the depth of s is less than the depth of t;s = (t1 , . . . , ti−1 , si , ti+1 , . . . , tn ) and si is order less than ti .

The tree order is the transitive closure of the order less relation. Now the derivations
can be ordered by imposing the tree order on them. Since every transition has a unique
derivation, we thus have an order relation on the transitions.
The following lemma states the congruence property of the 
x-bisimilarity.
Lemma 14 The following properties hold:(i)

If P ≈x Q then κ.P ≈x κ.Q provided that κ is not of the form a(x);(ii)

If P ≈x Q then P | O ≈x Q | O;(iii)

If P ≈x Q then a[P] ≈x a[Q];(iv)

If P ≈x Q then (y)P ≈x (y)Q;(v)

If P ≈x Q then !P ≈x !Q.

Proof (i) The proof is straightforward.
(ii,iii,iv) Construct a series of relations as follows:zS
0 = ≈opn
def

f

..
. ⎧

⎫
⎨ (P|N, Q|N) ⎬
defz P Sz Q((x)P,
(x)Q)
S
=
i

i+1
⎩
⎭
(a[P], a[Q]) ..
.
Let Sz bezzi∈ω Si . Clearly S is the relation{(C[P], C[Q]) | P ≈z Q, C[_] a context}
We prove by structural induction that {Sz }z⊆f N is an open bisimulation up to ∼. The
inductive proof is carried out in two steps:
1.
2.

zBase Step: The pairs in S
0 satisfy the bisimulation up to ∼ property;zInduction Step: If the pairs in S
i satisfy the bisimulation up to ∼ property, thenz
the pairs in Si+1 satisfy the bisimulation up to ∼ property.
fSince ≈opn satisfies the bisimulation property by definition, we only have to prove theinduction step. Notice that we are proving that Sz is an open bisimulation up to ∼ bystratifying the elements of Sz .

586

Y. Fu

z
Now suppose that the pairs in S
i satisfy the bisimulation up to ∼ property and thatz
PSi Q. That is we have the following induction hypotheses:
τ

1.
2.

If P −→ P then Q ⇒ Q ∼ Sz ∼ P for some Q .
κκ
If P −→ P and κ is not of the form a(x), then Q ⇒ Q ∼ Sz ∼ P for some

Q.

3.

If P −→ P then Q ⇒ Q ∼ Szx ∼ P for some Q .

4.

If P −→ P and λ is a label in the following set {a[out b], a[[out b]], a[bx], a[bx] |

a(x)

a(x)

λ

λ

a, b ∈ N } then Q ⇒ Q ∼ Sz ∼ P for some Q .
(x)a[bx](x)a[bx]⇒ Q ∼ Szx ∼ P for some Q .

5.

If P −→ P then Q

6.

m)AP then for every name d and every process O satisfying
If P −→ ([out a][out a] ∩ fn(O) = ∅ there exist some mn, B, Q , Q such that Q ⇒ −→ (n)BQ and(n)(B | d[Q | O]) ⇒ Q ∼ Sz ∼ (m)(A | d[P | O]).
7.

a[in b] ∩ fn(O) = ∅ some
If P −→ (m)AP then for every process O satisfying ma[in b]n)BQ and (n)(Q | b[B | O]) ⇒ Q ∼n, B, Q , Q exist such that Q ⇒ −→ (zS ∼ (
m)(P | b[A | O]).
8.

a[open b]

 ∩ fn(O) = ∅ some 
If P −→ (m)MP then for every O satisfying mn, N, Q ,a[open b]

Q exist such that Q ⇒ −→Sz ∼ (m)(P | b[M | O]).
9.

(n)NQ and (n)(Q | b[N | O])⇒ Q ∼

a[in b]If P −→ C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist somea[in b]C [_], Q such that Q ⇒ −→ C [_] and C [b[N]] ⇒ Q ∼ Sz ∼ C[b[N]].
10.

If P

a[open b]−→

C[_] then for every N satisfying fn(N) ∩ bn(C[_]) = ∅ there exist

some C [_], Q such that Q

a[open b]⇒ −→ C [_] and C [N] ⇒ Q ∼ Sz ∼ C[N].

We need to verify that the pairs (P|N, Q|N), ((x)P, (x)Q), (a[P], a[Q]), which are inzSi+1 , satisfy the bisimulation up to ∼ property. In other words, we demonstrate thateach of the above ten bisimulation properties persists through structural composition.
In what follows, we enumerate for each structural composition, say (P|N, Q|N), all
the possible interactive effects of each of the above ten bisimulations and show thatthe interactions always result in bisimulations under the induction hypotheses.
–(P|L, Q|L).
τ

τ

a(x)

a(x)

1.
2.

P −→ P . P | L −→ P | L is simulated by Q | L ⇒ Q | L ∼ Sz ∼ P | L.
κκP −→ P and κ is not of the form a(x). P | L −→ P | L is simulated by
κ



z
Q | L ⇒ Q | L ∼ S ∼ P | L.

3.

P −→ P . P|L −→ P |L is simulated by Q|L ⇒ Q |L ∼ Szx ∼ P |L.

4.

P −→ P and λ is a label in the following set {a[out b], a[[out b]], a[bx], a[bx] |

a(x)

λ

λ

λ

(x)a[bx](x)a[bx]

a, b ∈ N }. P | L −→ P | L is simulated by Q | L ⇒ Q | L ∼ Sz ∼ P | L.
5.
6.

(x)a[bx]

P −→ P . P|L −→ P |L is simulated by Q|L[out a][out a]⇒ Q |L ∼ Szx ∼ P |L.

[out a]P −→ (m)AP . P | L −→ (m)A(P | L) is simulated by Q | L ⇒ −→(n)B(Q | L) and (n)(B | d[Q | L | O]) ⇒ Q such that Q ∼ Sz ∼ (m)
(A | d[P | L | O]).

Fair ambients

7.

587

a[in b]P −→ (m)AP . Two cases:–

a[in b]

P | L −→ (m)A(P | L) is simulated by Q | L
anda[in b]⇒ −→ (n)B(Q | L)(n)(Q | L | b[B | O]) ∼ (n)(Q | b[B | O]) | L⇒ Q | LSz (
m)(P | b[A | O]) | L∼ (m)(P | L | b[A | O])–τb[in a]m)(P | C[A]) is simulated by
L −→ C[_]. In this case P | L −→ (
Q|L

τ

(
n)(Q | C[B])⇒⇒∼ Q
∼ Sz ∼ (m)(P | C[A])8.

a[open b]m)MP . Two cases:
P −→ (–a[open b]a[open b]

P|L −→ (m)M(P |L) is simulated by Q|L ⇒ −→ (n)N(Q |L)and(n)(Q | L | b[N | O]) ∼ (n)(Q | b[N | O]) | L⇒ Q | LSz (
m)(P | b[M | O]) | L∼ (m)(P | L | b[M | O])–τb[open a]

L −→ C[_]. In this case P | L −→ (m)(P | C[M]) is simulated by
Q|L

τ

⇒

(
n)(Q | C[N])⇒∼ Q
∼ Sz ∼ (m)(P | C[M])9.

a[in b]P −→ C[_]. Two cases:–

a[in b]a[in b]

P | L −→ C[_] | L is simulated by Q | L ⇒ −→ C [_] | L andC [b[N]] | L ⇒ Q | L ∼ Sz ∼ C[b[N]] | L–τb[in a]x)BL . P | L −→ (x)(C[B] | L ) is simulated by
L −→ (Q|L⇒(x)(C [B] | L )⇒(x)(Q | L )∼ Sz ∼ (x)(C[B] | L )10.

a[open b]

P −→ C[_]. Two cases:–

a[open b]a[open b]

P | L −→ C[_] | L is simulated by Q | L ⇒ −→ C [_] | L andC [N] | L ⇒ Q | L ∼ Sz ∼ C[N] | L

588

Y. Fu

–

τ

b[open a]

L −→ (x)ML . P | L −→ (x)(C[M] | L ) is simulated by
Q|L

⇒

(
x)(C [N] | L )⇒(x)(Q | L )∼ Sz ∼ (x)(C[M] | L )–((v)P, (v)Q).
τ

τ

a(x)

a(x)

1.
2.

P −→ P . (v)P −→ (v)P is simulated by (v)Q ⇒ (v)Q ∼ Sz ∼ (v)P .
κκP −→ P and κ is not of the form a(x). (x)P −→ (x)P is simulated byκ(x)Q ⇒ (x)Q ∼ (x)P .

3.

P −→ P . (v)P −→ (v)P is simulated by (v)Q ⇒ (v)Q ∼ Szx ∼ (v)P .

4.

P −→ P and λ is a label in the following set {a[out b], a[[out b]], a[bx], a[bx] |

a(x)

λ

λ

λ

a, b ∈ N }. And (v)P −→ (v)P is simulated by (v)Q ⇒ (v)Q ∼ Sz ∼ (v)P .
(x)a[bx](x)a[bx](x)a[bx]⇒ (v)Q ∼ Szx ∼5.

P −→ P . (v)P −→ (v)P is simulated by (v)Q(v)P .

6.

m)AP . (v)P −→ (v)(m)AP or (v)P −→ (m)A(v)P is simuP −→ ([out a][out a][out a][out a]lated either by (v)Q ⇒ −→ (v)(n)BQ and(v)(
n)(B | d[Q | O]) ⇒ (v)Q ∼ Sz ∼ (v)(
m)(A | d[P | O])[out a]n)B(v)Q andor by (v)Q ⇒ −→ ((n)(B | d[(v)Q | O])

∼

(v)(
n)(B | d[Q | O])⇒(v)Q

∼ Sz ∼ (v)(
m)(A | d[P | O])7.

a[in b]a[in b]a[in b]m)AP . (v)P −→ (v)(m)AP or (v)P −→ (m)A(v)P is simuP −→ (a[in b]lated either by (v)Q ⇒ −→ (v)(n)BQ and(v)(
n)(Q | b[B | O]) ⇒ (v)Q ∼ Sz ∼ (v)(
m)(P | b[A | O])a[in b]n)B(v)Q andor by (v)Q ⇒ −→ ((n)((v)Q | b[B | O])

∼

(v)(
n)(Q | b[B | O])⇒(v)Q

∼ Sz ∼ (v)(
m)(P | b[A | O])
8.

Pa[open b]−→(m)MP . (v)Pa[open b]−→a[in b](v)(m)MP or (v)P −→ (m)M(v)P isa[open b]

simulated either by (v)Q ⇒ −→ (v)(n)NQ and(v)(
n)(Q | b[N | O]) ⇒ (v)Q ∼ Sz ∼ (v)(
m)(P | b[M | O])a[open b]

or by (v)Q ⇒ −→ (n)N(v)Q and(n)((v)Q | b[N | O])

∼

(v)(
n)(Q | b[N | O])⇒(v)Q

∼ Sz ∼ (v)(
m)(P | b[M | O])

Fair ambients

9.

589

a[in b]a[in b]a[in b]P −→ C[_]. (v)P −→ (v)C[_] is simulated by (v)Q ⇒ −→ (v)C [_] and(v)C[b[B]] ⇒ (v)Q ∼ Sz ∼ (v)C[b[B]]10.

a[in b]a[in b]a[in b]P −→ C[_]. (v)P −→ (v)C[_] is simulated by (v)Q ⇒ −→ (v)C [_] and(v)C[N] ⇒ (v)Q ∼ Sz ∼ (v)C[N]–(c[P], c[Q]).
1.
2.

τ

τ

P −→ P . c[P] −→ c[P ] is simulated by c[Q] ⇒ c[Q ] ∼ Sz ∼ c[P ].
κ
P −→ P . Six cases:–

in ac[in a]c[in a]P −→ P . c[P] −→ P 0 is simulated by c[Q] ⇒ −→ Q1 0 anda[c[Q1 ] | O] ⇒ a[c[Q ] | O] ∼ Sz ∼ a[c[P ] | O]–

open ac[open a]c[open a]

P −→ P . c[P] −→ P 0 is simulated by c[Q] ⇒ −→ Q1 0 anda[Q1 | O] ⇒ a[Q | O] ∼ Sz ∼ a[P | O]

–

in a

c[in a]c[in a]P −→ P . c[P] −→ c[_ | P ] is simulated by c[Q] ⇒ −→ c[_ | Q1 ] andc[a[A] | Q1 ] ⇒ c[a[A] | Q ] ∼ Sz ∼ c[a[A] | P ]–open ac[open a]c[open a]

P −→ P . c[P] −→ c[_ | P ] is simulated by c[Q] ⇒ −→ c[_ | Q1 ]andc[M | Q1 ] ⇒ c[M | Q ] ∼ Sz ∼ c[M | P ]

–

out a

c[out a]c[out a]P −→ P . c[P] −→ P 0 is simulated by c[Q] ⇒ −→ Q1 0 andc[Q1 ] | a[O] ⇒ c[Q ] | a[O] ∼ Sz ∼ c[P ] | a[O]since c[Q ] ∼ Sz ∼ c[P ].

–

out a

c[out a]c[out a]

ax

c[ax]

c[ax]

ax

c[ax]

c[ax]

P −→ P . c[P] −→ c[P ] is simulated by c[Q]

⇒ c[Q ] ∼ Sz ∼ c[P ].

–P −→ P . c[P] −→ c[P ] is simulated by c[Q] ⇒ c[Q ] ∼ Sz ∼ c[P ].

–P −→ P . c[P] −→ c[P ] is simulated by c[Q] ⇒ c[Q ] ∼ Sz ∼ c[P ].
a(x)(x)b[ax](x)b[ax]⇒ b[Q ] ∼ Szx ∼ b[P ].

3.

P −→ P . b[P] −→ b[P ] is simulated by b[Q]4.

P −→ P and λ is a label in the following set {a[out b], a[[out b]], a[bx], a[bx] |a, b ∈ N }. This action is prohibited by c[P].

5.

P −→ P . This is prohibited by c[P].

6.

m)AP . In this case the action c[P] −→ (m)(A | c[P ]) is simuP −→ (lated by

λ(x)a[bx][out b]c[[out b]]c[Q]c[[out b]]⇒(n)(B | c[Q ])⇒Q

∼ Sz ∼ (m)(A | c[P ])7.

a[in b]P −→ (m)AP . This is prohibited by c[P].

590

Y. Fu
a[open b]8.

P −→ (m)MP . This is prohibited by c[P].

9.

P −→ C[_]. This is prohibited by c[P].

10.

P −→ C[_]. This is prohibited by c[P].

a[in b]a[open b]

We have proved that all pairs in Sz satisfy the bisimulation up to ∼ property definedin Definition A.1. Thus Sz ⊆≈z by Proposition A.4.
(v) Let Rx be the following binary relation{(C[!P], C[!Q]) | P ≈x Q, C[_] a context}
We prove that {Rx }z⊆f N is an open simulation up to {≈x }z⊆f N . This is done by using
induction on the derivations. Now suppose C[!P] Rx C[!Q] anda[in b]

C[!P] −→ (m)AP(29)

If the action (29) is solely caused by the context, then the bisimulation is easy toestablish. If P participates in the above action thena[in b]

C[P | !P] −→ (m)AP

(30)

with a smaller derivation order. By induction hypothesis it follows that for each O
some 
n, B, Q , Q exist such that the action in (30) can be matched up by
a[in b]n)BQ
C[P | !Q] ⇒ −→ (

(31)

and
(
n)(Q | b[B | O]) ⇒ Q Rx (m)(P | b[A | O])
But C[P | !Q] ≈x C[Q | !Q] ∼ C[!Q] by (ii) through (iv). Therefore (31) can be simua[in b]

lated by C[!Q]. That is to say that some n1 , B1 , Q1 , Q1 exist such that C[!Q] ⇒ −→(n1 )B1 Q1 andm)(P | b[A | O])(n1 )(Q1 | b[B1 | O]) ⇒ Q1 ≈x Rx (The arguments for the other actions are similar.
The intuition behind the above proof is this: Since every action of !P is caused by aλfinite number of P’s, the action in (29) is essentially the action C[P | · · · | P | !P] −→ U1
in which !P does not participate in the action. Then the following observation
C[!P] ∼ C[P | · · · | P | !P] Rx C[P | · · · | P | !Q] ≈x C[!Q]
immediately suggests the proof.
So we have established that both {Sx }z⊆f N and {(Sx )−1 }z⊆f N are open simulations

up to {≈x }z⊆f N . We are done by applying Proposition A.6.
Proposition 8.3 then follows from the above lemma and the following two lemmas.
Lemma 15 If P ≈x Q then P ≈y Q whenever x ⊆y.

Fair ambients

591

Proof Let {Rz }z⊆f N be the family of relations where each Rz is defined by the following set:{(P, Q)|P ≈y Q whenever y ⊆z}
It is routine to show that {Rz }z⊆f N is an open bisimulation.



Lemma 16 If P ≈xy Q for y  ∈ fn(P|Q) then P ≈x Q.
Proof Let {Rz }z⊆f N be the family of relations where each Rz is defined by the following set:{(Pσ , Qσ )|P ≈zy Q, y  ∈ fn(P|Q) and σ respects z}
Now suppose P ≈zy Q, y  ∈ fn(P|Q) and σ respects z. There are three cases:–––

σ does not contain y. Then σ respects 
zy. This case is simple because Pσ ≈zy Qσ .
y is in the domain of σ but not in the range of σ . In this case Pσ ≡ Pσ  andQσ ≡ Qσ  for some σ  that respects 
zy. So this case is also simple.
y is in the range of σ . In this case there are some substitution σ  and somename x such that σ = σ  {y/x} and σ  respects 
zy. So the problem is reduced
to cases where substitutions are of the form {y/x}. Now suppose σ = {y/x} andPσaσ [in bσ ]a[in b]−→ (m)Aσ P σ . Since y  ∈ fn(P), it is clear that P −→ (m)AP . Then fora[in b] ∩ fn(O) = ∅ there exist O satisfying mn, B, Q , Q such that Q ⇒ −→ (n)BQand(
n)(Q | b[B | O]) ⇒ Q ≈zy (m)(P | b[A | O])
Thus Qσaσ [in bσ ]⇒ −→ (nσ )Bσ Q σ and(n)(Q | b[B | O])σ

⇒ Q σ Rz (m)(P | b[A | O])σOther cases can be proved similarly.
We are done.
fProposition B.1 The equivalence ≈opn is congruent.
f

Proof Since ≈opn is closed under respectful substitutions, it is closed under all substitutions. Therefore it is closed under the prefix a(x) operation. The rest follows from
Lemma 14.
Appendix C: Quasi open bisimulation
An interesting example concerning the open bisimilarity is given by Sangiorgi andWalker [40]. Consider the pair of the π-processes:def

C = (z)az.(a(w) + a(w).zz + a(w).[w=z]zz)
def

D = (z)az.(a(w) + a(w).zz)
a(z) a(w)According to the definition of the open bisimulation [37] the transitions C −→−→
[w=z]zz can not be simulated by D. But from an observational viewpoint, C and D
should be equivalent.

592

Y. Fu

The quasi open bisimulations are rectifications of the open bisimulations thatremove the inequalities like the one in the above. Hence they are weaker than the
open bisimulations. Here is the definition.
Definition C.1 A quasi open bisimulation is a family of symmetric relations {Rz }z⊆f N
on the π-processes such that, for all P and Q, if PRz Q and σ respects
z then Pσ Rz Qσand the following properties hold:
τ

(i)
(ii)

If P −→ P then Q ⇒ Q Rz P for some Q .
ax
ax
If P −→ P then Q ⇒ Q Rz P for some Q .

(iii)

If P −→ P then Q ⇒ Q Rz P for some Q .

(iv)

ax

ax

a(x)

a(x)

If P −→ P then Q ⇒ Q Rzx P for some Q .

We write {≈zπ }z⊆f N for the largest quasi open bisimulation and refer to ≈zπ as the quasi
open 
z-bisimilarity. The quasi open bisimilarity ≈π is the quasi open ∅-bisimilarity≈∅π .
The quasi open bisimilarity ≈π is the same as the open barbed bisimilarity, the latter being defined as the largest barbed bisimulation closed under substitution. The
closure property of the quasi open bisimilarity is guaranteed by the following lemma.
Lemma 17 The following properties hold:
(i)
(ii)
(iii)
(iv)
(v)

If P ≈xπ Q then ay.P ≈xπ ay.Q and τ .P ≈xπ τ .Q;
If P ≈xπ Q then P | O ≈xπ Q | O;
If P ≈xπ Q and y  ∈ 
x then (y)P ≈xπ (y)Q;xy
If P ≈π Q then (y)P ≈xπ (y)Q;
If P ≈xπ Q then !a(x).P ≈xπ !a(x).Q.

The congruence of ≈π follows from the above lemma and the fact that ≈π is closed
under respectful substitutions and therefore all substitutions.
Corollary C.2 ≈π is equivalent and congruent.
For more information on the quasi open bisimilarity, see [40,15].

References
1. Abramsky, S.: The lazy lambda calculus. In: Turner, D. (ed.) Declarative Programming,
pp. 65–116. Addison-Wesley (1988)
2. Barendregt, H.: The lambda calculus: its syntax and semantics, Studies in Logic and Foundationsof Mathematics, North-Holland (1984)
3. Boneva, I., Talbot, J.: When ambients cannot be opened. In: Gordon, A. (ed.) FoSSaCS 2003,
pp. 169–184, Lecture Notes in Computer Science, vol. 2620 (2003)
4. Bugliesi, M., Castagna, G., Crafa, S.: Boxed ambients. In: Kobayashi, N., Pierce, B. (eds.) TACS
2001, pp. 38–63, Lecture Notes in Computer Science, vol. 2215 (2001)
5. Busi, N., Zavattaro, G.: On the expressive power of movement and restriction in pure mobile
ambients. Theor. Comput. Sci. 322, 477–515 (2004)
6. Cardelli, L.: Abstraction for mobile computation. In: Secure Internet Programming: Security
Issues for Mobile and Distributed Object, pp. 51–94, Lecture Notes in Computer Science, vol.
1603 (1999)
7. Cardelli, L.: Brane calculi. In: Danos, V., Schächter, V. (eds.) International Conference on Computational Methods in System Biology, Paris, May 26–28, 2004, Lecture Notes in Computer Science,
vol. 3082 (2005)

Fair ambients593

8. Cardelli, L., Gordon, A.: Mobile ambients. In: Nivat, M. (ed.) FoSSaCS 1998, pp. 140–155 Lecture
Notes in Computer Science, vol. 1378, (1998)
9. Cardelli, L., Gordon, A.: Types for mobile ambients. In: POPL 1999, pp. 79–92. ACM (1999)
10. Cardelli, L., Gordon, A.: Anytime, anywhere: modal logics for mobile ambients. In: POPL 2000,
pp. 365–377. ACM (2000)
11. Cardelli, L., Gordon, A.: Mobile ambients. Theor. Comput. Sci. 240, 177–213 (2000)
12. Cardelli, L., Ghelli, G., Gordon, A.: Mobility types for mobile ambients. In: Wiedermann, J.,
Emde Boas, P., Nielsen, M. (eds.) ICALP 1999, pp. 230–239, Lecture Notes in Computer Science(1999)
13. Fu, Y.: Variations on mobile processes. Theor. Comput. Sci. 221, 327–368 (1999)
14. Fu, Y.: Bisimulation congruences of chi calculus. Inf. Comput. 184, 201–226 (2003)
15. Fu, Y.: On quasi open bisimulation. Theor. Comput. Sci. 338, 96–126 (2005)
16. Fu, Y.: Checking equivalences for higher order process, working paper (2006)
17. Fu, Y., Yang, Z.: Tau laws for pi calculus. Theor. Comput. Sci. 308, 55–130 (2003)
18. Guan, X., Yang, Y., You, J.: Typing evolving ambients. Inf. Process. Lett. 80, 265–270 (2001)
19. Gordon, A., Cardelli, L.: Equational properties of mobile ambients. Math. Struct. Comput.
Sci. 13(3), 371–408 (2003)
20. Levi, F., Sangiorgi, D.: Controlling interference in ambients. In: POPL 2000, pp. 352–364. ACM(2000)
21. Maffeis, S., Phillips, I.: On the computational strength of pure ambient calculi. Theor. Comput.
Sci. 330, 501–551 (2005)
22. Merro, M., Hennessy, M.: Bisimulation congruences in safe ambients. In: POPL 2002, pp. 71–80.
ACM (2002)
23. Merro, M., Hennessy, M.: A bisimulation-based semantic theory of safe ambients. ACM Trans.
Program. Languages Systems 28(2), 290–330 (2006)
24. Merro, M., Zappa Nardelli, F.: Bisimulation proof methods for mobile ambients. In: Baeten, J.,
Lenstra, J., Parrow, J., Woeginger, G. (eds.) ICALP 2003, pp. 584–598, Lecture Notes in Computer
Science, vol. 2719 (2003)
25. Merro, M., Zappa Nardelli, F.: Behavioural theory for mobile ambients. J. ACM 52(6), 961–
1023 (2005)
26. Milner, R.: Communication and Concurrency. Prentice Hall, New Jersey (1989)
27. Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2, 119–146 (1992)
28. Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. In: Information and Computation, vol. 100, pp. 1–40 (Part I), pp. 41–77 (Part II). Academic, New York (1992)
29. Milner, R., Sangiorgi, D.: Barbed bisimulation. In: Dershowitz, N., Lindenstrauss, N. (eds.) ICALP
1992, pp. 685–695, Lecture Notes in Computer Science, vol. 623 (1992)
30. Nestmann, U.: Welcome to the jungle: a subjective guide to mobile process calculi. In: Bauer, C.,
Hermanns, H. (eds.) CONCUR 2006, pp. 52–63, Lecture Notes in Computer Science, vol. 4137
(2006)
31. Phillips, I., Vigliotti, M.: On reduction semantics for the push and pull ambient calculus. In: TCS
2002, IFIP 17th World Computer Congress, Montreal. Kluwer (2002)
32. Phillips, I., Vigliotti, M.: Electoral systems in ambient calculi. In: Walukiewicz, I. (ed.) FoSSaCS
2004, pp. 408–422, Lecture Notes in Computer Science, vol. 2987 (2004)
33. Regev, A., Panina, E., Silverman, W., Cardelli, L., Shapiro, E.: Bioambients: an abstraction forbiological compartments. Theor. Comput. Sci. 325(1), 141–167 (2004)
34. Sangiorgi, D.: Expressing mobility in process algebras: first-order and higher-order paradigms,
PhD thesis, University of Edinburgh (1993)
35. Sangiorgi, D.: From π -calculus to higher order π -calculus-and back. In: Gaudel, M.,
Jouannaud, J. (eds.) TAPSOFT’93, pp. 151-166, Lecture Notes in Computer Science, vol. 668(1993)
36. Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. Inf. Comput. 111, 120–
153 (1994)
37. Sangiorgi, D.: A theory of bisimulation for π -calculus. Acta Inf. 3, 69–97 (1996)
38. Sangiorgi, D.: Bisimulation for higher order process calculi. Inf. Comput. 131(2), 141–178(1996)
39. Sangiorgi, D., Milner, R.: Techniques of “Weak Bisimulation Up To”. In: Cleaveland, W. (ed.)
CONCUR 1992, pp. 32–46, Lecture Notes in Computer Science, vol. 630 (1992)
40. Sangiorgi, D., Walker, D.: On barbed equivalence in π -calculus. In: Larsen, K., Nielsen, M. (eds.)
CONCUR 2001, pp. 292–304, Lecture Notes in Computer Science, vol. 2154 (2001)
41. Sangiorgi, D., Walker, D.: The Pi Calculus—A Theory of Mobile Processes. CUP (2001)

594

Y. Fu

42. Teller, D., Zimmer, P., Hirschcoff, D.: Using ambients to control resources. In: Brim, L., Jancar,
P., Kretinsky, M., Kucera, A. (eds.) CONCUR 2002, pp. 288–303, Lecture Notes in Computer
Science, vol. 2421 (2002)
43. Vigliotti, M., Phillips, I.: Barbs and congruemces for safe mobile ambients. Electr. Notes Theor.
Comput. Sci. 66(3) (2002)
44. Zimmer, P.: On the expressiveness of pure mobile ambients. Electr. Notes Theor. Comput. Sci.
39(1) (2000)
45. Zimmer, P.: On the expressiveness of pure safe ambients. Math. Struct. Comput. Sci. 13(5),721–770 (2003)