Bisimulation Congruence of Chi Calculus
Yuxi Fu ∗Department of Computer Science
Shanghai Jiaotong University, Shanghai 200030, China

Abstract
Chi calculus was proposed as a process calculus that has a uniform treatment of names. Preliminary properties of chi calculus have been examined in literature. In this paper a more systematic studyof bisimilarities for chi processes is carried out. The notion of L-bisimilarity is introduced to give a
possible classification of bisimilarities on chi processes. It is shown that the set of L-bisimilarities form
a four element lattice and that well-known bisimilarities for chi processes fit into the lattice hierarchy.
The four distinct L-bisimilarities give rise to four congruence relations. Complete axiomatization
system is given for each of the four congruences.

Key Words: Process Algebra, Mobile Process, Bisimulation, Axiomatization

1

Introduction

The theory of mobile processes has been one of the focuses in concurrency theory over the nineties. The
prime example of calculi of mobile processes is of course the π-calculus ([17]) of Milner, Parrow andWalker. A mobile process differs from a CCS process ([16]) in that the communication topology of theformer can change during the evolution of the process while that of the latter is static. A communication
between two mobile processes passes a channel name from one process to another; and therefore may
establish new link between them. As it turns out, the ability to send and receive channel names gives
a considerable expressive power to calculi of mobile processes. For one thing, π-calculus can simulate
higher order process calculi in which processes can emit or receive processes as well as channel names([27, 28, 29, 23]). For another thing, the π-calculus has been shown to be capable of modeling a wide
range of computing phenomena familiar in the computing world ([31, 32]).
Mobility also renders the algebraic theory of process algebra difficult. One of the difficulties is to
do with prefix operations. Semantically an input action can instantiate the parameter name by anyother name. The congruence then requires that substituting a name for a free name in two equivalent
π-processes should result in two equivalent processes. This seems to suggest that equivalence relationson π-processes should be closed under substitution on names. In bisimulation equivalences however
there is a choice of whether the requirement of closure under substitution is placed on the first step ofa bisimulation or on each step of the bisimulation. On the other hand, a restricted output action isquite different. A plain fact about π-calculus is that a communication never changes a bound name. A
bound name remains so during process evolution. But in bisimulations, a restricted output action opens
up, so to speak, a bound name. This raises the question of if it is sensible to even consider restricted
output actions in bisimulation argument. Consequently there is a diversity as regards to observational
equalities on π-processes. Among the bisimulation equivalence relations, the early, late, open and barbed
equivalences are the most well known ([17, 24, 18]). The open equivalence is closed under substitution ineach bisimulation step. The other three are closed under substitution only in the first step of bisimulation.
This distinction makes open equivalence strictly stronger than the other three. The barbed equivalencediffers from the other three in another sense: It ignores restricted output actions. As a consequence, it is
weaker than both open and late equivalences and is at least as weak as the early equivalence. Anotherdifficulty is to do with axiomatization. To start with, what operators are necessary in order to have
∗ The author is supported by the NNSFC (69873032), the 863 Hi-Tech Project (863-306-ZT06-02-2), the Young Scientist
Research Fund and the University Scholar Funding Scheme. He is also supported by BASICS, Center of Basic Studies in
Computing Science, sponsored by Shanghai Education Commission. BASICS is affiliated to the Department of Computer
Science of Shanghai Jiaotong University.

1

an expansion law? For example how does one expand ax|b(y)? The law must take into account thepossibility that b might be equated to a after some substitution. For that purpose the match operator isintroduced. Now ax.P |b(y).Q can be expanded as follows:ax.(P |b(y).Q) + b(y).(ax.P |Q) + [a=b]τ.(P |Q{x/y})
The component [a=b]τ.(P |Q{x/y}) retains the possibility that a communication can happen between
ax.P and b(y).Q whenever a = b. Using match operator, complete axiomatization systems for various
strong congruences have been given. Lin has given for the first time a successful attempt to axiomatize
both the weak early congruence and the weak late congruence, using the symbolic approach ([13, 14, 15]).
For some time a complete system for the weak open congruence was not available although it was generally
believed that Milner’s tau laws are sufficient to lift a complete system for the strong open congruence to
a complete system for the weak open congruence. Recently the present author discovered in [10] that the
popular view was wrong. He has proved that Milner’s tau laws fail to achieve a completeness result for
weak open congruence introduced by Sangiorgi. A fourth tau law
τ.P = τ.(P + [x=y]τ.P )(1)

is called for. It is obvious that (1) is valid for weak early congruence, weak late congruence and weakbarbed congruence. One hopes that the discovery of (1) would lead to successful investigation of nonsymbolic approach to axiomatization for weak congruences on mobile processes.
Many variants of π-calculus have been proposed and studied. The internal π-calculus, the πI of
Sangiorgi ([25, 2]), removes the free output prefix operation from the π-calculus. The calculus becomes
symmetric. Another variant is obtained from π-calculus by omitting continuations of output operations.
This is the so called asynchronous π-calculus ([3, 12, 1]). Both variants place restrictions on the use of
output prefix operations. A third variant on the other hand places restrictions on input prefix operations.
The local π-calculus prohibit the use of a parameter name as the subject name of an input prefix in thecontinuation of a process in input prefix form ([19]). Other variants can be obtained by combining
the above features. In [6, 7] a symmetric presentation of π-calculus is given in which a communication
amounts to exchange of names. As for the π-calculus, the algebraic theories of these variants have been
investigated along two lines. One is to find sensible bisimulation equivalences for these languages. The
other is to figure out complete systems for the corresponding bisimulation congruences.
Another variant that departs from π-calculus more significantly is the χ-calculus ([4, 5, 8, 9]). It was
introduced with two motivations in mind. One is to remove the ad hoc nature of prefix operation in
π-calculus by having a uniform treatment of names, thus arriving at a conceptually simpler language.
The second is to materialize a communication-as-cut-elimination viewpoint, therefore taking up a proof
theoretical approach to concurrency theory ([7]), an approach that has been proved very fruitful in thefunctional world. Independently Parrow and Victor have come up with essentially the same language,
Update Calculus as they term it ([20]). They share, we believe, the first motivation but have quite adifferent second one originated from concurrent constraint programming. The difference between π and χlies mainly in the way communications happen. The former adopts the familiar value-passing mechanism
whereas the latter takes an information exchange or information update viewpoint. The algebraic theoryof the language has been investigated in the above mentioned papers. Parrow and Victor have looked into
strong bisimilarity and axiomatization of it for Update Calculus, while Fu has examined an observational
bisimilarity for χ-processes. Later on, Parrow and Victor have proposed Fusion Calculus ([21, 30]),
which is a polyadic version of χ-calculus. The authors have also studied an observational equivalence,called weak hyperbisimilarity ([22]). What we know about the language, albeit little, tells us that it canpractically do everything π can do and its algebraic properties are just as satisfactory.
The objective of this paper is to continue our examination of the algebraic theory of χ-calculus.
The focus will be on bisimulation congruences and their axiomatizations. We will introduce a uniform
definition of weak bisimilarities called L-bisimilarities. These bisimilarities differ from one another in theextent actions are admitted. There are by definition thirty one L-bisimilarities, most of which coincide.
It turns out that there are only four distinct L-bisimilarities. Ordered by inclusion, they form thediamond lattice of four elements. The bottom element of the lattice coincides with open bisimilarity
and the top element with barbed bisimilarity. We then investigate alternative characterizations of theL-bisimilarities. For each of the four L-bisimilarities, we introduce an open style bisimilarity, called
open L-bisimilarity, and prove its coincidence with L-bisimilarity. We then investigate axiomatization
problems for the largest congruence relations contained in the four open L-bisimilarities respectively. A
2sound and complete system for the smallest congruence is obtained by extending the complete system
for the strong bisimilarity with the tau laws. This system can be further extended to complete systems
for the other three congruence relations by adding additional axioms.
The contribution of the paper is two fold. First it introduces the L-bisimilarities, leading to thediscovery of bisimulation lattice. The notion of bisimulation lattice is general enough for it to be applied
to other calculi of mobile processes. For Fusion Calculus it points out that weak barbed bisimilarity
and weak open bisimilarity are distinct. For Update Calculus it leads to an explicit definition of barbed
congruence and axiomatization of it. Second it gives for the first time correct axiomatizations of all the
L-congruence relations. More importantly it explains how such axiomatizations can be achieved: First
one must work out an open characterization of an L-bisimilarity and then makes use of the fact that open
congruence on mobile processes is more easily axiomatized than any other congruence relations. Thisapproach can be readily applied to both Fusion Calculus and Update Calculus.
The paper is organized as follows: Section 2 reviews the operational semantics of χ. Section 3 defines
L-bisimilarities and investigates their relationship. Section 4 gives alternative characterizations of Lbisimilarities. Section 5 presents a complete axiomatization system for each of the congruence relations
induced by the four L-bisimilarities. Some conclusions are made in Section 6.
An extended abstract of this paper has been published ([8]). A mistake in [8] is corrected in this full
paper.

2

Operational Semantics

In π-calculus there are two kinds of bound names. One has dummy names as x in m(x).P and local
names as x in (x)mx.P . Semantically they are very different. The former can be instantiated by any othername received through communication whereas the latter remain unchanged in whatever environment
the process is placed. In simple words, the χ-calculus is obtained from π-calculus by unifying these twokinds of names. This identification forces a unification of input and output prefix operations. The two
π-processes just mentioned then turn into (x)mx.P and (x)mx.P respectively. In the resulting calculus
communications are completely symmetric as exemplified by the following instances of reductions:
τ

P |Q

(2)

τ

R{y/x}|(P {y/x}|Q{y/x}), where y 6= x

(3)τ(z)(P {z/x}|Q{z/y}), where z is fresh(4)

mx.P |mx.Q −→(x)(R|(my.P |mx.Q)) −→(x)mx.P |(y)my.Q −→In (3) a communication through channel m happens. The communication replaces the bound name x
by the free name y throughout the body the restriction operator (x) applies. In (4) the communication
identifies two bound names. The identification is achieved by replacing both the bound x and y by afresh name z and then binds it. In these two communications at least one bound name is affected. This
is not true of the other communication.
Let N be a set of names, ranged over by lower case letters. N , the set of conames, denotes {x | x ∈ N }.
The set N ∪ N will be ranged over by α. Let α be a if α = a and be a if α = a.
We will write C for the set of χ-processes defined by the following abstract syntax:
P := 0 | αx.P | P |P | (x)P | [x=y]P | P +P
As usual 0 denotes the inactive process. The process αx.P is in prefix form. It must first participate in acommunication through channel α or α before P can be activated. Here α or α is the subject name, andx the object name, of the prefix. The composition operator “|” is standard. Two components of | caneither evolve independently or communicate at a common channel. In (x)P the name x is declared local;
it is a bound name. Let bn(P ) denote the set of bound names in P . The set of free names, or nonboundnames, in P is denoted by f n(P ). We will adopt the α-convention saying that a bound name in a process
can be replaced by a fresh name without changing the syntax of the process. The conditional process[x=y]P behaves like either P or 0, depending on whether x = y or not. The constructor [x=y] is often
referred to as a match operator. The choice combinator ‘+’ is well-known. The process P +Q acts either
as P or as Q exclusively. In this paper we leave out the replication operator. The result of this paper
would not be affected had it been included.
The operational semantics can be defined either by reduction semantics ([5]) or in terms of a labeledtransition system ([4]). Here we opt for a pure transition semantics as it helps to present our results with3

clear-cut proofs. The following labeled transition system defines the operational semantics of χ-calculus,
in which symmetric rules are systematically omitted. In the rules the following conventions will be used:µ ranges over {τ } ∪ {αx, α(x) | x ∈ N } and δ over {τ } ∪ {αx, α(x), {y/x} | x, y ∈ N }. In αx and {y/x}
all names are free. In α(x) the name x is bound whereas the other name is free. Let f n(µ), respectivelybn(µ) denote the set of free names, respectively the set of bound names, in µ. The set of names appearedin µ is denoted by n(µ). The notations f n(δ), bn(δ) and n(δ) are defined similarly.
Sequentialization
αx

αx.P −→ P

Sqn

Compositiony/x

P −→ P 0µ

P −→ P 0 bn(µ) ∩ f n(Q) = ∅Cmp0µ
P |Q −→ P 0 |Q

y/x

P |Q −→ P 0 |Q{y/x}Cmp1

Communication
α(x)

α(x)

αy

αx

P −→ P 0αyQ −→ Q0y/xx 6= yP |Q −→ P 0 {y/x}|Q0 {y/x}α(x)P −→ P 0 Q −→ Q0
Cmm1
τP |Q −→ (x)(P 0 |Q0 )P −→ P 0 Q −→ Q0
Cmm0
τP |Q −→ P 0 {y/x}|Q0αxαxP −→ P 0 Q −→ Q0
Cmm3
τP |Q −→ P 0 |Q0

Cmm2

Localization
δP −→ P 0

αx

P −→ P 0

x 6∈ n(δ)δ(x)P −→ (x)P 0

Loc0

y/x

x 6∈ {α, α}α(x)(x)P −→ P 0

Loc1

P −→ P 0
Loc2
τ(x)P −→ P 0

ConditionδP −→ P 0δ[x=x]P −→ P 0

Cnd

SummationδP −→ P 0δ

P +Q −→ P 0

Sum

The labeled transition system uses four kinds of labels, the free action labels of the form αx, the boundaction labels of the form α(x), the internal communication label τ and the update labels of the form{y/x}. The update transition was first introduced in [4, 20] to help define communications in a transition
semantics. The second composition rule shows that an update action affects the neighbouring process
Q by substituting y for x in Q. The notation {y/x} occurred in Q{y/x} is an atomic substitution ofy for x. A general substitution σ is the composition of atomic substitutions, whose effect on a processdef
P is defined by P {y1 /x1 } . . . {yn /xn } = (P {y1 /x1 } . . . {yn−1 /xn−1 }){yn /xn }. The composition of zero
atomic substitution is an empty substitution {} whose effect on a process is vacuous. The labeledtransition system also contains four communication rules. The first is the common one. The second
describes the situation in which a communication identifies two bound names. The side condition is
to guarantee that the restriction operator (x) does not capture any free names already in P |Q. The
third introduces updates. The fourth communication rule admits the kind of communications like thatin (2). The side condition makes sure that Cmm2 and Cmm3 deal with exclusive situations. There
are altogether three localization rules. The first and the second are standard. The last localization rule
closes up an update. So an update is an incomplete communication. The condition rule Cnd and thesummation rule Sum are standard.
The following three derivations might help the reader understand some unusual rules of the semantics.
The first
Sqn
Sqn
mx
mx
mx.P −→ P
mx.Q −→ Qτmx.P |mx.Q −→ P |Q4

Cmm3

establishes (2); the second
Sqn

mymy.P −→ P

Sqn

mx

mx.Q −→ Q

Cmm2

y/x

my.P |mx.Q −→ P {y/x}|Q{y/x}

y/x
Cmp1
R|(my.P |mx.Q) −→ R{y/x}|(P {y/x}|Q{y/x})τ(x)(R|(my.P |mx.Q)) −→ R{y/x}|(P {y/x}|Q{y/x})

Loc2

justifies (3); and the third
Sqn

mz

mz.P {z/x} −→ P {z/x}mzmz.Q{z/y} −→ Q{z/y}

Sqn

m(z)
m(z)
Loc1
(z)mz.P {z/x} −→ P {z/x}(z)mz.Q{z/y} −→ Q{z/y}τ(x)mx.P |(y)my.Q −→ (z)(P {z/x}|Q{z/y})

Loc1
Cmm1

legalizes (4). In the third derivation the α-convention has been applied.
µ

τ

µ

δ

Let =⇒ be the reflexive and transitive closure of −→. We will write =⇒ (=⇒) for =⇒−→=⇒
µ
b

δ

µ

b
δ

δ

(=⇒−→=⇒). We will also write =⇒ (=⇒) for =⇒ (=⇒) if µ 6= τ (δ 6= τ ) and for =⇒ otherwise. A
sequence of names x1 , . . . , xn will be abbreviated as ~x; and consequently (x1 ) . . . (xn )P will be abbreviatedto (~x)P . When the length of ~x is zero, (~x)P is just P .
In the rest of this section we state some technical lemmas whose proofs are simple inductions onderivation.
y/xLemma 1. If P −→ P 0 then x 6∈ bn(P 0 ).
Lemma 2. The following properties hold:µµσ(i) If P −→ P 0 then P σ −→ P 0 σ.
y/x

yσ/xσ

y/x

τ

(ii) If P −→ P 0 and xσ 6= yσ then P σ −→ P 0 σ{yσ/xσ}.
(iii) If P −→ P 0 and xσ = yσ then P σ −→ P 0 σ.
Proof. The proof is carried out by mutual induction.
yσ/x(i) Suppose the last rule applied is Loc2 . By induction hypothesis on (ii), P σ −→ P 0 σ{yσ/x}. Byyσ/xτLemma 1 x 6∈ bn(P 0 ). So P σ −→ P 0 σ. Conclude that (x)P σ −→ P 0 σ.
ασxσ(ii) Suppose the last rule applied is Cmm2 . By induction hypothesis on (i), P σ −→ P 0 σ and
yσ/xσ

ασyσ

yσ/xσ

Qσ −→ Q0 σ. By Cmm2 , P σ|Qσ −→ P 0 σ{yσ/xσ}|Q0 σ{yσ/xσ}. So (P |Q)σ −→ (P 0 |Q0 )σ{yσ/xσ}.
(iii) The last rule applied must be either Cmp1 or Cmm2 . In both cases the proof is simple.
y/x

x/y

Lemma 3. If P =⇒ P 0 then P =⇒ P 0 {x/y}.
α(x)

α(y)

Lemma 4. If P =⇒ P 0 and y 6∈ n(P ) then P =⇒ P 0 {y/x}.
τa(y)a(y) τ

Lemma 5. Suppose a 6∈ bn(P ). If (x)(P |ax) −→−→ P 0 then (x)(P |ax) −→−→ P 0 .
τa(y)Proof. Suppose (x)(P |ax) −→ P1 −→ P 0 . Then P1 must be of the form (z)(P 00 |az). The last rule appliedττ
to derive (x)(P |ax) −→ P1 must be Loc0 . Therefore P {z/x} −→ P 00 for a fresh z and P1 ≡ (z)(P 00 |az).
τ
By Lemma 2, P {z/x}{y/z} −→ P 00 {y/z}. It follows thata(y)(x)(P |ax) −→τ−→P {y/x}|0 ≡ P {z/x}{y/z}|0
P 00 {y/z}|0 ≡ P1

We are done.
y/xτLemma 6. Suppose a 6∈ bn(P ). If (x)(P |ax) −→ P 0 |ay then P −→ P 0 .
y/x

y/x

Proof. The last rule applied must be Loc2 . So P |ax −→ P 0 |ay, which in turn implies that P −→ P 0 by
Cmp1 .
5

3

Bisimulation Lattice

The main focus of the algebraic theory of process algebras is on extensional equalities on processes. The
extensional equalities are observational in the sense that two processes are deemed equal if no process candetect their differences by communicating with them. The finest observational equalities are bisimulation
equalities. Two processes are bisimilar if they can simulate each other’s observational actions up to tau
actions, evolving to processes that are still bisimilar. In the standard approach, all non-tau actions areobservable. In χ-calculus however there are good reasons to ignore certain types of non-tau actions.
First the updates are incomplete communications; it is better to regard them as auxiliary. Second theχ-calculus is intended as target model for concurrent computation. When interpreting a process calculusin χ-calculus, not all non-tau actions of χ are used. An observable equality of the former is most likely
to be related to an observable equality on χ in which these non-tau actions are regarded as auxiliary.
We remark that there are fundamental difference between unobservable actions and auxiliary actions.
Unobservable actions as proper actions whereas auxiliary actions are not. In a bisimulation equivalence,
observable actions are required to match up each other up to unobservable actions. In such an equivalence
auxiliary actions are not even considered.
In this section we study systematically bisimulation equalities on χ-processes, whereby some non-tau
actions are seen as auxiliary actions. For that purpose, we introduce L-bisimilarities, which are refinementof the local bisimilarity of [5]. The L-bisimilarities provide a framework to understand bisimilarity
relations of interest.
Before formally defining L-bisimilarities, some notations need be fixed. Let f a denote the set {ax |a, x ∈ N } of free actions with positive subject name, f a the set {ax | a, x ∈ N } of free actions withnegative subject name, ba the set {a(x) | a, x ∈ N } of bound actions with positive subject name, ba
the set {ax | a, x ∈ N } of bound actions with negative subject name and u the set {y/x | x, y ∈ N } of
updates. Let L stand for {∪S | S ⊆ {f a, f a, ba, ba, u} ∧ S 6= ∅}. Let L range over L.
Definition 7. Let R be a binary symmetric relation on C and let L be an element of L. The relation R
is an L-bisimulation if whenever P RQ then for any process R and any sequence ~x of names it holds thatφif (~x)(P |R) −→ P 0 for φ ∈ L ∪ {τ } such that bn(φ) ∩ f n((~x)(Q|R)) = ∅ then there exists some Q0 suchbφthat (~x)(Q|R) =⇒ Q0 and P 0 RQ0 . The L-bisimilarity ≈L is the largest L-bisimulation.
This is a uniform definition of 31 L-bisimilarities. The intuition behind is that ≈L is what an observer
recognizes if he/she is capable of observing actions in L and only in L. We will show that the Lbisimilarities collapse to four distinct relations. In order to guarantee that ≈L is closed under all but
the choice combinator it is required that an L-bisimulation is closed under parallel composition andrestriction operation under every bisimulation step. First we establish a few technical lemmas. The firstlemma is about the following general property:
A weak observational equivalence ≈ is said to satisfy the *-property if P =⇒ P1 ≈ Q andQ =⇒ Q1 ≈ P implies P ≈ Q.
Lemma 8. ≈L satisfies the *-property.
Proof. Suppose P =⇒ P1 ≈ Q and Q =⇒ Q1 ≈ P . Then the relation {(P, Q)}∪ ≈L is an L-bisimulation.
φ

Suppose for instance (~x)(P |R) −→ P 0 for some φ ∈ L ∪ {τ }. Then by the fact that Q1 ≈L P one has
b
φ

b
φ

some Q0 such that (~x)(Q1 |R) =⇒ Q0 ≈L P 0 . It follows that (~x)(Q|R) =⇒ (~x)(Q1 |R) =⇒ Q0 ≈L P 0 .
Remark : The above lemma holds not only for the L-bisimilarities but also for a wide range of weakobservational equivalences. The barbed and open bisimilarities to be discussed later on enjoy the *property. The proofs of these facts are almost word for word iteration of the above proof.
φφ
For φ ∈ L, let hφi be the process such that (i) hφi −→ 0 and (ii) if hφi −→ A then A ≡ 0.
Lemma 9. Suppose a 6∈ f n(P |Q). Then(i) (x)(P |ax) ≈L (x)(Q|ax) implies P ≈L Q;(ii) P |ax ≈L Q|ax implies P ≈L Q.

6

φ

Proof. (i) Suppose φ ∈ L and n(φ) ∩ f n(P |Q) = ∅. As (x)(P |ax)|ax.hφi =⇒ (P |0)|0, Q1 exists such thata(x)φ(x)(Q|ax)|ax.hφi =⇒ (Q1 |0)|0 ≈L (P |0)|0, which implies (x)(Q|ax) =⇒ Q1 |0 ≈L P |0, which in turnimplies Q =⇒ Q1 ≈L P . Similarly P1 exists such that P =⇒ P1 ≈L Q. By Lemma 8, P ≈L Q.
(ii) can be proved similarly.
Lemma 10. If P ≈L Q then P σ ≈L Qσ for an arbitrary substitution σ.
Proof. Suppose P ≈L Q. We only have to show that for x ∈ f n(P |Q) and y 6= x one has that P {y/x} ≈L
Q{y/x}. Let b be a distinct fresh name. Suppose φ ∈ L and n(φ) ∩ f n(P |Q) = ∅. By definition theactionsφ(x)(P |(by|bx.hφi)) =⇒ P {y/x}|(0|0)
must be matched up by
φ(x)(Q|(by|bx.hφi)) =⇒ Q1 |(0|0)(5)τ

for some Q1 . If (x)(Q|(by|bx.hφi)) −→ (x0 )(Q2 |(by|bx0 .hφi)) then it follows from the proof of Lemma 5ττthat the reduction is the same as (x)(Q|(by|bx.hφi)) −→ (x)(Q3 |(by|bx.hφi)) such that Q −→ Q3 and0Q3 ≡ Q2 {x/x }. It follows that (5) can be factorized as follows(x)(Q|(by|bx.hφi)) =⇒ (x)(Q0 |(by|bx.hφi))τ−→ Q0 {y/x}|(0|hφi)φ=⇒ Q1 |(0|0)
for some Q0 such that Q =⇒ Q0 and Q0 {y/x} =⇒ Q1 ≈L P {y/x}. By Lemma 2, Q{y/x} =⇒ Q0 {y/x}.
Similarly P1 exists such that P {y/x} =⇒ P1 ≈L Q{y/x}. By Lemma 8, P {y/x} ≈L Q{y/x}.
By definition the L-bisimilarity is closed under restriction and composition. Using Lemma 10 it canbe easily seen that ≈L is also closed under prefix operation.
Theorem 11. If P ≈L Q and O ∈ C then(i) αx.P ≈L αx.Q;(ii) P |O ≈L Q|O;(iii) (x)P ≈L (x)Q;(iv) [x=y]P ≈L [x=y]Q.
Proof. (ii) and (iii) follow easily from definition.
(i) Using (ii) and (iii), one can easily prove that {((~y )(R|αx.P ), (~y )(R|αx.Q)) | ~y names, R ∈ C, P ≈LQ}∪ ≈L is an L-bisimulation.
(iv) Similarly {((~z)(R|[x=y]P ), (~z)(R|[x=y]Q)) | x, y, ~z names, R ∈ C, P ≈L Q}∪ ≈L is an Lbisimulation.
We investigate next the order structure of L-bisimilarities. The following theorem unveils the full
picture.
Theorem 12 (bisimulation lattice). The following properties hold of the L-bisimilarities:(i) ≈f a 6⊆≈f a ; ≈f a 6⊆≈f a .
(ii) ≈L ⊆≈u .
(iii) ≈L ⊆≈ba =≈ba .
Proof. (i) It is immediate that (x)ax.(b)(bx|bz) 6≈f a az+(x)ax.(b)(bx|bz). It takes a little while to seethat (x)ax.(b)(bx|bz) ≈f a az+(x)ax.(b)(bx|bz).
y/x(ii) To prove ≈L ⊆≈u , one only has to show, by Theorem 11, that if P ≈L Q and P −→ P 0 then Q0
y/x

y/x

τ

exists such that Q =⇒ Q0 and P 0 ≈L Q0 . Now P −→ P 0 implies that (x)(P |ax) −→ P 0 |ay for a fresh a.

7≈ba ,≈u ,≈ba
*

Y
H

HH

H
≈f a
≈f a
Y
H
*

HH

H

≈f a∪f a
Figure 1: The Bisimulation Lattice of Chi Processes
So (x)(Q|ax) =⇒ Q0 |ay for some Q0 such that P 0 |ay ≈L Q0 |ay. It follows from Lemma 9 that P 0 ≈L Q0 .
Clearly (x)(Q|ax) =⇒ Q0 |ay can be factorized as follows(x)(Q|ax) =⇒ (x)(Q1 |ax)τ−→ Q2 |ay=⇒ Q0 |ay
y/x

τ

y/x

where Q =⇒ Q1 . By Lemma 6, (x)(Q1 |ax) −→ Q2 |ay implies Q1 −→ Q2 . Hence Q =⇒ Q0 .
α(x)τ(iii) Assume P ≈L Q and P −→ P 0 . Suppose φ ∈ L and n(φ) ∩ f n(P |Q) = ∅. Now P |(αz+hφi) −→P1 |0 for some fresh z such that P 0 ≡ P1 {x/z}. There has to be some Q1 such that Q|(αz+hφi) =⇒
α(y)

α(x)

(Q1 |0) ≈L (P1 |0). So Q =⇒ Q1 such that Q1 {z/y} ≈L P1 . Then Q =⇒ Q1 {x/y} by Lemma 4. On theother hand Q1 {x/y} ≡ Q1 {z/y}{x/z} ≈L P1 {x/z} ≡ P 0 by Lemma 10. Hence ≈L ⊆≈ba =≈ba .
In the proof of (iii) of the above theorem, we need to use a fresh name z because we cannot concludeα(y)τR −→ R0 from R|αx −→ R0 |0. It may well be that R participates in the communication by performing
αxR −→ R0 .
Let L(χ) be {≈L | L ∈ L}, the set of all L-bisimilarities. L(χ) is a partial order when equipped withthe subset relation ⊆. For ≈L1 , ≈L2 ∈ L(χ), ≈L1 ∪L2 is the infimum. Theorem 12 says that L(χ) is afour element lattice as drawn in Figure 1. In the diagram each node is the principal representative of anumber of L-bisimilarities that boil down to a same relation. For instance ≈f a represents all the elementsof {≈L | f a ⊆ L ⊆ f a ∪ ba ∪ ba ∪ u, L ∈ L}. An arrow indicates a strict inclusion. The bottom element isrepresented by ≈f a∪f a while the top element is by ≈ba =≈ba =≈u . We will call (L(χ), ⊆) the bisimulation
lattice of χ-processes. The lattice structure suggests that the ability to observe free actions is stronger
than that to observe bound actions.

4

Alternative Characterization

The definition of L-bisimilarities is natural but not very tractable. It contains universal quantifications
over both processes and names. In this section alternative characterizations of the four distinct Lbisimilarities are presented. For each of the relations, an open style bisimilarity is shown to coincidewith it. In the alternative definitions, one still has a universal quantification over substitutions. But it
is clear that one only has to consider a finite number of them at each step. First we will see how barbed
bisimilarity fits into the lattice hierarchy.

4.1

Barbed Bisimilarity

Barbed bisimilarity ([18]) seems to be the weakest bisimulation equivalence proposed so far. It applies toa whole range of process calculi and therefore acts as a convenient tool to study relationships between different process calculi. The relationship of barbed bisimilarity to other bisimilarities is itself an interestingquestion. Usually it is easy to show that a given bisimilarity is included in the barbed one. The difficulty
is often in deciding if the inclusion is strict or not. This section takes a look at barbed bisimilarity on
χ-processes.
α(x)

αx

Definition 13. A process P is strongly barbed at a, notation P ↓a, if P −→ P 0 or P −→ P 0 for some P 0such that a ∈ {α, α}. P is barbed at a, written P ⇓a, if some P 0 exists such that P =⇒ P 0 ↓a. A binary
relation R is barbed if ∀a ∈ N .P ⇓a ⇔ Q⇓a whenever P RQ.
8The idea of barbed bisimilarity is that two processes are regarded as equal if they can simulate eachother’s communication while maintaining same ability to communicate through any particular name.
Definition 14. Let R be a barbed symmetric relation on C. It is called a barbed bisimulation if wheneverτ
P RQ then for any R and any sequence ~x of names it holds that if (~x)(P |R) −→ P 0 then Q0 exists suchthat (~x)(Q|R) =⇒ Q0 and P 0 RQ0 . The barbed bisimilarity ≈b is the largest barbed bisimulation.
The barbed bisimilarity ≈b can be investigated in a similar manner the L-bisimilarities have been
investigated. We will avoid such a rerun by establishing the coincidence of ≈b with one of the Lbisimilarities. The proof of the coincidence employs the following lemma.
Lemma 15. ≈b is closed under substitution.
Proof. Suppose P ≈b Q and a is a distinct fresh name. Nowτ(x)(P |(ax|ay)) −→ P {y/x}|(0|0)
which by definition must be matched up by(x)(Q|(ax|ay)) =⇒ Q1 |(0|0) ≈b P {y/x}|(0|0)
By the proof of Lemma 5 the above reduction can be factorized as(x)(Q|(ax|ay))=⇒ (x)(Q2 |(ax|ay))−→ Q2 {y/x}|(0|0)=⇒ Q1 |(0|0)

such that Q =⇒ Q2 . By Lemma 2, Q{y/x} =⇒ Q2 {y/x} =⇒ Q1 ≈b P {y/x}. Similarly P1 exists
such that P {y/x} =⇒ P1 ≈b Q{y/x}. To show that ≈b satisfy the *-property we need to verify that∀c ∈ N .P {y/x}⇓c ⇔ Q{y/x}⇓c. But this is obvious for if P {y/x} =⇒ P1 ↓c then (x)(P |(ax|ay)) =⇒(P1 |(0|0))↓c, which implies that (x)(Q|(ax|ay)) =⇒ (Q0 |(0|0))↓c for some Q0 by barbedness. It follows
that Q{y/x} =⇒ Q0 ↓c. By the remark right after Lemma 8 one conclude that P {y/x} ≈b Q{y/x}.
We can now locate ≈b in the bisimulation lattice.
Theorem 16. ≈b is the same as ≈ba .
α(x)

α(z)

Proof. As ≈ba is clearly barbed, ≈ba ⊆≈b . Now suppose P ≈b Q and P −→ P 0 . By Lemma 4, P −→ P1
for some fresh z such that P 0 ≡ P1 {x/z}. Let a be fresh. Nowττ

P |(αz.aa|aa) −→−→ P1 |(0|0)
which must be matched up by
Q|(αz.a[a]|aa) =⇒ Q1 |(0|0) ≈b P1 |(0|0).
αz

α(y)

There are only two ways for Q to evolve into Q1 : either Q =⇒ Q1 or Q =⇒−→ Q0 and Q0 {z/y} =⇒ Q1 .
The former is impossible because z is fresh. By Lemma 2 and Lemma 4α(x)Q =⇒−→ Q0 {x/y}andQ0 {z/y}{x/z} =⇒ Q1 {x/z}
By Lemma 15α(x)Q =⇒ Q1 {x/z} ≈b P1 {x/z} ≡ P 0 .
Conclude that ≈b ⊆≈ba .

9

4.2

Open Bisimilarity

In calculi of mobile processes the names in a process are “open” for instantiations by other names. It istherefore natural to require that bisimulations on mobile processes should be closed under substitution.
Such bisimulations have been studied by Sangiorgi in [24] for π-processes. In this section we define open
bisimilarities for χ-processes and relate them to the L-bisimilarities.
Definition 17. Let R be a binary symmetric relation on C. It is called an open bisimulation if wheneverδbδ

P RQ then for any substitution σ it holds that if P σ −→ P 0 then Q0 exists such that Qσ =⇒ Q0 and
P 0 RQ0 . The open bisimilarity ≈open is the largest open bisimulation.
It is clear from the definition that ≈open is closed under substitution.
Lemma 18. ≈open is closed under restriction and composition.
Proof. Using the fact that ≈open is closed under substitution, one sees immediately that {((x)P, (x)Q) |
y/x

τ

y/x

P ≈open Q} is an open bisimulation. For instance if (x)P −→ P 0 is caused by P −→ P 0 then Q =⇒Q0 ≈open P 0 and therefore (x)Q =⇒ Q0 . Other cases are equally simple.
Theorem 19. ≈open coincides with ≈f a∪f a .
Proof. By Lemma 10 and the proof of Theorem 12, (f a ∪ f a)-bisimilarity is an open bisimulation. By
Lemma 18, open bisimilarity is an (f a ∪ f a)-bisimulation.
The definition of open bisimilarity makes it easy to give axiomatization system for finite χ-processes.
Theorem 19 enables us to axiomatize the largest congruence contained in the bottom element of thebisimulation lattice L(χ), as we shall see in next section. In order to do the same for the other threeelements of the bisimulation lattice, one would like to characterize these three L-bisimilarities in an ‘open’
style, so to speak. This is precisely what we are going to do next. The intuition for the following definition
comes from the example given in the proof of (i) of Theorem 12.
Definition 20. Let R be a binary symmetric relation on C. It is called an open ba-bisimulation (openf a-bisimulation, open f a-bisimulation) if whenever P RQ then for any substitution σ it holds thatφ(i) if P σ −→ P 0 for φ ∈ ba ∪ ba ∪ u ∪ {τ } (φ ∈ f a ∪ ba ∪ ba ∪ u ∪ {τ }, φ ∈ f a ∪ ba ∪ ba ∪ u ∪ {τ }) then Q0bφexists such that Qσ =⇒ Q0 and P 0 RQ0 ; and
αx
ax
ax
αx
(ii) if P σ −→ P 0 (P σ −→ P 0 , P σ −→ P 0 ) then some Q0 exists such that P 0 RQ0 and either Qσ =⇒ Q0ax

α(z) x/zaxa(z) x/za(z) x/z(Qσ =⇒ Q0 , Qσ =⇒ Q0 ) or Qσ =⇒=⇒ Q0 (Qσ =⇒=⇒ Q0 , Qσ =⇒=⇒ Q0 ) for some fresh z.
fafa
The open ba-bisimilarity (open f a-bisimilarity, open f a-bisimilarity), denoted by ≈ba
open (≈open , ≈open ),is the largest open ba-bisimulation (open f a-bisimulation, open f a-bisimulation).
The next theorem explains the reason to introduce Definition 20.
aaTheorem 21. (i) ≈fopen=≈f a ; (ii) ≈fopen=≈f a ; (iii) ≈ba
open =≈ba .
αx

Proof. It is enough to see how to establish (iii). Suppose P ≈ba Q and P −→ P 0 . For a fresh name z
x/z

x/z

one has P |αz −→ P 0 |0. As ≈ba =≈u , Q0 exists such that Q|αz =⇒ Q0 |0 ≈ba P 0 |0. There are only twoα(y) x/yαxα(z) x/z

possibilities: either Q =⇒ Q0 ≈ba P 0 or Q =⇒=⇒ Q0 ≈ba P 0 . If the latter holds then Q =⇒=⇒ Q0 ≈ba P 0
by Lemma 4 and Lemma 10. Hence ≈ba ⊆≈baopen by Lemma 10.
To prove the reverse inclusion we use the fact that ≈ba
open is by definition closed under substitution.
We only have to show that composition and restriction operators preserve the relation ≈baopen . To provethat {((~v )(P |R), (~v )(Q|R)) | P ≈ba
Q}
is
an
open
ba-bisimulation,itissufficienttoexaminethe cases
open
where P performs a free action.
x/y

αx

αy

αx

• (~v )(P |R) −→ (~v )(P 0 {x/y}|R0 {x/y}) is derived from P −→ P 0 and R −→ R0 . If P −→ P 0 can
α(z)

αx

0
be matched up by Q =⇒ Q0 ≈ba
open P we are done. Otherwise it must be matched up by Q =⇒{x/z}

Q1 =⇒ Q0 for some Q1 , Q0 and fresh z. By Lemma 2x/y(~v )(Q|R) =⇒ (~v )(Q1 {y/z}|R0 ) =⇒ (~v )(Q0 {y/z}{x/y}|R0 {x/y}) ≡ (~v )(Q0 {x/y}|R0 {x/y})
10

y/x

αy

αx

αx

• (~v )(P |R) −→ (~v )(P 0 {y/x}|R0 {y/x}) is derived from P −→ P 0 and R −→ R0 . Suppose P −→ P 0 is
α(z)

x/z

z/x

matched up by Q =⇒ Q1 =⇒ Q0 for some Q1 , Q0 and fresh z. Then Q1 =⇒ Q0 {z/x}. It follows
y/x

from Lemma 2 that Q1 {y/z} =⇒ Q0 {y/x}. Hencey/x(~v )(Q|R) =⇒ (~v )(Q1 {y/z}|R0 ) =⇒ (~v )(Q0 {y/x}|R0 {y/x})
τ

α(y)

αx

• (~v )(P |R) −→ (~v )(P 0 |R0 ) is derived from P −→ P 0 and R −→ R1 such that R0 ≡ R1 {x/y}. Suppose
{x/z}

α(z)

αx

P −→ P 0 is matched up by Q =⇒ Q1 =⇒ Q0 for some Q1 , Q0 and fresh z. Therefore(~v )(Q|R) =⇒ (~v )(z)(Q1 |R1 {z/y}) =⇒ (~v )(Q0 |R1 {z/y}{x/z}) ≡ (~v )(Q0 |R0 )α(x)αx• Suppose that (~v )(P |R) −→ (v~0 )(P 0 |R), where x ∈ {~v }, is derived from P −→ P 0 by applying rule
α(z)

αx

x/z

Loc1 . Suppose P −→ P 0 is matched up by Q =⇒ Q1 =⇒ Q0 for some Q1 , Q0 and fresh z. For afresh w one has thatα(z)w/zQ{w/x} =⇒ Q1 {w/x} =⇒ Q0 {w/x}
By Lemma 4 and Lemma 10
α(x)

w/x

Q{w/x} =⇒ Q1 {w/x}{x/z} =⇒ Q0 {w/x}since z 6∈ f n(Q0 {w/x}). By Lemma 3
α(x)

x/w

Q{w/x} =⇒ Q1 {w/x}{x/z} =⇒ Q0
It follows thatα(x)(v~00 )(Q{w/x}|R{w/x}) =⇒ (v~00 )(Q1 {w/x}{x/z}|R{w/x})=⇒ (v~0 )(Q0 |R)
where w is a fresh name and v~00 is obtained from ~v by substituting w for x.
The closure property allows us to conclude that ≈ba
open is a ba-bisimulation.
Using the above theorem it is easy to see that the following propositions hold:(z)mz.(P + hx|zi.Q)(z)mz.(P + hx|zi.Q)(z)αz.(P + hx|zi.Q)

=f a
=f a
=ba

(z)mz.(P + hx|zi.Q) + mx.Q{x/z}, where x 6= z(z)mz.(P + hx|zi.Q) + mx.Q{x/z}, where x 6= z(z)αz.(P + hx|zi.Q) + αx.Q{x/z}, where x 6= z

The open style bisimilarities are particularly suitable for χ-like process calculi in which names are
uniform.

5

Axiomatization

For each of the congruence relation on processes, there is a question of how to give an inference system thatis sound and complete for the relation on finite processes. This is an important question in two aspects.
First a complete system represents a crucial step in our understanding of the congruence relation. Second
a complete system is usually a basis for automatic reasoning of the relation. The question is relatively
simple for congruence relations in CCS ([11, 16]). It is a difficult one in π-calculus.
The L-bisimilarities are not congruence relations. To get a congruence relation from ≈L we use thestandard approach: Let =L be the largest congruence contained in ≈L . It can be formally defined asfollows:
Definition 22. P =L Q if and only if P ≈L Q and for each substitution σ the following property holds:ττ(i) whenever P σ −→ P 0 then Q0 exists such that Qσ =⇒ Q0 and P 0 ≈L Q0 ;ττ00(ii) whenever Qσ −→ Q then P exists such that P σ =⇒ P 0 and P 0 ≈L Q0 .
11

The fact that =L is congruent is established by exploiting Theorem 19 and Theorem 21 since thestandard argument can be applied to the open bisimilarities in an obvious way. We will call =L the Lcongruence on χ-processes. The bisimulation lattice says that there are only four distinct L-congruence
relations.
The aim of this section is to give complete axiomatization systems for all the four distinct L-congruence
relations.

5.1

Strong Case

Before tackling the problem of axiomatizing L-congruences, we introduce strong bisimilarity on χprocesses and its complete axiomatization system. The results in this section are not original, mostof which are already in [22]. They are included for completeness reason.
Definition 23. Let R be a binary symmetric relation on C. The relation R is a strong bisimulationδδif, for each substitution σ, whenever P σ −→ P 0 then Q0 exists such that Qσ −→ Q0 and P 0 RQ0 . The
largest strong bisimulation, called the strong bisimilarity, is denoted by ∼.
The relation is what one would have called strong open bisimilarity. It is routine to show that ∼ is anequivalence and congruence relation and is closed under substitution. Strong versions of L-bisimilarity,
barbed bisimilarity and others can be defined in very much the standard manner. All of them coincidewith ∼. It seems better to leave out any adjective and simply call ∼ the strong bisimilarity.
For purpose of axiomatization, we introduce update and tau prefix operations. They are defined asfollows, where a and b are fresh:hy|xi.P
τ.P

def

=

(a)(ay|ax.P )def=(b)hb|bi.P

τNotice that hx|xi.P −→ P and hx|xi.P =L τ.P . So hx|xi also plays the role of τ prefix operation. It isclear that hx|yi.P =L hy|xi.P due to the symmetry of communication.
We will need to deal with a sequence of match constructs concatenated one after another. It isconvenient to have a meta symbol for such a sequence. In the rest of the paper M and N denote finite
lists of match equalities. Suppose M is x1 =y1 , . . . , xn =yn . Then [M ]P denotes [x1 =y1 ] . . . [xn =yn ]P .
If M logically implies N , we write M ⇒ N ; and if both M ⇒ N and N ⇒ M we write M ⇔ N . If
M is an empty list, it plays the role of logical truth, in which case [M ]P is just P . Clearly a list M ofmatch equalities defines an equivalence relation on the set n(M ) of names appearing in M . We use σM
to denote an arbitrary substitution that sends all members of an equivalence class of that relation to arepresentative of that class. Let π and γ range over {αx, hy|xi | x, y ∈ N }.
In [24] Sangiorgi presents a complete system for strong open congruence on π-processes. Parrow andVictor consider in [20] two axiomatization systems for strong bisimilarity on Update processes, one withmismatch operator and one without mismatch operator. The latter is of similar style to Sangiorgi’ssystem. The strong bisimilarity of Fusion processes has also been axiomatized ([22]). In Figure 2 aconditional equational system is defined, which is a monadic version of Parrow and Victor’s systems. Let
AS denote the system consisting of the rules and laws in Figure 2 plus the following expansion law:
P |Q =X[Mi ](~x)πi .(Pi |Q) +

i

X

P

[Mi ][Nj ](~x)(~y )[ai =bj ]hxi |yj i.(Pi |Qj ) +γj =bj yj[Nj ](~y )γj .(P |Qj ) +jwhere P is

πi X
=ai xi

πi X=ai xi[Mi ][Nj ](~x)(~y )[ai =bj ]hxi |yj i.(Pi |Qj )γj =bj yjx)πi .Pi and Q isi [Mi ](~P

πi X
=ai xiy )γj .Qj . In the expansion law the summandj [Nj ](~[Mi ][Nj ](~x)(~y )[ai =bj ]hxi |yj i.(Pi |Qj )γj =bj yj

contains [Mi ][Nj ](~x)(~y )[ai =bj ]hxi |yj i.(Pi |Qj ) as a summand whenever πi = ai xi and γj = bj yj . AS is
Victor and Parrow’s system without mismatch. The only difference is that we use a symmetric update
prefix operator. Some derived rules of AS, together with their justifications, are given in Figure 3.
12Equivalence
E1
E2
E3
Congruence
C1
C2
C3
C4
C5
Localization
L1
L2
L3
L4
L5
L6
L7
L8
L9
L10
Match
M1
M2
M3
Selection
S1
S2
S3
S4
Update
U1
U2
U3

P
P
P

=
=
=

P
Q
R

αx.P
(x)P
[x=y]PP +R
P0 |P1

=
=
=
=
=

αx.Q
(x)Q
[x=y]Q
Q+R
Q0 |Q1(x)0(x)αy.P(x)αy.P(x)(y)P(x)[y=z]P(x)[x=y]P(x)(P +Q)(x)hy|zi.P(x)hy|xi.P(x)hx|xi.P

=
=
=
=
=
=
=
=
=
=

0
0
αy.(x)P(y)(x)P[y=z](x)P0(x)P +(x)Q
hy|zi.(x)Pτ.P {y/x}
τ.(x)P[M ]P[x=y]P[x=y](P +Q)

=
=
=

[N ]P
[x=y]P {y/x}[x=y]P +[x=y]Q

P +0
P +Q
P +(Q+R)[x=y]P +P

=
=
=
=

P
Q+P
(P +Q)+RP

hy|xi.P
hy|xi.Phx|xi.P===hx|yi.P
hy|xi.[x=y]P
τ.P

if Q = P
if P = Q and Q = R
if P = Q
if P = Q
if P = Q
if P = Q
if P0 = Q0 and P1 = Q1

x ∈ {α, α}x 6∈ {y, α, α}x 6∈ {y, z}

x 6∈ {y, z}
y 6= x

if M ⇔ N

Figure 2: Axioms for Strong Bisimilarity on Chi Processes
We will write AS∪{R1 , . . . , Rn } ` P = Q to mean that the equality P = Q is derivable from the rules
and axioms of AS together with rules R1 , . . . , Rn . When no confusion arises, we simply write P = Q.
R
We will also write P = Q to indicate that R is the major axiom applied to derive P = Q.
Using axioms in AS, a process can be converted to a process that contains no occurrence of composition
operator.
Definition 24. A process P is in normal form if it is of the form
X
X
X[Mi ]αi xi .Pi +[Mi ](x)αi x.Pi +[Mi ]hzi |yi i.Pi
i∈I1

i∈I2

i∈I3

such that x does not appear in P and Pi is in normal form for each i ∈ I1 ∪ I2 ∪ I3 . Here I1 , I2 and I3
are pairwise disjoint finite indexing sets.
Notice that if P is in normal form and σ is a substitution then P σ is in normal form. The depth ofa process measures the maximal length of nested prefixes in the process. The structural definition goesas follows: (i) d(0) = 0; (ii) d(αx.P ) = 1 + d(P ); (iii) d(P |Q) = d(P ) + d(Q); (iv) d((x)P ) = d(P ); (v)d([x=y]P ) = d(P ); (vi) d(P +Q) = max{d(P ), d(Q)}.
Lemma 25. In AS every process P is provably equal to some P 0 in normal form such that d(P 0 ) ≤ d(P ).
13

LD1
MD1
MD2
MD3
SD1
SD2
UD1

(x)hx|xi.P[x=y].0[x=x].P[M ]P
P +P[M ]P +P
hy|xi.P

=
=
=
=
=
=
=

hy|yi.(x)P0P[M ](P σM )PP
hy|xi.P {y/x}U3 and L8
S1 and S4
M1
M2
MD2 and S4
S-rules
U2 and M2

Figure 3: Some Laws Derivable from AS
Proof. The proof is carried out by structural induction. If for example the outer most combinator of aprocess is a restriction operator then the process is either equal to 0 or equal to a process of the form(x)αx.P such that x 6∈ {α, α} or the restriction operator can be pushed inside. It is obvious that thisconversion procedure does not increase the depth of the process.
Theorem 26. AS is sound and complete for ∼.
Proof. By Lemma 25 every process is provably equal to a normal form process. So we can focus on
normal form processes exclusively. Let P be
XXX
[Mi ]αi xi .Pi +[Mi ](x)αi x.Pi +[Mi ]hzi |yi i.Pi
i∈I1

i∈I2

i∈I3

and Q beX

[Nj ]αj xj .Qj +

j∈J1

X

[Nj ](x)αj x.Qj +

j∈J2

X

[Nj ]hzj |yj i.Qj

j∈J3

Suppose P ∼ Q. We show that P = Q is provable in AS. The proof is carried out by induction on the sumzi σM /yi σMiiof depths of P and Q. Consider [Mi ]hzi |yi i.Pi for some i ∈ I3 . Now either ([Mi ]hzi |yi i.Pi )σMi−→τPi σMi {zi σMi /yi σMi } or ([Mi ]hzi |yi i.Pi )σMi −→ Pi σMi . In the first case , some j ∈ J3 must exist suchzj σM /yj σMiithat ([Nj ]hzj |yj i.Qj )σMi−→
Qj σMi {zj σMi /yj σMi }, Mi ⇒ Nj , zi σMi = zj σMi , yi σMi = yj σMi
and Pi σMi {zi σMi /yi σMi } ∼ Qj σMi {zj σMi /yj σMi }. By induction hypothesis Pi σMi {zi σMi /yi σMi } =Qj σMi {zj σMi /yj σMi } is provable in AS. It follows thatQ + [Mi ]hzi |yi i.Pi

M D3

=

Q + [Mi ]hzi σMi |yi σMi i.Pi σMi

U D1

=

Q + [Mi ]hzi σMi |yi σMi i.Pi σMi {zi σMi /yi σMi }

I.H.

=

Q + [Mi ]hzj σMi |yj σMi i.Qj σMi {zj σMi /yj σMi }U D1

Q + [Mi ]hzj σMi |yj σMi i.Qj σMi

M D3

=

Q + [Mi ]hzj |yj i.Qj

M1

Q + [Mi ][Nj ]hzj |yj i.Qj

=

=

SD2

=

Q

In the second case it can also be proved that Q + [Mi ]hzi |yi i.Pi = Q.
Similarly one shows that AS ` Q + [Mi ]αi xi .Pi = Q for every i ∈ I1 and AS ` Q + [Mi ](x)αi x.Pi = Q
for every i ∈ I2 . Conclude AS ` P + Q = P . Similarly AS ` P + Q = Q. Hence AS ` P = Q.

5.2

Weak Case

Complete systems for L-congruence relations are obtained by extending the system for strong bisimilarity.
We need the χ-version of the well-known tau laws as given in Figure 4. The simple forms of T1 through T3
are enough since TD1 through TD4 are derivable from T1 and T3. As we mentioned in the introduction,
we need a new tau law to deal with mobility. The following lemma demonstrates the power of this newtau law.

14

T1
T2
T3
T4
TD1
TD2
TD3
TD4

αx.τ.PP + τ.P
αx.(P + τ.Q)
τ.P
hx|yi.τ.P
τ.τ.P
hx|yi.(P + τ.Q)
τ.(P + τ.Q)

=
=
=
=
=
=
=
=

αx.P
τ.P
αx.(P + τ.Q) + αx.Q
τ.(P + [x=y]τ.P )hx|yi.P
τ.P
hx|yi.(P + τ.Q) + hx|yi.Q
τ.(P + τ.Q) + τ.Q

Figure 4: The Tau Laws
P1
P2(z)az.(P + hx|zi.Q)(z)az.(P + hx|zi.Q)==(z)az.(P + hx|zi.Q) + ax.Q{x/z}(z)az.(P + hx|zi.Q) + ax.Q{x/z}x 6= zx 6= zFigure 5: The Prefix Laws
Lemma 27. AS ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.(P +Pi∈I [Mi ]τ.P ) for a finite nonempty indexing set I.

Proof. First we prove that AS ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.(P + [M ]τ.P ). When M is empty, the result
follows from T1 and T2. So the base case holds. Now observe that
τ.P

T4

=

SD2

=

I.H.

=

M2

=

M1

=

M2

=

T4

=

τ.(P + [x=y]τ.P )τ.(P + [M ][x=y]τ.P + [x=y]τ.P )τ.(P + [M ][x=y]τ.P + [x=y]τ.(P + [M ]τ.P ))τ.(P + [M ][x=y]τ.P + [x=y]τ.(P + [M ]τ.P ){y/x})
τ.(P + [M ][x=y]τ.P + [x=y]τ.(P + [M ][x=y]τ.P ){y/x})
τ.(P + [M ][x=y]τ.P + [x=y]τ.(P + [M ][x=y]τ.P ))τ.(P + [M ][x=y]τ.P )So the induction step can be established.
The above result provides the base case of the lemma, and the following derivation provides theinduction step:
X
X
X
I.H.
τ.(P +[Mi ]τ.P + [M ]τ.P ) = τ.(P +[Mi ]τ.P + [M ]τ.(P +[Mi ]τ.P ))
i∈I

i∈I

=

τ.(P +Xi∈I[Mi ]τ.P )

i∈I
I.H.

=

τ.P

where the second equality holds by the above result.
The tau laws are enough to characterize =f a∪f a . To get complete systems for the other three Lcongruence relations, we need what we call prefix laws given in Figure 5. Notice that(z)az.(P + hx|zi.Q) =6 fa(z)az.(P + hx|zi.Q) =f a(z)az.(P + hx|zi.Q) 6=f a(z)az.(P + hx|zi.Q) =f a(z)az.(P + hx|zi.Q) + ax.Q{x/z}(z)az.(P + hx|zi.Q) + ax.Q{x/z}(z)az.(P + hx|zi.Q) + ax.Q{x/z}(z)az.(P + hx|zi.Q) + ax.Q{x/z}

The counter examples given in the proof of (i) of Theorem 12 are special instances of P1 and P2.
The following lemma is crucial to the simple proof of completeness theorem. The properties it describes
are usually called saturation properties.
15

Lemma 28. Suppose Q is in normal form and M is a sequence of match equalities. Thenτ(i) if QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ]τ.Q0 ;αx(ii) if QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ]αx.Q0 ;α(z)(iii) if QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ](z)αz.Q0 ;x/y(iv) if QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ]hx|yi.Q0 ;m(z) x/z(v) if QσM =⇒ =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ∪ {P 1} ` Q = Q + [M ]mx.Q0 ;m(z) x/z(vi) if QσM =⇒ =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ∪ {P 2} ` Q = Q + [M ]mx.Q0 ;α(z) x/z(vii) if QσM =⇒=⇒ Q0 then AS ∪ {T 1, T 2, T 3} ∪ {P 1, P 2} ` Q = Q + [M ]αx.Q0 .
Proof. (i) through (iii) are proved by induction.
x/y(iv) Suppose [Nj ]hxj |yj i.Qj is a summand of Q such that M ⇒ Nj and QσM −→ Q0 is caused byxj σM /yj σM([Nj ]hxj |yj i.Qj )σMy = yj σM . Therefore−→

Qj σM {xj σM /yj σM }. Then Q0 ≡ Qj σM {xj σM /yj σM }, x = xj σM andAS ∪ {T 1, T 2, T 3} ` Q + [M ]hx|yi.Q0=

Q + [M ]hxj σM |yj σM i.Qj σM {xj σM /yj σM }U D1

Q + [M ]hxj σM |yj σM i.Qj σM

M D3

=

Q + [M ]hxj |yj i.Qj

M1

Q + [M ][Nj ]hxj |yj i.Qj

=

=

SD2

=

x/y

τ

Q

τ

If for example QσM =⇒ Q1 −→ Q2 =⇒ Q0 then by (i)AS ∪ {T 1, T 2, T 3} ` Q==

Q + [M ]τ.Q1
Q + [M ]τ.(Q1 + hx|yi.Q2 )T2=

Q + [M ](τ.(Q1 + hx|yi.Q2 ) + hx|yi.Q2 )

M3

=
=
=

Q + [M ]τ.(Q1 + hx|yi.Q2 ) + [M ]hx|yi.Q2
Q + [M ]hx|yi.Q2
Q + [M ]hx|yi.(Q2 + τ.Q0 )

T D3

=

Q + [M ](hx|yi.(Q2 + τ.Q0 ) + hx|yi.Q0 )M3

Q + [M ]hx|yi.(Q2 + τ.Q0 ) + [M ]hx|yi.Q0
Q + [M ]hx|yi.Q0==

This completes the proof of (iv).
m(z)

x/z

(v) Suppose QσM =⇒ Q1 =⇒ Q0 . Then by (iii) and (iv)AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ](z)mz.Q1
andAS ∪ {T 1, T 2, T 3} ` Q1 = Q1 + hx|zi.Q0
ThereforeQ=

Q + [M ](z)mz.(Q1 + hx|zi.Q0 )P1=

Q + [M ]((z)mz.(Q1 + hx|zi.Q0 ) + mx.Q0 )M3

Q + [M ](z)mz.(Q1 + hx|zi.Q0 ) + [M ]mx.Q0
Q + [M ]mx.Q0==

This completes the proof of (v).
(vi) through (vii) are proved similarly.

16

Using the saturation properties, we can establish the promotion properties, so called because theproperties allows one to lift a pair, P and Q, of semantically equivalent processes to a pair, τ.P and τ.Q,
of proof theoretically equal terms.
Lemma 29. Suppose both P and Q are in normal form. The following properties hold:(i) If P ≈f a∪f a Q then AS ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.Q;(ii) If P ≈f a Q then AS ∪ {T 1, T 2, T 3, T 4} ∪ {P 1} ` τ.P = τ.Q;(iii) If P ≈f a Q then AS ∪ {T 1, T 2, T 3, T 4} ∪ {P 2} ` τ.P = τ.Q;(iv) If P ≈ba Q then AS ∪ {T 1, T 2, T 3, T 4} ∪ {P 1, P 2} ` τ.P = τ.Q.
Proof. (i) The proof is done by induction on the sum of the depths of P and Q. Suppose P and Q are
in normal form. Let P be
XXX
[Mi ]αi xi .Pi +[Mi ](x)αi x.Pi +[Mi ]hzi |yi i.Pi
i∈I1

i∈I2

i∈I3

and Q beX

[Nj ]αj xj .Qj +

j∈J1

X

[Nj ](x)αj x.Qj +

j∈J2

X

[Nj ]hzj |yj i.Qj

j∈J3

Suppose further that P ≈f a∪f a Q and [Mi ](x)αi x.Pi is a summand of P . Now([Mi ](x)αi x.Pi )σMi

αi σMi (x)−→Pi σMiαi σM (x)imust be matched up by QσMi =⇒Q0 such that Pi σMi ≈f a∪f a Q0 . Both Pi σMi and Q0 are in normal
0form and d(Pi σMi ) + d(Q ) ≤ d(P ) + d(Q). So AS ∪ {T 1, T 2, T 3, T 4} ` τ.Pi σMi = τ.Q0 by induction
hypothesis. It follows that[Mi ](x)αi x.Pi

M D3

=

T1

[Mi ](x)αi σMi x.Pi σMi=[Mi ](x)αi σMi x.τ.Pi σMi

I.H.

=

[Mi ](x)αi σMi x.τ.Q0

T1[Mi ](x)αi σMi x.Q0=

Therefore [Mi ](x)αi x.Pi + Q = [Mi ](x)αi σMi x.Q0 + Q = Q by (iii) of Lemma 28. Similarly one provesthat [Mi ]αi xi .Pi + Q = Q whenever [Mi ]αi xi .Pi is a summand of P .
Now suppose [Mi ]hxi |yi i.Pi is a summand of P . Then there are two cases. Either([Mi ]hxi |yi i.Pi )σMi

xi σMi /yi σMi−→or

Pi σMi {xi σMi /yi σMi }τ([Mi ]hxi |yi i.Pi )σMi −→ Pi σMi
xi σM /yi σMii
In the first case one has some Q0 such that QσMi=⇒Q0 and Pi σMi {xi σMi /yi σMi } ≈f a∪f a Q0 .
By induction hypothesis AS ∪ {T 1, T 2, T 3, T 4} ` τ.Pi σMi {xi σMi /yi σMi } = τ.Q0 . So

[Mi ]hxi |yi i.Pi

M D3

=

[Mi ]hxi σMi |yi σMi i.Pi σMi

U D1

=

[Mi ]hxi σMi |yi σMi i.Pi σMi {xi σMi /yi σMi }T1=[Mi ]hxi σMi |yi σMi i.τ.Pi σMi {xi σMi /yi σMi }

I.H.

=

[Mi ]hxi σMi |yi σMi i.τ.Q0

T1[Mi ]hxi σMi |yi σMi i.Q0=

Therefore [Mi ]hxi |yi i.Pi + Q = [Mi ]hxi σMi |yi σMi i.Q0 + Q = Q by (iv) of Lemma 28. In the second caseτsome Q0 exists such that Pi σMi {xi σMi /yi σMi } ≈f a∪f a Q0 and either QσMi =⇒ Q0 or QσMi ≡ Q0 . By
17

induction hypothesis τ.Pi σMi {xi σMi /yi σMi } = τ.Q0 . In the first subcase it can be easily shown that[Mi ]hxi |yi i.Pi + Q = Q. In the second subcase one has[Mi ]hxi |yi i.Pi

M D3

=

[Mi ]hxi σMi |yi σMi i.Pi σMi

U D1

=

[Mi ]hxi σMi |yi σMi i.Pi σMi {xi σMi /yi σMi }

T D1

=

[Mi ]hxi σMi |yi σMi i.τ.Pi σMi {xi σMi /yi σMi }

I.H.

=

[Mi ]hxi σMi |yi σMi i.τ.Q0

T D1[Mi ]hxi σMi |yi σMi i.QσMi

=

U3

=

M D3

=

[Mi ]τ.QσMi[Mi ]τ.Q

P
It follows that AS ∪ {T 1, T 2, T 3, T 4} ` P +Q = Q+ i∈I
P [Mi ]τ.Q for some finite indexing sets I. By
Lemma 27, AS ∪ {T 1, T 2, T 3, T 4} ` τ.(P +Q) = τ.(Q+ i∈I [Mi ]τ.Q) = τ.Q. Similarly one can provethat AS ∪ {T 1, T 2, T 3, T 4} ` τ.(P +Q) = τ.P . Hence AS ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.Q.
Theorem 30 (completeness). We have the following completeness results:(i) AS ∪ {T 1, T 2, T 3, T 4} is sound and complete for =f a∪f a ;(ii) AS ∪ {T 1, T 2, T 3, T 4} ∪ {P 1} is sound and complete for =f a ;(iii) AS ∪ {T 1, T 2, T 3, T 4} ∪ {P 2} is sound and complete for =f a ;(iv) AS ∪ {T 1, T 2, T 3, T 4} ∪ {P 1, P 2} is sound and complete for =ba .
Proof. The proof of completeness is almost the same as that of Lemma 29. The only difference is that in
the inductive step, one uses Lemma 29 rather than induction hypothesis! For illustration, let’s assume
that P =f a∪f a Q for normal form processes P and Q. Suppose [Mi ]hzi |yi i.Pi is a summand of P andτ

τ([Mi ]hzi |yi i.Pi )σMi −→ Pi σMi . Then QσMi =⇒ Q0 ≈f a∪f a P 0 . By Lemma 29, AS ∪ {T 1, T 2, T 3, T 4} `τ.P 0 = τ.Q0 , from which it is routine to show that AS ∪ {T 1, T 2, T 3, T 4} ` [Mi ]hzi |yi i.Pi + Q = Q. Thisshould provide enough information about how to establish AS ∪ {T 1, T 2, T 3, T 4} ` P + Q = Q. Similarly
AS ∪ {T 1, T 2, T 3, T 4} ` P + Q = P . Hence AS ∪ {T 1, T 2, T 3, T 4} ` P = Q.

6

Conclusion

The paper has achieved two things. First a general framework is introduced to give a possible classificationof bisimulation congruence relations. The L-bisimilarity covers all familiar bisimulation equivalences. For
instance the bottom element of the bisimulation lattice is the open bisimilarity and the top element of thelattice coincides with the barbed bisimilarity. This interesting phenomenon suggests that open congruenceis usually the strongest congruence whereas the barbed congruence the weakest. An explanation of thephenomenon is this: In the open approach processes are supposed to simulate each other’s actions to thefull extent. The actions not only reveal the channels at which the actions occurs but also the messages
carried by the actions. On the other extreme, the barbed approach only requires bisimilar processes tosimulate each other’s ability to communicate at particular channels. The contents of communications
are irrelevant. The barbed bisimilarity on χ-processes satisfies some unusual equalities not known in thestudies of π-calculus. It departs from the ‘standard bisimilarity’ significantly. The second achievement is
a complete system for each of the L-congruences. This is the first time non-symbolic complete systems arederived for weak observational congruences on finite χ-like processes. There have been other attempts
to axiomatize weak equivalences using non-symbolic approach. Unfortunately all of them have been
unsuccessful.
The approach used in this paper has strong implications to other calculi of mobile processes. The
asymmetric χ-calculus, the Update Calculus without the mismatch combinator, can be investigatedin similar line. The situation is complicated by the presence of restricted updates in the asymmetriclanguage. Preliminary results are reported in [10]. The study of polyadic χ-calculus, the Fusion Calculus
without the mismatch operator, can also benefit from the idea of bisimulation lattice. The top elementof the bisimulation lattice for Fusion processes is the barbed bisimilarity, which is strictly weaker than
the weak hyperbisimilarity, the latter being the same as the open bisimilarity in the fragment of Fusion
Calculus without the mismatch operator. Complete axiomatization systems for barbed equivalence and18

hyperequivalence on Fusion processes without the mismatch combinator can be given using T4 and someversions of P-rules as well as the rules given in [22].
The result of this paper should be of help to the investigation of a non-symbolic approach to axiomatization of π-calculus. The introduction of T4 allows us to promote the complete system for the strong
open congruence on π-processes to one for the weak open congruence. However this system still has todeal with distinctions. This use of distinction is unsatisfactory because it is a disguised form of symbolic
treatment. So one avenue for further study is to see how to eliminate distinctions from the system.
The relationship of this piece of work to the work of Parrow and Victor is as follows:• Parrow and Victor have studied weak hyperbisimilarity ([30]), which is basically the weak open
bisimilarity. We have studied in this paper L-bisimilarities that subsume the weak hyperbisimilarity,
the latter being the smallest L-bisimilarity under the subset inclusion. The largest L-bisimilarity
is the barbed bisimilarity. The definition of barbed bisimilarity considered in this paper is different
from that of the barbed equivalence of Milner and Sangiorgi. The latter is required to be closed
under context only at the very beginning of bisimulation. The definition of the barbed bisimilarity
makes it easy to compare to the L-bisimilarities. Our intuition strongly suggests that the barbed
bisimilarity and the barbed equivalence, which Parrow and Victor have studied, coincide in theabsence of the mismatch operator. But so far we have not be able to formally prove this conjecture.
In the setting of π-calculus, Sangiorgi and Walker have introduced open barbed bisimilarity which
is closed under substitution in every bisimulation step. They have proved that the open barbed
bisimilarity coincides with quasi open bisimilarity that is slightly different from the well known open
bisimilarity. For detail confer [26]. It is clear that the barbed bisimilarity is contained in the barbed
equivalence. Therefore the barbed equivalence is strictly weaker than the weak hyperequivalence.
This result rectifies a mistaken result in [30].
• Parrow and Victor have studied complete axiomatic system for the strong hyperequivalence on
fusion processes ([22]). The results in Section 5.1 are special cases of their results. In the same
paper they have tried to give a complete axiomatic system for the weak hyperequivalence. But thesystem they came up with is incorrect because it lacks of the tau law T4. The fourth tau law plays
an essential role in the semantics of open style congruences.
Acknowledgement
The work reported in this paper has been supported by the National Nature Science Foundation ofChina (69873032) and by the National 863 High-Tech Project (863-306-ZT06-02-2).
The author wishes to thank two anonymous referees for their criticism and suggestions. He also wishes
to thank Zhenrong Yang for proof-reading the paper.

References[1] R. Amadio, I. Castellani, D. Sangiorgi. On Bisimulation for the Asynchronous π-Calculus. CONCUR’96 , Lecture Notes in Computer Science 1119, Springer, 1996.
[2] M. Boreale. On the Expressiveness of Internal Mobility in Name-Passing Calculi. CONCUR ’96 ,Lecture Notes in Computer Science 1119, Springer, 161–178, 1996.
[3] G. Boudol. Asynchrony and the π-calculus. Research Report 1702, INRIA, Sophia-Antipolis, 1992.
[4] Y. Fu. The χ-Calculus. Proceedings of the International Conference on Advances in Parallel andDistributed Computing, 74-81, March 19th-21th, Shanghai, IEEE Computer Society Press, 1997.
[5] Y. Fu. A Proof Theoretical Approach to Communications. ICALP’97 , 325–335, July 7th-11th,
Bologna, Italy, Lecture Notes in Computer Science 1256, Springer, 325-335, 1997.
[6] Y. Fu. Symmetric π-Calculus. Journal of Computer Science and Technology, 13: 202–208, 1998.
[7] Y. Fu. Reaction Graphs. Journal of Computer Science and Technology, 13: 510–530, 1998.
[8] Y. Fu. Bisimulation Lattice of Chi Processes. ASIAN’98 , December 8-10, Manila, The Philippines,
Lecture Notes in Computer Science 1538, Springer, 245–262, 1998.
19

[9] Y. Fu. Variations on Mobile Processes. Theoretical Computer Science, 221: 327-368, 1999.
[10] Y. Fu. Open Bisimulations of Chi Processes. CONCUR’99 , Eindhoven, August 24-27, Lecture Notes
in Computer Science 1664, Springer, 304-319, 1999.
[11] M. Hennessy, R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM ,67: 137–161, 1985.
[12] K. Honda, M. Tokoro. An Object Calculus for Asynchronous Communication. Proc. ECOOP ’91 ,Geneva, 1991.
[13] H. Lin. Complete Inference Systems for Weak Bisimulation Equivalences in the π-Calculus. Proceedings of Sixth International Joint Conference on the Theory and Practice of Software Development,
Lecture Notes in Computer Science 915, Springer, 187–201, 1995.
[14] H. Lin. Unique Fixpoint Induction for Mobile Processes. CONCUR ’95, Lecture Notes in Computer
Science 962, Springer, 88–102, 1995.
[15] H. Lin. Complete Proof Systems for Observation Congruences in Finite-Control π-Calculus. ICALP’98, Lecture Notes in Computer Science 1443, Springer, 443–454, 1998.
[16] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[17] R. Milner, J. Parrow, D. Walker. A Calculus of Mobile Processes. Information and Computation,
100: 1–40 (Part I), 41–77 (Part II), Academic Press.
[18] R. Milner, D. Sangiorgi. Barbed Bisimulation. 19th ICALP , Lecture Notes in Computer Science 623,
Springer, 685–695, 1992.
[19] M. Merro, D. Sangiorgi. On Asynchrony in Name-Passing Calculi. ICALP’98 , Lecture Notes in
Computer Science 1443, Springer, 1998.
[20] J. Parrow, B. Victor. The Update Calculus. AMAST’97, Sydney, December 13-17, 1997.
[21] J. Parrow, B. Victor. The Fusion Calculus: Expressive and Symmetry in Mobile Processes. LICS’98 ,1998.
[22] J. Parrow, B. Victor. The Tau-Laws of Fusion. CONCUR’98 , Lecture Notes in Computer Science,
1998.
[23] D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms,
PhD thesis, Department of Computer Science, University of Edinburgh, 1993.
[24] D. Sangiorgi. A Theory of Bisimulation for π-Calculus. CONCUR 93 , Lecture Notes in Computer
Science 715, Springer, 1993.
[25] D. Sangiorgi. π-Calculus, Internal Mobility and Agent-Passing Calculi. Theoretical Computer Science, 235–274, 1996[26] D. Sangiorgi, D. Walker. On Barbed Equivalence in π-Calculus. CONCUR’01 , 292-304, Lecture
Notes in Computer Science, 2001.
[27] B. Thomsen. A Calculus of Higher Order Communicating Systems. POPL ’89 , ACM, 143–154, 1989.
[28] B. Thomsen. Plain CHOCS—A Second Generation Calculus for Higher Order Processes. Acta Informatica, 30: 1–59, 1993.
[29] B. Thomsen. A Theory of Higher Order Communicating Systems. Information and Computation,
116: 38–57, 1995.
[30] B. Victor, J. Parrow. Concurrent Constraints in the Fusion Calculus. ICALP’98 , Lecture Notes in
Computer Science, 1998.
[31] D. Walker. π-Calculus Semantics for Object-Oriented Programming Languages, TACS ’91 , Lecture
Notes in Computer Science 526, Springer, 532–547, 1991.
[32] D. Walker. Objects in the π-Calculus, Information and Computation, 116: 253–271, 1995.

20