A Schematic Axiom for Open Congruence
Yuxi Fu?
Department of Computer Science
Shanghai Jiaotong University, Shanghai 200030, China

Abstract. A schematic law dealing with localization operator is proposed for pi calculus. It isshown that the law renders the use of distinction unnecessary in the axiomatic theory of open
congruence.

1

Introduction

The role of bisimulation equivalences in process algebra has been reinforced over the last decades. The
studies of the π-calcululs ([15]) and many of its variants have demonstrated both the diversity and thepertinent nature of bisimulation equivalences. Bisimulation equivalences are stronger than other observational equivalences in the sense that they are not sensitive to the changes of environment. In otherwords no matter how environment changes two bisimilar processes can always simulate each other. In
CCS ([14]) the bisimulation approach gives rise to a relatively small number of equivalence relations.
In the π-calculus however there is a proliferation of bisimulation equivalences, one of which is the open
equivalence ([18]). The open equivalence assumes that environments may have significant effect on processes. The change of an environment could modify the names of process residing in the environment
although it can not alter the topological structure of the process. This requires that the definition of open
bisimulation incorporate the idea that process equivalence should be closed under substitution of names
in every bisimulation step. Recent studies on χ-calculus ([1–5, 8–10, 17]) shows that the assumption ofopen bisimulation is very reasonable.
The open equivalence was proposed by Sangiorgi who did just enough to convince the reader of thesimplicity of the relation. Due to the very definition of bisimulation, proofs of theoretical properties ofbisimulation equivalences often rely on inductions on bisimulation steps. For mobile processes bisimulations incur name substitutions. Therefore inductions are made easier if the subject bisimulations areclosed under substitutions. Take for example Sangiorgi’s complete axiomatization system for strong open
equivalence. The proof of the completeness theorem is a straightforward induction. It is considerably simpler than the corresponding proofs for strong early equivalence and strong late equivalence using symbolic
approach ([11, 13]). However in order to deal with localization Sangiorgi’s system introduces distinctions,which is a form of conditions as used in the symbolic framework.
The definition of weak open equivalence, for the π-calculus without the mismatch combinator, can beobtained in the standard manner. Most part of the algebraic theory of this weak relation is simple except in
one aspect. Contrary to the popular belief, the complete system for the strong open equivalence extended
with Milner’s three tau laws does not constitute a complete system for the weak open congruence. A newtau law, T4, proposed by the present author is necessary.
It has to be said that Sangiorgi’s definition of weak open bisimulation applies only to the π-calculus
without the mismatch operator. It was discovered by Fu and Zhang ([6, 7]) that if one applies Sangiorgi’s
definition to the π-calculus with the mismatch operator one gets a relation that is not closed undercomposition! The following example is given in [6]: The processes a(x).P +a(x).[x6=y]P and a(x).[x6=y]Pshould not be bisimilar; but they are indistinguishable by Sangiorgi’s original definition. To bypass the
problem Fu and Zhang have proposed two new equivalence relations. They are the early open bisimilarity
and the late open bisimilarity. The terminologies should suggest that the difference between these two
equivalence relations draws a similarity to that between the early equivalence and the late equivalence.
Fu and Zhang have investigated axiomatization systems for both early and late open congruences. The
two complete systems contain the following schematic laws:(x)C[[x6=y]P ] = (x)C[P ]?

(1)

The author is supported by the NNSFC for Distinguished Young Scholars (60225012) and the Development
Fund of Shanghai Committee of Science and Technology (025115032). He is also supported by BASICS, The
Laboratory for Basic Studies in Computing Science, sponsored by Shanghai Education Commission. BASICS
is affiliated to the Department of Computer Science of Shanghai Jiaotong University.

where x, y are not bound in C[] and x 6= y. This law is equivalent to the following schematic law(x)C[[x=y]P ] = (x)C[0](2)where x, y are not bound in C[] and x 6= y. It is clear that (2) is more general than (1) since it does notrefer to the mismatch combinator. These schematic laws render distinctions unnecessary.
The purpose of this paper is to show that one can use (2) to give a distinction free complete system
for the open congruence of the π-calculus without the mismatch operator. The structure of the paper
is as follows: Section 2 introduces the necessary background materials of π-calculus. Section 3 gives thestrong and the weak systems. Section 4 defines internal distinction and discusses some properties of it.
Section 5 proves a generalized completeness result.

2

Preliminaries

This section fixes up some preliminary notations of π-calculus. The grammar of the π-processes without
the mismatch operator is as follows:
P := 0 | π.P | P | P | (x)P | P +P | [x=y]P |!P
where
π := a(x) | ax | τThe set P of processes is defined in terms of the set N of names. In both a(x).P and (x)P the name x
is bound. The notations f n( ), bn( ), n( ) are standard. A substitution σ is a function from N to N suchthat {x | σ(x) 6= x} is a finite set. We write P σ for the process obtained by substituting names in P
according to σ. The composition of two substitutions σ, σ 0 is denoted by σσ 0 and P σσ 0 is understood as(P σ)σ 0 . We often write {y1 /x1 , . . . , yn /xn } for the substitution that maps x1 , . . . , xn respectively onto
y1 , . . . , yn and maps any other name to itself.
The operational semantics is defined in terms of the following labelled transition system:
Prefixππ.P −→ P
Composition
λa(x)P −→ P 0a(x)ay

P −→ P 0 Q −→ Q0
τP | Q −→ P 0 {y/x} | Q0

λ

P | Q −→ P 0 | Qa(x)P −→ P 0 Q −→ Q0
τP | Q −→ (x)(P 0 | Q0 )Restrictionax

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

P −→ P 0λ(x)P −→ P 0a(x)(x)P −→ (x)P 0
Condition
λP −→ P 0λ[x=x]P −→ P 0
ChoiceλP −→ P 0λ

P +Q −→ P 0
Replication
λP | !P −→ P 0
λ!P −→ P 0
The letter λ ranges over the set {a(x), ax, a(x) | a, x are names} ∪ {τ } of action labels. In what followsµ stands for a finite sequence of match operators concatenated one after another. We will write C[] fora context inductively defined as follows: (i) ( ) is a context; (ii) if C[] is a context then C[] | P , P | C[],(x)C[], C[]+P , P +C[], [x=y]C[], a(x).C[], ax.C[] and τ.C[] are contexts.
A nice property about the π-calculus without the mismatch operator is that actions are preserved bysubstitution of names.
λλσLemma 1. If P −→ P 0 then P σ −→ P 0 σ for any substitution σ.

When defining bisimulation equivalences for π-processes the most subtle problem is to do with thelocalization operator. Sangiorgi’s solution to the problem is to use distinctions.
Definition 2. A distinction is a finite symmetric and irreflexive relation on names. Distinctions will bedenoted by D, D0 etc.. The notation D\x denotes D \ {(x, y), (y, x) | y is a name}.
A substitution σ respects a distinction D if σ(x) 6= σ(y) whenever (x, y) ∈ D. A sequence of match
combinators µ respects a distinction D if µ 6⇒ x=y whenever (x, y) ∈ D.
The strong and weak open bisimilarities are defined as follows.
Definition 3. The set R = {RD } of binary symmetric relations on processes is an open bisimulation if
for each distinction D and for each substitution σ respecting D, P RD Q implies the following properties:λλ(i) If P σ −→ P 0 and λ is not a restricted output action then Q0 exists such that Qσ −→ Q0 and P 0 RDσ Q0 .
a(x)

a(x)

0

(ii) If P σ −→ P 0 then Q0 exists such that Qσ −→ Q0 and P 0 RD Q0 , where D0 is Dσ ∪{x}×f n(P σ+Qσ)∪
f n(P σ+Qσ)×{x}.
P is open bisimilar to Q with respect to D, notation P ∼D
o Q, if there exists an open bisimulation R suchthat (P, Q) ∈ RD . We say that P is open bisimilar to Q if P ∼∅o Q.
Definition 4. The set R = {RD } of binary symmetric relations on processes is a weak open bisimulation
if for each distinction D and for each substitution σ respecting D, P RD Q implies the following properties:bλλ(i) If P σ −→ P 0 and λ is not a restricted output action then Q0 exists such that Qσ =⇒ Q0 and P 0 RDσ Q0 .
a(x)

a(x)

0

(ii) If P σ −→ P 0 then Q0 exists such that Qσ =⇒ Q0 and P 0 RD Q0 , where D0 is Dσ ∪{x}×f n(P σ+Qσ)∪
f n(P σ+Qσ)×{x}.
P is weak open bisimilar to Q with respect to D, notation P ≈D
o Q, if there exists a weak open bisimulation
R such that (P, Q) ∈ RD . We say that P is weak open bisimilar to Q if P ≈∅o Q.
As is well-known ≈Do is not a congruence relation. The standard approach to obtain a congruenceis
givenby the following definition.
relation from ≈DoDDefinition 5. P and Q are open congruent, notation P 'D
o Q, if P ≈o Q and, for each substitution σrespecting D, the following conditions are satisfied:ττ0(i) If P σ −→ P 0 then Qσ =⇒ Q0 such that P 0 ≈D
o Q .
τ
τ
0
0
0
D
(ii) If Qσ −→ Q then P σ =⇒ P such that P ≈o Q0 .

Before ending this section we mention some useful results.
Lemma 6. The following properties hold:
00D0(i) If P ∼Do Q then P ∼o 0 Q for each distinction D such that D ⊆ D .
D0D(ii) If P ≈o Q then P ≈o Q for each distinction D such that D ⊆ D0 .
Lemma 7. The following properties hold:D{y/x}
Q{y/x}.
(i) If P ∼Do Q and (x, y) 6∈ D then P {y/x} ∼o
D{y/x}
D
Q{y/x}.
(ii) If P ≈o Q and (x, y) 6∈ D then P {y/x} ≈oProof. Suppose σ respects D{y/x}. Then {y/x}σ respects D. So (i) and (ii) follow from definitions.

3tu

System

A complete system for process congruence consists of a set of equational laws and a set of inference rules.
These laws and rules contain the usual ones for equivalence and congruence. Figure 1 contains some
useful laws for the strong open congruence. It is well-known that an expansion law is necessary in order
to convert processes in parallel composition form to those in summation form. We omit the standard
expansion law in this paper as it is well-known. So in the rest of the paper we focus on the fragment ofthe π-calculus with neither the composition operator nor the replication operator.
Systems for the weak open congruence enjoy the tau laws in Figure 2. Let ASow be the system
ASo ∪ {T 1, T 2, T 3, T 4}. The proofs of the following soundness results are straightforward.
Proposition 8. (i) ASo is sound for ∼∅o . (ii) ASow is sound for '∅o .
Most of the completeness proofs rely on some kind of normal forms. In our situation we need thefollowing version of normal form.

M1µP = µ0 PM2[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
L1(x)0 = 0L2(x)(y)P = (y)(x)P
L3(x)(P +Q) = (x)P +(x)QL4(x)π.P = π.(x)PL5(x)π.P = 0
L6(x)[y=z]P = [y=z](x)P
L7 (x)C[[x=y]P ] = (x)C[0]if µ ⇔ µ0

if x 6∈ n(π)
if x ∈ subj(π)
if x 6∈ {y, z}
x, y are not bound in C[] and x6=yFig. 1. The Strong System ASo
T1
T2
T3
T4

λ.τ.P = λ.P
P + τ.P = τ.Pλ.(P + τ.Q) = λ.(P + τ.Q) + λ.Q
τ.P = τ.(P + [x=y]τ.P )Fig. 2. The Tau Laws

P
Definition 9. A process P is in strong normal form on V ⊇ f n(P ) if P ≡ i∈I µi λi .Pi and the following
conditions hold(i) For each i ∈ I and each match sequence µ satisfying f n(µ) ⊆ V there exists some j ∈ I such thatµj ⇔ µi µ, λi = λj and Pi ≡ Pj .
(ii) If λi is not an input prefix then Pi is in strong normal form on V . If λi is an input prefix a(x) thenPi is in strong normal form on V ∪ {x}.
For a strong normal form process P let d(P ) be the maximal nested number of prefix operators of it.
Lemma 10. For each π-process P and V ⊇ f n(P ) there exists a process Q which is in strong normal
form on V such that ASo ` Q = P and d(Q) ≤ d(P ).

4Internalizing Distinction

In the rest of this paper we show that ASo is complete for ∼∅o and that ASow is complete for '∅o . If a proof
for the former is available then it is routine to obtain a proof for the latter. So we will be confining ourattention to the strong case. For that purpose we need the operation ( )D , for a distinction D, defined asfollows:def

0D = 0def(a(x).P )D = a(x).P D , where x 6∈ n(D)def(ax.P )D = ax.P D
def(τ.P )D = τ.P D
def((x)P )D = (x)P D , where x 6∈ n(D)def

(P + Q)D = P D + QD
def([x=y]P )D = [x=y](P {y/x})D{y/x} , where (x, y) 6∈ D
def([x=y]P )D = 0, where (x, y) ∈ D
The role of the operation ( )D is to transfer a D-equivalent pair to an ∅-equivalent pair. Notice that thisdefinition can not be applied to the π-calculus with parallel combinator. But thanks to the expansion
law, in axiomatization one can remove the parallel operator in favour of the choice combinator. One of

the properties of ( )D is that it should preserve observational equivalence. This property would be lost
had we replaced the seventh clause of the above definition by the following:def([x=y]P )D = [x=y]P D , where (x, y) 6∈ D
Suppose D = {(x, y), (y, x)}. It is easy to see that[x=z]ax.[x=y][y=z]P ∼∅o [x=z]ax.[y=z]Pbut([x=z]ax.[x=y][y=z]P )D 6∼∅o ([x=z]ax.[y=z]P )D
had we used the alternative definition.
Lemma 11. Suppose σ respects D. Then (P D )σ ≡ (P σ)Dσ .
Proof. The lemma can be proved by structural induction. Suppose for instance (x, y) 6∈ D. Then(([x=y]P )D )σ = ([x=y](P {y/x})D{y/x} )σ= [xσ=yσ](P {y/x})D{y/x} σ
I.H.

= [xσ=yσ](P {y/x}σ)D{y/x}σM2= [xσ=yσ](P {y/x}σ)D{y/x}σ {yσ/xσ}

I.H.

= [xσ=yσ](P {y/x}σ{yσ/xσ})D{y/x}σ{yσ/xσ}= [xσ=yσ](P σ{yσ/xσ})Dσ{yσ/xσ}= ([xσ=yσ]P σ)Dσ
= (([x=y]P )σ)Dσ

If (x, y) ∈ D then (([x=y]P )D )σ ≡ 0 ≡ (([x=y]P )σ)Dσ .

t
u

λ

λ

Lemma 12. If P D −→ P 0 then there exists some P1 such that P −→ P1 and P1D ≡ P 0 .
Proof. We take a look at only one case. Suppose P ≡ [x=y]P2 . Then by definition it must be the caseλthat (x, y) 6∈ D and x = y. So P ≡ [x=x]P2 and P D ≡ [x=x]P2D . Consequently P2D −→ P 0 . By induction
λλhypothesis P2 −→ P1 for some P1 such that P1D ≡ P 0 . It follows that P −→ P1 .
λ

t
u

λ

Lemma 13. If P −→ P1 then P D −→ P1D .
Proof. Suppose P is [x=y]P2 . Then it must be the case that x = y. Therefore P D ≡ [x=y]P2D . The restof the argument is easy.
t
u
λ

λ

Corollary 14. Suppose σ respects D. If P σ −→ P 0 then (P D )σ −→ (P 0 )Dσ .
D1
1 ∪D2
2
Q.
then P ∼D
Lemma 15. Suppose D1 and D2 are distinctions. If P D1 ∼Doo Q

Proof. Suppose D is a distinction. Let RD be
D1
2{(P, Q) | P D1 ∼D, D1 and D2 are distinctions, D1 ∪ D2 = D}o Q
λWe prove that R = {RD } is a strong open bisimulation. Suppose σ respects D and P σ −→ P 0 . Thenλ2
(P D1 )σ −→ (P 0 )D1 σ by Corollary 14. It follows from P D1 ∼D
QD1 and Lemma 11 that (QD1 )σ ≡oλλ(Qσ)D1 σ −→ Q1 for some Q1 to match up the action (P D1 )σ −→ (P 0 σ)D1 σ . By Lemma 12 some Q0
λexists such that Qσ −→ Q0 and (Q0 )D1 σ ≡ Q1 . There are two cases:
2σ– λ is not a restricted output action. Then (P 0 )D1 σ ∼D(Q0 )D1 σ by the choice of Q0 . Consequentlyo(P 0 , Q0 ) ∈ RDσ .
0
0 D1 σ– λ is a restricted output action, say a(x). Then (P 0 )D1 σ ∼Dby the choice of Q0 , where D0 iso (Q )
D1
D1
D1
D1
D2 σ∪{x}×f n(P σ+Q σ)∪f n(P σ+Q σ)×{x}. Notice that f n(P D1 σ+QD1 σ) ⊆ f n(P σ+Qσ).
00
By Lemma 6 one has (P 0 )D1 σ ∼D(Q0 )D1 σ , where D00 is D2 σ∪{x}×f n(P σ+Qσ)∪f n(P σ+Qσ)×{x}.
o00Dσ∪{x}×f n(P σ+Qσ)∪f n(P σ+Qσ)×{x}
It follows that (P , Q ) ∈ R.

This completes the proof.
Corollary 16. If P D ∼∅o QD then P ∼D
o Q.

t
u

5

A General Completeness Result

We first prove some auxiliary lemmas.
Lemma 17. If µ ⇔ µ0 then ASo ` (µP )D = (µ0 P )D .
Proof. Suppose µ is [x1 =y1 ] . . . [xn =yn ] and µ0 is [a1 =b1 ] . . . [am =bm ]. Then(µP )D = µ(P {y1 /x1 } . . . {yn /xn })D{y1 /x1 }...{yn /xn }= µµ0 (P {y1 /x1 } . . . {yn /xn })D{y1 /x1 }...{yn /xn }= µµ0 (P {y1 /x1 } . . . {yn /xn }{b1 /a1 } . . . {bm /am })D{y1 /x1 }...{yn /xn }{b1 /a1 }...{bm /am }= µµ0 (P {b1 /a1 } . . . {bm /am })D{b1 /a1 }...{bm /am }= µ0 (P {b1 /a1 } . . . {bm /am })D{b1 /a1 }...{bm /am }= (µ0 P )D
The third equality holds because {b1 /a1 } . . . {bm /am } and {y1 /x1 } . . . {yn /xn }{b1 /a1 } . . . {bm /am } are
the same map using the fact that µ ⇔ µ0 .
tuLemma 18. Suppose µ respects D. Then ASo ` (µP )D = µ(P σµ )Dσµ .
Proof. Suppose σµ is {a1 /x11 , . . . , a1 /x1m1 , . . . , an /xn1 , . . . , an /xnmn }. Then clearly
σµ = {a1 /x11 } . . . {a1 /x1m1 } . . . {an /xn1 } . . . {an /xnmn }as functions. Let µ0 be [a1 = x11 ] . . . [a1 = x1m1 ] . . . [an = xn1 ] . . . [an = xnmn ]. Then µ ⇔ µ0 . By Lemma 17,(µP )D = (µ0 P )D
1

1

n

n

= µ0 (P {a1 /x11 } . . . {a1 /x1m1 } . . . {an /xn1 } . . . {an /xnmn })D{a1 /x1 }...{a1 /xm1 }...{an /x1 }...{an /xmn }= µ0 (P σµ )Dσµ
= µ(P σµ )Dσµtu

We are done.
The next lemma describes a generalized completeness result.
D
Lemma 19. If P ∼D
= QD .
o Q then ASo ` P

Proof. The proof is carried out by induction on d(Pthat both P and Q are
P ) + d(Q). We may assumePstrong normal forms on f n(P +Q). Suppose P ≡ i∈I µi λi .Pi and Q ≡ j∈J µj λj .Qj . Let (µi λi .Pi )D
be a summand of P D , meaning that µi λi .Pi is a summand of P and µi respects D. Let σ be σµi . It isλ σieasy to see that σ respects D. It follows from P σ −→Pi σ and P ∼Do Q that Q must contain a summand

λj σ

λ σ

i
µj λj .Qj such that µi ⇒ µj , λi σ ≡ λj σ and that Qσ −→ Qj σ matches up P σ −→Pi σ. Since Q is instrong normal form on f n(P + Q), there must be a summand µj 0 λj .Qj of Q such that µj 0 ⇔ µi .

– If λi σ is not a restricted output action then Pi σ ∼DσQj σ. It follows by induction hypothesis thatoASo ` (Pi σ)Dσ = (Qj σ)Dσ . Consequently
ASo ` QD = QD + (µj 0 λj .Qj )D= QD + (µi λj .Qj )D= QD + µi (λj σ.Qj σ)Dσ
= QD + µi λj σ.(Qj σ)DσI.H.

= QD + µi λi σ.(Pi σ)Dσ
= QD + (µi λi .Pi )D

where the second equality holds by Lemma 17 and the third equality holds by Lemma 18.

00– If λi σ is a restricted output action a(x) then Pi σ ∼Do Qj σ where D is Dσ ∪ {x}×f n(P σ+Qσ) ∪0
D0
f n(P σ+Qσ)×{x}. By induction hypothesis one has that ASo ` (Pi σ) = (Qj σ)D . Suppose we canprove

ASo ` a(x).(Pi σ)Dσ = a(x).(Qj σ)Dσ

(3)

Then
ASo ` QD = QD +(µi a(x).Qj )D= QD + µi aσ(x).(Qj σ)Dσ
(3)

= QD + µi aσ(x).(Pi σ)Dσ
= QD + (µi a(x).Pi )D

It follows that ASo ` QD = QD + P D . Similarly ASo ` P D = P D + QD . Hence ASo ` P D = QD .
0
It remains to establish (3). First we show that ASo ` a(x).(Pi σ)Dσ = a(x).(Pi σ)D . There are twocases:– Suppose there is no context C[] such that Pi σ ≡ C[[x=y]R] or Pi σ ≡ C[[y=x]R] for a free name y0
in f n(P σ+Qσ) and a process R. Then it is easy to see from the definition of ( )D that (Pi σ)D ≡0(Pi σ)Dσ . Consequently ASo ` a(x).(Pi σ)Dσ = a(x).(Pi σ)D .
– If there is a context C[] such that Pi σ ≡ C[[x=y]R] for some free name y in f n(P σ+Qσ) and someprocess R. Then by definition one has that0

(Pi σ)D ≡ (C[0])D0and by L8a that
ASo ` a(x).(Pi σ)Dσ = a(x).(C[0])Dσ
Repeat the above construction until we get some P1 such that0

(Pi σ)D ≡ P1D

0and
ASo ` a(x).(Pi σ)Dσ = a(x).P1Dσ
Now the previous case applies to P1 , meaning that
ASo ` a(x).P1Dσ = a(x).P1D

0

It follows that
ASo ` a(x).(Pi σ)Dσ = a(x).(Pi σ)D
0

0

0

0

Similarly ASo ` a(x).(Qj σ)Dσ = a(x).(Qj σ)D . Then (3) follows from ASo ` (Pi σ)D = (Qj σ)D .

tuCorollary 20. For the finite π-processes without the mismatch combinator the following equivalencesD
hold: P D ∼∅o QD if and only if P ∼D
= QD .
o Q if and only if ASo ` PDD
Proof. By Corollary 16, P D ∼∅o QD implies P ∼D
= QD .
o Q. By Lemma 19, P ∼o Q implies ASo ` P
D
D
D
∅
D
By Proposition 8, ASo ` P = Q implies P ∼o Q .
tuTheorem 21. ASo is complete for ∼∅o on the π-processes without the mismatch combinator.
Proof. Take D in the Corollary 20 to be the empty distinction.

tuUsing the technique that should be familiar to the reader by now, one can generalize the above
arguments to the weak case. We state the result without any proof.
w
D
Lemma 22. If P ≈D
= QD .
o Q then ASo ` P

Theorem 23. ASow is complete for '∅o on the π-processes without the mismatch combinator.

6

Comment

The short paper focuses on a particular axiom for the localization operator in π-calculus. This problem
has been looked at by Lin in his symbolic approach to axiomatization ([13]) and by Parrow and Sangiorgi([16]). In the symbolic approach equality reasoning is done under the assumption of a set of equational
and/or inequational conditions on names. Under a complete condition the match and mismatch operatorsconcerning a localized name in a process can be removed. This achieves the same effect as the law L7.
Lin’s method is applicable to π-calculus both with the mismatch combinators and without the mismatch
combinators. It has to be said however that even if the π-calculus is without the mismatch operator thesymbolic system has to deal with inequational conditions. Lin has studied the early/late strong/weakcongruences, while Li has investigated the strong/weak open congruences ([12]). Parrow and Sangiorgi
have worked on the problem in a non-symbolic framework. The π-calculus they used is the one withthe mismatch operator. The underlying idea is similar to that of Lin’s using the fact that the mismatch
operator allows to internalize conditions to a great extent. The contribution of this short paper is toshow how one can deal with the axiomatization of the π-calculus without the mismatch operator in a
non-symbolic fashion.
Acknowledgement The author would like to thank Xiaoju Dong and Zhenrong Yang for helpful discussions.

References
1. Dong X, Fu Y. Observing Asymmetry and Mismatch. APLAS’03, Lecture Notes in Computer Science 2895,
Springer, 2003, 2∼19.
2. Fu Y. A Proof Theoretical Approach to Communications, ICALP’97, Lecture Notes in Computer Science
1256, Springer, 1997, 325∼335.
3. Fu Y. Bisimulation Lattice of Chi Processes, ASIAN’98, Lecture Notes in Computer Science 1538, Springer,
1998, 245∼262.
4. Fu Y. Variations on Mobile Processes, Theoretical Computer Science, 1999, 221(1-2): 327∼368.
5. Fu Y. Open Bisimulations of Chi Processes. CONCUR’99, Lecture Notes in Computer Science 1664, Springer,
1999, 304∼319.
6. Fu Y, Yang Z. Chi Calculus with mismatch. CONCUR 2000, Lecture Notes in Computer Science 1877,
Springer, 2000, 596∼610.
7. Fu Y, Yang Z. The Ground Congruence for Chi Calculus. FST&TCS 2000, Lecture Notes in Computer Science
1974, Springer, 2000, 385∼396.
8. Fu Y. Bisimulation Congruences of Chi Calculus. Information and Computation, 2003, 184(1): 201∼226.
9. Fu Y, Yang Z. Understanding the Mismatch Combinator in Chi Calculus. Theoretical Computer Science,
2003, 290(1): 779∼830.
10. Fu Y, Yang Z. Tau Laws for Pi Calculus. Theoretical Computer Science, 2003, 308(1-3): 55∼130.
11. Hennessy M, Lin H. Symbolic Bisimulations. Theoretical Computer Science, 1995, 138(2): 353∼369.
12. Li Z. Theories and Algorithms for the Verification of Bisimulation Equivalences in Value-Passing CCS andthe π-Calculus. PhD Thesis (Changsha Institute of Technology), 1999.
13. Lin H. 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, 1995, 187∼201.
14. Milner R. Communication and Concurrency. Prentice Hall, 1989.
15. Milner R, Parrow J, Walker D. A Calculus of Mobile Processes. Information and Computation, 1992, 100(1):1∼40 (Part I), 41∼77 (Part II).
16. Parrow J, Sangiorgi S. Algebraic Theories for Name-Passing Calculi. Information and Computation, Academic
Press, 1995, 120(2): 174∼197.
17. Parrow J, Victor B. The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. LICS’98, IEEE
Computer Society, 1998, 176∼185.
18. Sangiorgi D. A Theory of Bisimulation for π-Calculus. Acta Informatica, 1996, 3(1): 69–97.