Bisimulation Lattice of Chi Processes?
Yuxi Fu??
Department of Computer Science
Shanghai Jiaotong University, Shanghai 200030, China

Abstract. Chi calculus was proposed as a process algebra that has auniform treatment of names. The paper carries out a systematic studyof bisimilarities for chi processes. 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 forms a four element lattice
and that well-known bisimilarities for chi processes fit into the latticehierarchy. The four distinct L-bisimilarities give rise to four congruence
relations. Complete axiomatization system is given for each of the four
relations. The bisimulation lattice of asynchronous chi processes and thatof asymmetric chi processes are also investigated. It turns out that theformer consists of two elements while the latter twelve elements. Finally
it is pointed out that the asynchronous asymmetric chi calculus has abisimulation lattice of eight elements.

The χ-calculus ([4]) was introduced with two motivations in mind. One is toremove the ad hoc nature of prefix operation in π-calculus ([11]) by having a uniform treatment of names ([3]), thus arriving at a conceptually simpler language.
The second is to materialize a communication-as-cut-elimination viewpoint ([5]),therefore taking up a proof theoretical approach to concurrency theory, an approach that has been proved very fruitful in the functional world. Independently
Parrow and Victor have come up with essentially the same language, Update
Calculus as they term it ([13]). They share, we believe, the first motivation but
have quite a different 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 thelatter takes an information exchange or information update viewpoint. The algebraic theory of the language has been investigated in the above mentioned papers. Parrow and Victor have looked into strong bisimilarity and axiomatizationof it for Update Calculus, while Fu has examined an observational bisimilarityfor χ-processes. More recently, Parrow and Victor have proposed Fusion Calculus([14, 17]), which is a polyadic version of χ-calculus. The authors have also studied an observational equivalence called weak hyperbisimilarity. What we know
about the language, albeit little, tells us that it can practically do everything π
can do and its algebraic properties are just as satisfactory. The studies carriedout so far are however preliminary.
?
??

ASIAN ’98 , Lecture Notes in Computer Science 1538, 245-262, 1998.
Supported by the National Nature Science Foundation of China.

The objective of this paper is to continue our examination of the algebraic
theory of χ-calculus. Section 1 reviews the operational semantics of χ. Section 2
defines L-bisimilarities and investigates their relationship. Section 3 gives alternative characterizations of L-bisimilarities. Section 4 presents a complete axiomatization system for each of the congruence relations induced by the fourL-bisimilarities. The next three sections look into the L-bisimilarities of asynchronous, asymmetric, asynchronous asymmetric χ-calculi respectively.

1

Operational Semantics

In π-calculus there are two kinds of closed names, one has dummy names as x
in m(x).P and local names as x in (x)mx.P . In simple words, the χ-calculus
is obtained from π-calculus by unifying these names. This identification forces
a unification of input and output prefix operations. The two π-processes justmentioned then turn into (x)m[x].P and (x)m[x].P respectively. In the resulting calculus communications are completely symmetric as exemplified by thefollowing reductions:τm[x].P |m[x].Q −→ P |Qτ(x)(R|(m[y].P |m[x].Q)) −→ R[y/x]|(P [y/x]|Q[y/x]), where y 6= xτ(x)m[x].P |(y)m[y].Q −→ (z)(P [z/x]|Q[z/y]), where z is fresh
The reader is referred to [3–6, 13, 14, 17] for more explanations and examples.
Let N be a set of names, ranged over by lower case letters. N , the set ofconames, denotes {x | x ∈ N }. The following conventions will be used: α ranges
over N ∪ N , µ over {τ } ∪ {α[x], αx | x ∈ N }, and δ over {τ } ∪ {α[x], αx, [y/x] |x, y ∈ N }. The set C of χ-processes are defined by BNF as follows:
P := 0 | α[x].P | P |P | (x)P | [x=y]P | P +P
The process α[x].P is in prefix form. Here α or α is the subject name, and x
the object name, of the prefix. The composition operator “|” is standard. In(x)P the name x is declared local; it cannot be seen from outside. The set ofglobal names, or nonlocal names, in P is denoted by gn(P ). We will adopt the
α-convention saying that a local name in a process can be replaced by a freshname without changing the syntax of the process. The choice combinator ‘+’
is well-known. The process P +Q acts either as P or as Q exclusively. In thispaper 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 ([4])
or in terms of a labeled transition system ([3]). Here we opt for a pure transition
semantics as it helps to present our results with clear-cut proofs. The labeledtransition system given below defines an early semantics. The reason to use an
early semantics is that the definition of weak bisimulation is more succinct inearly semantics than in late semantics. In the following formulation, symmetricrules are systematically omitted:δδP −→ P 0

P −→ P 0α[x]α[x].P −→ P

Sqn

δ[x=x]P −→ P 0

α[x]

αx

P −→ P 0 Q −→ Q0
Cmm0
τP |Q −→ P 0 |Q0
α[x]

[y/x]

δ

(x)P −→ (x)P 0[y/x]

P |Q −→ P 0 |Q[y/x]

Cmp1

αx

αx

α[x]

α[x]

α[y]

P −→ P 0 Q −→ Q0 x 6= y[y/x]

P |Q −→ P 0 [y/x]|Q0 [y/x]α[x]P −→ P 0 x 6∈ n(δ)
Loc0

Sum

P −→ P 0 Q −→ Q0 x 6∈ gn(P |Q)
Cmm1
τP |Q −→ (x)(P 0 |Q0 )P −→ P 0 Q −→ Q0
Cmm2
τP |Q −→ P 0 |Q0δδ

P +Q −→ P 0

P −→ P 0µ

P −→ P 0
Cmp0µ
P |Q −→ P 0 |Q

Cnd

Cmm3

[y/x]

P −→ P 0 x 6∈ {α, α}αyLoc1(x)P −→ P 0 [y/x]P −→ P 0
Loc2
τ(x)P −→ P 0[y/x]

Labeled transitions of the form −→, called update transitions, are first introduced in [3, 13] to help define communications in a transition semantics. In applying Loc1 local names need be renamed if necessary to prevent y from being
captured. In Loc0 , n(δ) denotes the set of names appeared in δ. The notation[y/x] occurred in P [y/x] for example is an atomic substitution of y for x. A
general substitution σ is the composition of atomic substitutions, whose effect isdefdefined 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 isvacuous.
The next lemma collects some technical results whose proofs are simple inductions on derivation.
µµσ

Lemma 1. (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 σ.
[y/x]

[x/y]

(iv) If P =⇒ P 0 then P =⇒ P 0 [x/y].
αxαz(v) P −→ P 0 if and only if P −→ P1 for some fresh z such that P 0 ≡ P1 [x/z].
ay τ
τ ay
(vi) Suppose a 6∈ gn(P ). If (x)(P |a[x]) −→−→ P 0 then (x)(P |a[x]) −→−→ P 0 .
[y/x]

τ

(vii) Suppose a 6∈ gn(P ). If (x)(P |a[x]) −→ P 0 |a[y] then P −→ P 0 .
τµLet =⇒ be the reflexive and transitive closure of −→. We will write =⇒
b
µ
b
µ
µ
δ
δ
δ
δ
(=⇒) for =⇒−→=⇒ (=⇒−→=⇒). We will also write =⇒ (=⇒) for =⇒ (=⇒)
if µ 6= τ (δ 6= τ ) and for =⇒ otherwise. A sequence of names x1 , . . . , xn will beabbreviated to x; and consequently (x1 ) . . . (xn )P will be abbreviated to (x)P .
When the length of x is zero, (x)P is just P .

2Bisimulation Lattice

We introduce in this section L-bisimilarities, which are refinement of the local
bisimilarity of [4]. The reason to study L-bisimilarities is that they provide aframework to understand bisimilarity relations of interest.
In a symmetric calculus such as χ, it does not make much sense to say that anaction with positive, respectively negative, subject name is an input, respectively
output, action. An action is an input or output, depending on if the object nameis being received or being sent out. Let o denote the set {a[x] | a, x ∈ N } of
output actions, o the set {a[x] | a, x ∈ N } of co-output actions, i the set {ax |a, x ∈ N } of input actions, i the set {ax | a, x ∈ N } of co-input actions and u theset {[y/x] | x, y ∈ N } of updates. Let L stand for {∪S | S ⊆ {o, o, i, i, u}∧S 6= ∅}.
Definition 2. 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 forb
φφ ∈ L ∪ {τ } then there exists some Q0 such 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 L-bisimilarities collapse to four distinct
relations. In the rest of this section let L be an arbitrarily fixed element of L.
First we establish a few technical lemmas. The next one follows directly fromdefinition.
Lemma 3. If P =⇒ P1 ≈L Q and Q =⇒ Q1 ≈L P then P ≈L Q.
φ

φ

For φ ∈ L, let hφi be a process such that (i) hφi −→ 0 and (ii) if hφi −→ A thenA ≡ 0.
Lemma 4. Suppose a 6∈ gn(P |Q). Then (i) (x)(P |a[x]) ≈L (x)(Q|a[x]) implies
P ≈L Q; and (ii) P |a[x] ≈L Q|a[x] implies P ≈L Q.
φ

Proof. (i) Suppose φ ∈ L and n(φ) ∩ gn(P |Q) = ∅. As (x)(P |a[x])|a[x].hφi =⇒φ(P |0)|0, Q1 exists such that (x)(Q|a[x])|a[x].hφi =⇒ (Q1 |0)|0 ≈L (P |0)|0, whichax
implies (x)(Q|a[x]) =⇒ Q1 |0 ≈L P |0, which in turn implies Q =⇒ Q1 . Similarly
P1 exists such that P =⇒ P1 ≈L Q. By Lemma 3, P ≈L Q. (ii) can be proved
similarly.
tuLemma 5. 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 ∈ gn(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(φ) ∩ gn(P |Q) = ∅. By definition the actions (x)(P |(b[y]|b[x].hφi)) =⇒P [y/x]|(0|0) must be matched up by
φ(x)(Q|(b[y]|b[x].hφi)) =⇒ Q1 |(0|0).

(1)

τ

If (x)(Q|(b[y]|b[x].hφi)) −→ (x0 )(Q2 |(b[y]|b[x0 ].hφi)) then by symmetry and αconvention the reduction is the same asτ(x)(Q|(b[y]|b[x].hφi)) −→ (x)(Q3 |(b[y]|b[x].hφi))τsuch that Q −→ Q3 . It follows that (1) can be factorized as follows(x)(Q|(b[y]|b[x].hφi)) =⇒ (x)(Q0 |(b[y]|b[x].hφi))τ−→ Q0 [y/x]|(0|hφi)φ=⇒ Q1 |(0|0)
for some Q0 and Q1 such that Q =⇒ Q0 and Q0 [y/x] =⇒ Q1 ≈L P [y/x]. By
Lemma 1, Q[y/x] =⇒ Q0 [y/x]. Similarly P1 exists such that P [y/x] =⇒ P1 ≈L
Q[y/x]. By Lemma 3, P [y/x] ≈L Q[y/x].
tu
By definition the L-bisimilarity is closed under localization and composition.
Using Lemma 5 it can be easily seen that ≈L is closed under prefix operation.
Theorem 6. 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; and (iv) [x=y]P ≈L [x=y]Q.
We investigate next the order structure of L-bisimilarities.
Theorem 7. The following properties hold of the L-bisimilarities:(i) ≈o 6⊆≈o ; ≈o 6⊆≈o . (ii) ≈L ⊆≈u . (iii) ≈L ⊆≈i =≈i .
Proof. (i) It is obvious that (x)a[x].(b)(b[x]|b[z]) 6≈o a[z]+(x)a[x].(b)(b[x]|b[z]).
It takes a while to see that (x)a[x].(b)(b[x]|b[z]) ≈o a[z]+(x)a[x].(b)(b[x]|b[z]).
[y/x](ii) To prove ≈L ⊆≈u , one only has to show that if P ≈L Q and P −→ P 0
[y/x]

[y/x]

then Q0 exists such that Q =⇒ Q0 and P 0 ≈L Q0 . Now P −→ P 0 implies thatτ(x)(P |a[x]) −→ P 0 |a[y] for a fresh a. So (x)(Q|a[x]) =⇒ Q0 |a[y] for some Q00such that P |a[y] ≈L Q0 |a[y]. It follows from Lemma 4 that P 0 ≈L Q0 . Clearly(x)(Q|a[x]) =⇒ Q0 |a[y] can be factorized asτ(x)(Q|a[x]) =⇒ (x)(Q1 |a[x]) −→ Q2 |a[y] =⇒ Q0 |a[y],
τ

[y/x]

where Q =⇒ Q1 . By (vii) of Lemma 1, (x)(Q1 |a[x]) −→ Q2 |a[y] implies Q1 −→[y/x]

Q2 . Hence Q =⇒ Q0 .
αx(iii) Assume P ≈L Q and P −→ P 0 . Suppose φ ∈ L and n(φ) ∩ gn(P |Q) = ∅.
τ
Now P |(α[z]+hφi) −→ P1 |0 for some fresh z such that P 0 ≡ P1 [x/z]. There has
αz
to be some Q1 such that Q|(α[z]+hφi) =⇒ Q1 |0 ≈L P1 |0. So Q =⇒ Q1 ≈L P1 .
αx
0Therefore Q =⇒ Q1 [x/z] ≈L P1 [x/z] ≡ P by Lemma 1 and Lemma 5. Hence≈L ⊆≈i =≈i .
tu≈i ,≈i ,≈u

*





≈o

H
Y
HH
H

≈o

H
Y
HH

H

≈o∪o

*





Fig. 1. The Bisimulation Lattice of Chi Processes

In the proof of (iii) of the above theorem, we need to use a fresh name zταxbecause we cannot conclude R −→ R0 from R|α[x] −→ R0 |0. It may well be thatα[x]R participates in the communication by performing R −→ R0 .
Let L(χ) be {≈L | L ∈ L}, the set of all L-bisimilarities. L(χ) is a partial
order when equipped with ⊆. For ≈L1 , ≈L2 ∈ L(χ), ≈L1 ∪L2 is the infimum. Theorem 7 says that L(χ) is a four element lattice. The diagram in Fig. 1 is a pictorial
representation of the lattice. In the diagram each node is the principal representative of a number of L-bisimilarities that boil down to a same relation. An
arrow indicates a strict inclusion. The bottom element is represented by ≈o∪owhile the top element is by ≈i =≈i =≈u . We will call (L(χ), ⊆) the bisimulation
lattice of χ-processes. The lattice structure suggests that the ability to observe
output actions is stronger than that to observe input actions. One way to understand this is that the effect of an output action is unknown whereas that ofan input action has already been delimited.

3

Alternative Characterization

The definition of L-bisimilarity is natural but intractable. It contains universal
quantifications over both processes and names. In this section alternative characterizations of the four distinct L-bisimilarities are presented. For each of therelations, an open style bisimilarity is shown to coincide with 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. Firstwe will see how barbed bisimilarity fits into the lattice hierarchy.
3.1

Barbed Bisimilarity

Barbed bisimilarity ([12]) seems to be the weakest bisimulation equivalence proposed so far. It applies to a whole range of process calculi and therefore acts as
a convenient tool to study relationships between different calculi. The relationship of barbed bisimilarity to other bisimilarities is itself an interesting question.
Usually it is easy to show that a given bisimilarity is included in the barbed one.
The difficulty is in deciding if the inclusion is strict. This section answers thequestion for χ-processes.

αxDefinition 8. A process P is strongly barbed at a, notation P ↓a, if P −→ P 0
α[x]or P −→ P 0 for some P 0 such that a ∈ {α, α}. P is barbed at a, notation
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.
Definition 9. 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 such that (x)(Q|R) =⇒ Q0 and
P 0 RQ0 . The barbed bisimilarity ≈b is the largest barbed bisimulation.
The next result locates ≈b in the bisimulation lattice.
Theorem 10. ≈b is the same as ≈i .
Proof. As ≈i is clearly barbed, ≈i ⊆≈b . To prove the reverse inclusion, first
notice that ≈b is closed under substitution, the proof of which is similar toαxthat of Lemma 5. Now suppose P ≈b Q and P −→ P 0 . By (v) of Lemma 1
αz
P −→ P1 for some fresh z such that P 0 ≡ P1 [x/z]. Let a be fresh. Nowττ
P |(α[z].a[a]|a[a]) −→−→ P1 |(0|0). This sequence of reductions must be matched
up by Q|(α[z].a[a]|a[a]) =⇒ Q1 |(0|0) ≈b P1 |(0|0). There are only two ways for
α[z]

αz

Q to evolve into Q1 : either Q =⇒ Q1 or Q =⇒ Q1 . The former is impossiαz
ble because z is fresh. Hence Q =⇒ Q1 ≈b P1 . It follows from Lemma 1 thatαx0Q =⇒ Q1 [x/z] ≈b P1 [x/z] ≡ P . Conclude that ≈b ⊆≈i .
tu
3.2

Open Bisimilarity

Open bisimilarity is proposed by Sangiorgi in [16] for π-processes as a “correctionof late bisimulation”. This section defines open bisimilarity for χ-processes andrelates it to one of the L-bisimilarities.
Definition 11. Let R be a binary symmetric relation on C. It is called an openδbisimulation if whenever P RQ then for any substitution σ it holds that if P σ −→bδ
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 12. ≈open is closed under localization and composition.
This easy lemma can be proved by constructing appropriate bisimulations.
Theorem 13. ≈open coincides with ≈o∪o .
Proof. By Lemma 5 and the proof of Theorem 7, (o ∪ o)-bisimilarity is an opentubisimulation. By Lemma 12, open bisimilarity is an (o ∪ o)-bisimulation.

The definition of open bisimilarity makes it easy to give axiomatization system for finite χ-processes. Theorem 13 enables us to axiomatize the bottom
element of the bisimulation lattice L(χ). In order to do the same for the otherthree elements of the bisimulation lattice, one would like to characterize thesethree L-bisimilarities in an ‘open’ style, so to speak. This is precisely what weare going to do next. The intuition for the following definition comes from theexample given in the proof of (i) of Theorem 7.
Definition 14. Let R be a binary symmetric relation on C. It is called an open
i-bisimulation (open o-bisimulation, open o-bisimulation) if whenever P RQ thenfor any substitution σ it holds thatφ(i) if P σ −→ P 0 for φ ∈ i∪i∪u∪{τ } (φ ∈ o∪i∪i∪u∪{τ }, φ ∈ o∪i∪i∪u∪{τ })bφthen Q0 exists such that Qσ =⇒ Q0 and P 0 RQ0 ; and
a[x]

α[x]

a[x]

(ii) if P σ −→ P 0 (P σ −→ P 0 , P σ −→ P 0 ) then some Q0 exists such that
a[x]

α[x]

a[x]

αz [x/z]

P 0 RQ0 and either Qσ =⇒ Q0 (Qσ =⇒ Q0 , Qσ =⇒ Q0 ) or Qσ =⇒ =⇒ Q0
az [x/z]az [x/z](Qσ =⇒ =⇒ Q0 , Qσ =⇒ =⇒ Q0 ) for some fresh z.
The open i-bisimilarity (open o-bisimilarity, open o-bisimilarity), denoted by≈iopen (≈oopen , ≈oopen ), is the largest open i-bisimulation (open o-bisimulation,
open o-bisimulation).
The next theorem explains the reason to have Definition 14.
Theorem 15. (i) ≈oopen =≈o ; (ii) ≈oopen =≈o ; (iii) ≈iopen =≈i .
α[x]Proof. It is enough to see how to establish (iii). Suppose P ≈i Q and P −→ P 0 .
[x/z]

For a fresh name z one has P |α[z] −→ P 0 |0. As ≈i =≈u , Q0 exists such that
[x/z]

α[x]

Q|α[z] =⇒ Q0 |0 ≈i P 0 |0. There are only two possibilities: either Q =⇒ Q0 ≈i P 0
αz [x/z]or Q =⇒ =⇒ Q0 ≈i P 0 . Hence ≈i ⊆≈iopen by Lemma 5.
To prove the reverse inclusion we use the fact that ≈iopen is by definition closed
under substitution. We only have to show that the composition and localization
operators preserve the relation ≈iopen . To prove that {((v)(P |R), (v)(Q|R)) |P ≈iopen Q} is an open i-bisimulation, it is sufficient to examine the cases where
P performs an output action. We consider only one case:αz– Suppose that (v)(P |R) −→ (u)(P 0 [z/y]|R[z/y]), where y ∈ {v}, is derived
α[y]

α[y]

from P −→ P 0 by applying rule Loc1 . Suppose P −→ P 0 is matched up
[y/w]

αw

αz

by Q =⇒ Q1 =⇒ Q0 for some Q1 , Q0 and fresh w. By Lemma 1, Q =⇒[y/z]

Q1 [z/w] =⇒ Q0 [z/w][y/z] ≡ Q0 [y/z] as w 6∈ gn(Q0 ). By (iv) of Lemma 1,
αz

[z/y]

Q =⇒ Q1 [z/w] =⇒ Q0 [y/z][z/y] ≡ Q0 [z/y]. It follows thatαz(v)(Q|R) =⇒ (v)(Q1 [z/w]|R) =⇒ (u)(Q0 [z/y]|R[z/y])αzmatches up (v)(P |R) −→ (u)(P 0 [z/y]|R[z/y]).

The closure property enables us to conclude that ≈iopen is an i-bisimulation. utThe open style bisimilarities are particularly suitable for χ-like process calculi
in which names are uniform.

4

Axiomatization

The L-bisimilarities are not congruence relations. To get a congruence relationfrom ≈L we use the standard approach.
ττDefinition 16. P =L Q if and only if P ≈L Q and whenever P −→ P 0 (Q −→ττQ0 ) then Q0 (P 0 ) exists such that Q =⇒ Q0 (P =⇒ P 0 ) and P 0 ≈L Q0 .
We will call =L the L-congruence on χ-processes. According to the bisimulation lattice, there are only four distinct L-congruence relations. The aim of thissection is to give complete axiomatization systems for all the four distinct Lcongruence relations. In this section we omit most of the proofs since they arevery much similar to the corresponding proofs in [7, 10]. In the axiomatization weneed a prefix operation that generalizes the standard τ -operation. It is defined
as follows:def[y|x].P = (a)(a[y]|a[x].P ) where a is fresh.
The next result is known as Hennessy Lemma. It is very useful in the study ofaxiomatization systems.
Lemma 17. P ≈L Q if and only if either [x|x].P =L Q or P =L Q or P =L
[x|x].Q.
For purpose of axiomatization, let π and γ range over {α[x], [y|x] | x, y ∈ N }.
In the rest of this section M and N denote finite lists of match equalities x=y.
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 wewrite M ⇔ N . If M is an empty list, it plays the role of logical truth, in whichcase [M ]P is just P . Clearly a list M of match equalities defines an equivalence
relation on the set n(M ) of names appeared in M . We use σM to denote anarbitrary substitution that replaces all members of an equivalence class by arepresentative of that class.
In [16] Sangiorgi presents a complete system for strong open congruence on
π-processes. Parrow and Victor consider in their paper ([13]) two axiomatization
systems for strong hyperbisimilarity, one with match operator and one without
match operator. In Fig. 2 a conditional equational system AS is defined together
with some derived rules and their justifications. The expansion law is the following equation:PPπi =ai [xi ][Mi ][Nj ](x)(y)[ai =bj ][xi |yj ].(Pi |Qj )+j [yj ]
Pγπji=b=ai [xi ]j [Nj ](y)γj .(P |Qj ) +γj =bj [yj ] [Mi ][Nj ](x)(y)[ai =bj ][xi |yj ].(Pi |Qj )i [Mi ](x)πi .(Pi |Q) +P |Q = PL1(x)0 = 0L2(x)α[y].P = 0x ∈ {α, α}L3(x)α[y].P = α[y].(x)Px 6∈ {y, α, α}L4(x)(y)P = (y)(x)PL5(x)[y=z]P = [y=z](x)Px 6∈ {y, z}
L6(x)(P +Q) = (x)P +(x)QL7(x)[x=y]P = 0L8(x)[y|x].P = [y|y].P [y/x]x 6= yL9(x)[y|z].P = [y|z].(x)Px 6∈ {y, z}
M1[M ]P = [N ]P
if M ⇔ N
M2[x=y]P = [x=y]P [y/x]M3[x=y](P +Q) = [x=y]P +[x=y]Q
S1
P +0 = P
S2
P +Q = Q+P
S3
P +(Q+R) = (P +Q)+R
S4[x=y]P +P = P
U1[y|x].P = [x|y].P
U2[x|x].P = [y|y].P
U3[y|x].P = [y|x].[x=y]PExpansion Law
LD1(x)[x|x].P = [y|y].(x)PU2 and L9MD1[x=y].0 = 0
S1 and S4MD2[x=x].P = P
M1
MD3[M ]P = [M ](P σM )M2
SD1
P +P = PMD2 and S4
SD2[M ]P +P = P
S-rulesUD1[y|x].P = [y|x].P [y/x]U3 and M2

Fig. 2. Axiom System AS and its Derived Rules

P
P
where P is i [Mi ](x)πi .Pi and Q is j [Nj ](y)γj .Qj . Rules concerning equivalence and congruence relations have been omitted. This is Victor and Parrow’ssystem without mismatch. The only difference is that we use a symmetric update
prefix operator.
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 .
R
When no confusion arises, we simply write P = Q. We will also write P = Q toindicate that R is the major axiom applied to derive P = Q.
P
Definition
18. A processi∈I1 [Mi ]αi [xi ].Pi +P
P P is in normal form if P ≡
[M
](x)α
[x].P
+
[M
][z
|y
].P
such
that
x
does
not
appear in P and
i
i
i
i
i i
i
i∈I2
i∈I3
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 of a process measures the maximal length of nested prefixes in the process. The structural definition goes as follows: (i) d(0) = 0;T1
α[x].[y|y].P = α[x].P
T2
P + [y|y].P = [y|y].P
T3
α[x].(P + [y|y].Q) = α[x].(P + [y|y].Q) + α[x].Q
TD1[x|z].[y|y].P = [x|z].P
TD2[x|z].(P + [y|y].Q) = [x|z].(P + [y|y].Q) + [x|z].Q
O1 (z)m[z].(P + [x|z].Q) = (z)m[z].(P + [x|z].Q) + m[x].Q x 6= z
O2 (z)m[z].(P + [x|z].Q) = (z)m[z].(P + [x|z].Q) + m[x].Q x 6= z
O3 (z)α[z].(P + [x|z].Q) = (z)α[z].(P + [x|z].Q) + α[x].Q x 6= z

Fig. 3. The Tau Laws and the Output Laws

(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)}; (vii) d([x|y].P ) = 1+d(P ).
Lemma 19. In AS each process P is provably equal to some P 0 in normal form
such that d(P 0 ) ≤ d(P ).
We need the χ-version of the well-known tau laws as given in Fig. 3. TD1 andTD2 are derivable from T1 and T3 respectively.
The tau laws are enough to characterize =o∪o . To get complete systems forthe other three L-congruence relations, we need what we call output laws O1,O2 and O3 given in Fig. 3.
The following lemma is crucial to the proof of the completeness theorem.
Lemma 20. Suppose Q is in normal form. Thenτ(i) if QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ][x|x].Q0 for each x;α[x](ii) if QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ]α[x].Q0 ;αz(iii) if z 6∈ gn(Q) ∪ n(M ) and QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q =0
Q + [M ](z)α[z].Q ;[x/y](iv) if QσM =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + [M ][x|y].Q0 ;mz [x/z](v) if z 6∈ gn(Q) ∪ n(M ) and QσM =⇒ =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ∪ {O1} `Q = Q + [M ]m[x].Q0 ;mz [x/z](vi) if z 6∈ gn(Q) ∪ n(M ) and QσM =⇒ =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ∪ {O2} `Q = Q + [M ]m[x].Q0 ;αz [x/z](vii) if z 6∈ gn(Q) ∪ n(M ) and QσM =⇒ =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ∪ {O3} `Q = Q + [M ]α[x].Q0 .
Proof. (i) through (iv) are proved by inductions on derivation. (v) through (vii)
are proved using (iii) and (iv).
tuTheorem 21. We have the following completeness results:(i) AS ∪ {T 1, T 2, T 3} is sound and complete for =o∪o ;(ii) AS ∪ {T 1, T 2, T 3} ∪ {O1} is sound and complete for =o ;(iii) AS ∪ {T 1, T 2, T 3} ∪ {O2} is sound and complete for =o ;(iv) AS ∪ {T 1, T 2, T 3} ∪ {O3} is sound and complete for =i .

Proof. The soundness part is clear.
(i) Suppose P and Q are in normal form and P =o∪o Q. We prove the completeness by induction on the sum of the depths of P and Q. Let [Mi ](x)αi [x].Pi
αi σM xbe a summand of P . Now ([Mi ](x)αi [x].Pi )σMi −→i Pi σMi must be matched
αi σM xup by QσMi =⇒i Q0 such that Pi σMi ≈o∪o Q0 . By Lemma 17, we know thateither [y|y].Pi σMi =o∪o Q0 or Pi σMi =o∪o Q0 or Pi σMi =o∪o [x|x].Q0 . Suppose Pi σMi =o∪o [y|y].Q0 is the case. Both Pi σMi and [y|y].Q0 are in normal
form and d(Pi σMi ) + d([y|y].Q0 ) < d(P ) + d(Q). So by induction hypothesis
Pi σMi = [y|y].Q0 . It follows that
M D3[Mi ](x)αi [x].Pi = [Mi ](x)αi σMi [x].Pi σMi
I.H.

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

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

Hence [Mi ](x)αi [x].Pi + Q = [Mi ](x)αi σMi [x].Q0 + Q = Q by (iii) of Lemma 20.
The situation is the same when P 0 =o∪o Q0 or P 0 =o∪o [x|x].Q0 . It can besimilarly proved that [Mi ]αi [xi ].Pi + Q = Q, respectively [Mi ][xi |yi ].Pi + Q = Q,
whenever [Mi ]αi [xi ].Pi , respectively [Mi ][xi |yi ].Pi , is a summand of P . Conclude
that P + Q = Q. Symmetrically P + Q = P . Hence P = Q.
(iv) Let P and Q be in normal form and P =i Q. Suppose([Mi ]αi [xi ].Pi )σMi
αi σM zαi σMi [xi σMi ]−→Pi σ M i[xi σM /z]

is matched up by QσMi =⇒i Q1 =⇒i Q0 such that Pi σMi ≈i Q0 . By Theorem 13 this is the only situation not covered by the proof of (i). By Lemma 17,
either [x|x].Pi σMi =i Q0 or Pi σMi =i Q0 or Pi σMi =i [x|x].Q0 . Now suppose[x|x].Pi σMi =i Q0 is the case. Both [x|x].Pi σMi and Q0 are in normal form. So
by induction hypothesis [x|x].Pi σMi = Q0 . Therefore[Mi ]αi [xi ].Pi = [Mi ]αi σMi [xi σMi ].Pi σMi= [Mi ]αi σMi [xi σMi ].Q0 .
Thus [Mi ]αi [xi ].Pi + Q = [Mi ]αi σMi [xi σMi ].Q0 + Q = Q by (vii) of Lemma 20.
The rest of the proof can be safely omitted.
tu5

Asynchronous Chi Calculus

In the world of π-calculus, attention has been paid to an asynchronous versionof the language ([8, 2, 1]). It has been argued that it has the same expressive
power as the synchronous one. There is also a case for asynchronous χ-calculus.
Merro has recently given a fully abstract translation from the asynchronous χto the asynchronous π ([9]). One hopes to establish that χ and π have the same
expressive power by relating χ to its asynchronous cosine. As one would expect
the asynchronous χ is defined as follows:
P := 0 | a[x].P | a[x] | P |P | (x)P | [x=y]P | P +P

The operational semantics remains unchanged. So does the definition of Lbisimilarity. Lemma 5 and Theorem 6 still hold. But the bisimulation latticeshrinks.
Theorem 22. ≈o ⊂≈o =≈u =≈i =≈i . The inclusion is strict.
Proof. The proofs of the equivalence ≈u =≈i =≈i and the strictness of the inclusion are as before. It remains to show that ≈L ⊆≈o for all L-bisimilarities
a[x]≈L . Now suppose P ≈L Q and P −→ P 0 . Let R be a[x]+hφi such that φ ∈ Lτand n(φ) ∩ gn(P |Q) = ∅. Then P |R −→ P 0 |0. It follows that Q0 exists sucha[x]τthat Q|R −→ Q|0 and P 0 ≈L Q0 . There are two cases: Either Q =⇒ Q0 or
[x/z]

az

Q =⇒ Q2 =⇒ Q0 for some fresh z. In the latter case, notice that no action
is causally dependent on the action az. So all the rest of the actions can be
performed before the action at that particular a happens. But then the update[x/z]−→ becomes a communication in which a local name is substantiated by x.
It follows that the delayed action at that particular a must be a[x]. That is
az

a[x]

[x/z]

a[x]

Q =⇒ Q2 =⇒ Q0 can be rearranged as Q =⇒ Q0 . So in either case P −→ P 0 isa[x]matchable by Q =⇒ Q0 .

tuConsequently the bisimulation lattice of the asynchronous χ contains only
two elements.

6

Asymmetric Chi Calculus

The simplicity of the lattice L(χ) is due essentially to the symmetry of thelanguage. If we insist that there is a difference between an action with a positive
subject name and an action with a negative subject name then an asymmetricversion of χ-calculus results. This is the Update Calculus of Parrow and Victor.
The operational semantics of the asymmetric χ-calculus is defined similarly
as is for symmetric χ. The rule Sqn, Cnd and Sum remain unchanged. Other
rules are given below:µP −→ P 0 if µ = m(x) then x 6∈ gn(Q)Cmp0µP |Q −→ P 0 |Q
[y/x]

(y/x]

P −→ P 0[y/x]

P |Q −→ P 0 |Q[y/x]mx

P −→ P 0 y 6∈ gn(Q)
Cmp1

m[x]

P −→ P 0 Q −→ Q0
Cmm0
τP |Q −→ P 0 |Q0
m[x]

m[x]

P −→ P 0 Q −→ Q0
Cmm2
τP |Q −→ P 0 |Q0(y/x]

P |Q −→ P 0 |Q[y/x]

Cmp2

m(x)

mx

P −→ P 0 Q −→ Q0 x 6∈ gn(P )Cmm1τP |Q −→ (x)(P 0 |Q0 )
m[x]

m[y]

P −→ P 0 Q −→ Q0 x 6= y[y/x]

P |Q −→ P 0 [y/x]|Q0 [y/x]

Cmm3

m(y)

m[x]

P −→ P 0 Q −→ Q0 y 6∈ gn(P )
Cmm4

(y/x]

P |Q −→ P 0 [y/x]|Q0 [y/x]δm[x]P −→ P 0 x 6∈ n(δ)δ(x)P −→ (x)P 0
[y/x]

Loc0

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

P −→ P 0 x 6= mmyLoc1(x)P −→ P 0 [y/x][y/x]P −→ P 0(y/x](y)P −→ P

m[x]P −→ P 0 x 6= mm(x)(x)P −→ P 0

Loc2

(y/x]

0 Loc4P −→ P 0
Loc5τ(x)P −→ (y)P 0

In the rules, µ ranges over {τ } ∪ {m[x], m[x], mx, m(x) | m, x ∈ N } and δ ranges
over {τ } ∪ {m[x], m[x], mx, m(x), [y/x], (y/x] | m, x, y ∈ N }.
The localization operator in asymmetric χ-calculus is fundamentally different from the restriction combinator in π-calculus. The next example is quite illuminating: (x)([x=y]a[a]|b[x]) ≈ (x)b[x] in π-calculus but (x)([x=y]a[a]|b[x]) 6≈(x)b[x] in the asymmetric χ-calculus. In asymmetric χ-calculus the effect of theconsecutive communications
τ(z)(a[z].(b)(b[z]|b[y]))|(x)a[x].Q =⇒ (b)(0|0)|Q[y/x] ≈ Q[y/x]is the same as the χ-communication
τa[y]|(x)a[x].Q −→ 0|Q[y/x] ≈ Q[y/x].
The asymmetric χ-calculus can be investigated in completely the same way as
the χ-calculus has been. The proofs of the corresponding results are more or lessthe same. In this language, we think of an action with positive subject name as
an input action whereas that with a negative subject name as an output action.
Let f o denote the set {a[x] | a, x ∈ N } of free output, f i the set {a[x] | x ∈ N }of free input, i the set {ax | x ∈ N } of input, ro the set {a(x) | a, x ∈ N }of restricted output, u the set {[y/x] | x, y ∈ N } of updates and ru the set{(y/x] | x, y ∈ N } of restricted updates. We can define L-bisimilarities ≈L ,open bisimilarity and barbed bisimilarity for asymmetric χ-processes as we havefor χ-processes. There are altogether 63 L-bisimilarities for the asymmetric χprocesses. The next theorem conveys all the necessary information to construct
the bisimulation lattice of the asymmetric χ-calculus.
Theorem 23. The following properties hold for asymmetric χ-calculus:(i) ≈ru∪f i∪u and ≈i coincide respectively with open and barbed bisimilarities.
(ii) ≈L ⊆≈i .
(iii) ≈L ⊆≈f o .
(iv) ≈L1 6⊆≈L2 if f i ∩ L1 = ∅ and f i ⊆ L2 .
(v) ≈L1 6⊆≈L2 if ru ∩ L1 = ∅ and ru ⊆ L2 .
(vi) ≈L1 6⊆≈L2 if (ru ∪ ro) ∩ L1 = ∅ and ro ⊆ L2 .
(vii) ≈L1 6⊆≈L2 if u ∩ L1 = ∅ and u ⊆ L2 .
(viii) If L ∩ i = ∅ then the inclusion ≈L ⊂≈i is strict.
(ix) ≈ru ⊂≈ro . The inclusion is strict.

≈i , ≈f o
≈ro

≈ru

*

Y
H

6 HH

H
≈f i

 6H
*
Y
*


H 
HH


≈ro∪f i

H
*

H
6Y
 HH

≈ro∪u

≈f i∪u

H
Y
* 6

*

HH

 H


≈ru∪u

≈ru∪f i

≈u

* 6

H
Y
HH
 H

≈ro∪f i∪u

H
Y
H

*


HH 6
≈ru∪f i∪u

Fig. 4. The Bisimulation Lattice of Asymmetric Chi Processes

Proof. (i,ii) The proofs are similar to those in χ-calculus.
a[x](iii) Suppose P ≈L Q and P −→ P 0 . Let R be a[x]+hφi such that φ ∈ Lτand n(φ) ∩ gn(P |Q) = ∅. Then P |R −→ P 0 |0. It follows that Q0 exists such000that Q|R =⇒ Q |0 and P ≈L Q . Due to asymmetry, it must be the case thata[x]Q =⇒ Q0 .
(iv) Assume f i ∩ L1 = ∅ and f i ⊆ L2 . Then (x)a[x].(b)(b[z]|b[x]) ≈L1 a[z] +(x)a[x].(b)(b[z]|b[x]) but (x)a[x].(b)(b[z]|b[x]) 6≈L2 a[z] + (x)a[x].(b)(b[z]|b[x]).
(v) One has (a)((x)a[x]|a[y])) 6≈ru 0 but (a)((x)a[x]|a[y])) ≈L1 0 wheneverru ∩ L1 = ∅.
(vi) Let R be (x)a[x].(b)(b[x]|(y)b[y].(w)c[w]). Suppose (ru ∪ ro) ∩ L1 = ∅ andro ⊆ L2 . Then R ≈L1 (x)a[x].(w)c[w] + R but R 6≈L2 (x)a[x].(w)c[w] + R.
(vii) Let R be (b)(z)(b[z]|b[x].(a)(a[z]|a[y] + a[y]|a[z])). Suppose u ∩ L1 = ∅and u ⊆ L2 . Then R ≈L1 (a)(a[x]|a[y]) + R but R 6≈L2 (a)(a[x]|a[y]) + R.
(viii) By (ii) through (vii) the inclusion ≈L ⊂≈i is strict whenever L ∩ i = ∅.
a(x)

(x/z]

(ix) Suppose P ≈ru Q and P −→ P 0 . Then P |a[z] −→ P 0 |0 for fresh z.
(x/z]

a(x)

So Q|a[z] =⇒ Q0 |0 for some Q0 . Hence Q =⇒ Q0 . Therefore ≈ru ⊆≈ro . The
strictness follows from (v).
tuAccording to Theorem 23 the L-bisimilarities ≈f i , ≈i , ≈ro , ≈u and ≈ru
are all pairwise distinct. Using these five relations, the bisimulation lattice ofasymmetric χ-processes can be generated. The pictorial description of the latticeis given by the diagram in Fig. 4. There are altogether 12 elements in the lattice.
The bottom element is ≈ru∪f i∪u , which characterizes the open bisimilarity. The
top element is ≈i , which coincides with the barbed bisimilarity.

7

The Asynchronous Asymmetric Chi

It seems reasonable to remove the symmetry of communications in asynchronous
χ-calculus. The resulting language has the same grammar as the asynchronous χ≈ro , ≈i , ≈f o*YH 6 HH



H

≈f i

≈ru

H
*

H
6Y
H
 H

≈u

H
Y
*

H
H 6
 H

≈ru∪u

≈ru∪f i≈f i∪u

H
Y
HH

*

6 
H

≈ru∪f i∪u

Fig. 5. The Bisimulation Lattice of Asynchronous Asymmetric Chi Processes

and the same operational semantics as the asymmetric χ. Without further ado,
we come to describe the bisimulation lattice of the language.
Theorem 24. In the asynchronous asymmetric χ-calculus, one has:(i) ≈f i , ≈ru , ≈u ⊆≈ro =≈i =≈f o ;(ii) ≈f i , ≈ru , ≈u are pairwise distinct.
Proof. Apart from the part to establish (vi), the proof of Theorem 23 works
fine. The only extra work is to prove that ≈L ⊆≈ro for all L-bisimilarities ≈L .
a(x)Suppose P ≈L Q and P −→ P 0 . Let R be (y)a[y].b[y] for some fresh b. Thenbx

bx

P |R =⇒ P 0 |0. It follows that Q0 exists such that Q|R =⇒ Q0 |0 and P 0 ≈L Q0 .
The rest of the argument is similar to that given in the proof of Theorem 22. Inbxbx
Q|R =⇒ Q0 |0 only the reduction −→ causally depends on the communication
involving R. So this particular communication can be delayed to happen justa(x)before the action involving b. It can then be easily seen that Q =⇒ Q0 . To help
understand the idea. Let’s see an example. Suppose Q is (x)(a[x]|Q1 ). Then(x)(a[x]|Q1 )|(y)a[y].b[y] =⇒ (x)(a[x]|Q2 )|(y)a[y].b[y]−→ (x)((0|Q2 )|b[x])bx=⇒ (0|Q3 )|0 ≡ Q0 |0.
a(x)Clearly (x)(a[x]|Q1 ) =⇒ (x)(a[x]|Q3 ) −→ 0|Q3 ≡ Q0 .

tu

The bisimulation lattice of the asynchronous asymmetric χ-calculus is pictured by the diagram in Fig. 5.

8

Final Remark

The χ-calculus is meant to be a concurrent generalization of λ-calculus. In thelatter the variables are uniform in the sense that both free and closed variables
can be instantiated by any term. Free and closed variables become global andlocal names in our model. In this way the names in χ-calculus behave very much
like logical variables. This is not at all surprising as the calculus is designed with
proof theory in mind. At the level of operational semantics, the computationas-cut-elimination is a well accepted approach in the world of λ-calculus andits descendants but has attracted far less attention in process algebra. The χcalculus advocates this approach and invites further study of it.
The L-bisimilarities are introduced as possible classification of bisimilaritieson χ-processes. In both χ and its asymmetric version, open bisimilarity andbarbed bisimilarity are respectively the bottom and the top elements of thebisimulation lattices. Other well-known bisimilarities also fit into the lattice hierarchy. For instance, ground bisimilarity coincides with ≈o∪o .
The fact that the barbed bisimilarity on χ-processes is different from theobvious bisimilarity called open bisimilarity in this paper was first discoveredin [6]. In present paper the difference is recast in the framework of L-bisimilarity.
The barbed bisimilarity on χ-processes has some very interesting and unusual
properties unknown from the study of π-processes. Our result implies that weakbarbed congruence and weak hyperequivalence on Fusion processes are different.
The operational semantics of χ defined in this paper is slightly different fromthat given in [4]. In that paper the reduction
τa[x].P |a[x].Q −→ P |Q
is not admissible althoughτ(x)(a[x].P |a[x].Q) −→ (x)(P |Q)
is legal. It should be pointed out that if this restricted communication mechanism
is adopted, the elements of the bisimulation lattices discussed in this paper would
proliferate. For instance the bisimulation lattice of asymmetric χ-processes would
have eighteen elements, the reason being that ≈f o is different from ≈i in thisvariant for the same reason that ≈f i is different from ≈i .
[y/x]

In our definition of L-bisimilarities, an update transition P −→ P 0 is required[y/x]

to be matched up by Q =⇒ Q0 such that P 0 ≈L Q0 . This is correct because
we use an early semantics. In late semantics we must replace P 0 ≈L Q0 by
P 0 [y/x] ≈L Q0 [y/x]. A simple example suffices to explain the situation. Let R be[y|x].(x[x]|y[y].c[c]) where all names are assumed to be distinct. Then [y|x].c[c] +[y/x]R ≈L R. In late semantics there is no R0 such that R =⇒ R0 ≈L c[c].
In a sense, axiomatization is internalization. Usually a meta-operation isinternalized as choice operator and a meta-judgement is internalized as match
combinator in calculi of mobile processes. The simplicity of the axiomatization
systems for χ-processes is due to the fact that, unlike in π-calculus, one does nothave the trouble of having to treat localization operator separately by resorting
to distinction. In χ-calculus, if a local name can be ‘opened up’ it is open for all
instantiations. The work reported in this paper was carried out independently
with [15]. As far as axiomatization is concerned, the novelty of our result is acomplete system for barbed congruence. We believe that by adding a modifiedversion of the output law O3 to Parrow and Victor’s axiom system for weak
hyperequivalence we get a complete system for the weak barbed congruence on
finite Fusion processes.
An interesting avenue for further investigation is axiomatization of asymmetric χ-processes. We have already obtained complete systems for some of thetwelve L-congruence relations. The rest appears more subtle.

References
1. Amadio, R., Castellani, I., Sangiorgi, D.: On Bisimulation for the Asynchronousπ-Calculus. CONCUR’96, Lecture Notes in Computer Science 1119 (1996)
2. Boudol, G.: Asynchrony and the π-Calculus. Research Report 1702, INRIA,
Sophia-Antipolis (1992)
3. Fu, Y.: The χ-Calculus. Proceedings of the International Conference on Advances
in Parallel and Distributed Computing, March 19th-21th, Shanghai, IEEE Computer Society Press (1997) 74-81
4. Fu, Y.: A Proof Theoretical Approach to Communications. ICALP’97, July 7th11th, Bologna, Italy, Lecture Notes in Computer Science 1256 (1997) 325–335
5. Fu, Y.: Reaction Graph. To appear in Journal of Computer Science and Technology(1998)
6. Fu, Y.: Variations on Mobile Processes. To appear in Theoretical Computer Science, Elsevier Science Publisher
7. Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency.
Journal of ACM 67 (1985) 137–161
8. Honda, K., Tokoro, M.: An Object Calculus for Asynchronous Communication.
ECOOP ’91, Geneve, Lecture Notes in Computer Science (1991)
9. Merro, M.: On the Expressiveness of Chi, Update and Fusion Calculus. Express’98(1998)
10. Milner, R.: Communication and Concurrency. Prentice Hall (1989)
11. Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes. Information
and Computation 100 (1992) Part I:1–40, Part II:41–77
12. Milner, R., Sangiorgi, D.: Barbed Bisimulation. ICALP’92, Lecture Notes in Computer Science 623 (1992) 685–695
13. Parrow, J., Victor, B.: The Update Calculus. Proceedings of AMAST’97, Sydney,
December 13-17 (1997)
14. Parrow, J., Victor, B.: The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. To appear in LICS’98 (1998)
15. Parrow, J., Victor, B.: The Tau-Laws of Fusion. To appear in CONCUR’98 (1998)
16. Sangiorgi, D.: A Theory of Bisimulation for π-Calculus. CONCUR’93, Lecture
Notes in Computer Science 715 (1993)
17. Victor, B., Parrow, J.: Concurrent Constraints in the Fusion Calculus. To appear
in ICALP’98 (1998)