The Ground Congruence for Chi Calculus?
Yuxi Fu??

Zhenrong Yang

Department of Computer Science
Shanghai Jiaotong University, Shanghai 200030, China

Abstract. The definition of open bisimilarity on the χ-processes does
not give rise to a sensible relation on the χ-processes with the mismatch
operator. The paper proposes ground open congruence as a principal
open congruence on the χ-processes with the mismatch operator. The
algebraic properties of the ground congruence is studied. The paper also
takes a close look at barbed congruence. This relation is similar to theground congruence. The precise relationship between the two is worked
out. It is pointed out that the sound and complete system for the ground
congruence can be obtained by removing one tau law from the complete
system for the barbed congruence.

1

Introduction and χ-Calculus with Mismatch

The π-calculus ([6]) is a powerful process calculus. The expressiveness is partly
supported by input processes of the form a(x).P and output processes of theform ax.P . The former may receive a name at channel name a before evolving
as P with x replaced by the received name. The latter can emit x at a and thencontinues as P . The expressiveness is also supported by processes of the form(x)P . The localization operator (x) encapsulates the name x in P . In χ-calculus([1–4]) the input and output processes are unified as α[x].P , in which α stands
for either a name or a coname.
Formally χ-processes are defined by the following abstract syntax:
P := 0 | α[x].P | P |P | (x)P | [x=y]P | P +P
where α ∈ N ∪ N . Here N is the set of names ranged over by small case letters.
The set {x | x ∈ N } of conames is denoted by N . The name x in (x)P is
local. A name is global in P if it is not local in P . The global names, the local
names and the names of a syntactical object, as well as the notations gn( ), ln( )and n( ), are defined with their standard meanings. We adopt the α-convention
widely used in the literature on process algebra. We do not consider replication
or recursion operator since it does not affect the results of this paper.
?
??

FST&TCS 2000 , Lecture Notes in Computer Science 1974, 385-396, 2000.
The author is funded by NNSFC (69873032) and 863 Hi-Tech Project (863-306ZT06-02-2). He is also supported by BASICS, Center of Basic Studies in Computing
Science, sponsored by Shanghai Education Committee. BASICS is affiliated to the
Department of Computer Science at Shanghai Jiaotong University.

The following labeled transition system defines the operational semantics ofχ-calculus, in which symmetric rules are systematically omitted. In the following
rules the letter γ ranges over the set {α(x), α[x] | α ∈ N ∪ N , x ∈ N } ∪ {τ }and the letter λ over the set {α(x), α[x], [y/x] | α ∈ N ∪ N , x, y ∈ N } ∪ {τ }.
The symbols α(x), α[x], [y/x] represent restricted action, free action and update
action respectively. The x in the label α(x) is local.
Sequentialization
Sqn

α[x]

α[x].P −→ P
Composition[y/x]

P −→ P 0γ

P −→ P 0 ln(γ) ∩ gn(Q)=∅Cmp0
γ
P |Q −→ P 0 |Q

[y/x]

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

Communication
α(x)

α[y]

α(x)

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

[y/x]

α[x]

x 6= yP |Q −→ P 0 [y/x]|Q0 [y/x]α(x)P −→ P 0 Q −→ Q0
Cmm1
τP |Q −→ (x)(P 0 |Q0 )α[x]P −→ 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

M tch

Summation
λP −→ P 0λ

P +Q −→ P 0

Sum

A substitution is a function from N to N that is identical on all but a finite
number of names. Substitutions are usually denoted by σ, σ 0 , . . .. The notationsb
λ=⇒ and =⇒ are used in their standard meanings.
We will use two induced prefix operators, tau and update prefixes, defineddef
def
as follows: [y|x].P = (a)(a[y]|a[x].P ) and τ.P = (b)[b|b].P where a, b are fresh.
6=
The subject language of this paper is χ -calculus, the χ-calculus with themismatch operator. The operational semantics of the mismatch combinator isdefined as follows:λP −→ P 0 x 6= y
M ismtchλ[x6=y]P −→ P 0

The set of χ6= -processes is denoted by C. Suppose Y is a finite set {y1 , . . . , yn } ofnames. The notation [y6∈Y ]P will stand for [y6=y1 ] . . . [y6=yn ]P , where the orderof mismatch operators is immaterial. We will write φ and ψ, called conditions, tostand for sequences of match and mismatch combinators concatenated one after
another, µ for a sequence of match operators, and δ for a sequence of mismatch
operators. Consequently we write ψP , µP and δP . When the length of ψ (µ, δ)is zero, ψP (µP , δP ) is just P . The notation φ ⇒ ψ says that φ logically implies
ψ and φ ⇔ ψ that φ and ψ are logically equivalent. A substitution σ agrees with
ψ, and ψ agrees with σ, when ψ ⇒ x=y if and only if σ(x)=σ(y).
Bisimulation equivalence relations on mobile processes are a lot more complex
than those on CCS processes. The complication is mainly due to the dynamic
aspect of mobile processes. The names in a process are subject to updates during
the evolution of the process. These updates could be caused either by actions
in which the process participates or by changes incurred by environments. A
sensible observational equivalence for mobile processes must take that into account. To illustrate what kind of relations one would obtain if s/he ignored themobility, we introduce the following definition for χ-calculus:
Definition 1. Let R be a symmetric binary relation on the set of χ-processes.
λIt is called a naked bisimulation if whenever P RQ and P −→ P 0 then some Q0b
λexists such that Q =⇒ Q0 RP 0 . The naked bisimilarity ≈ is the largest naked
bisimulation.
It is obvious that the definition of ≈ is simply a reiteration of the weak bisimilarity of CCS in terms of the operational semantic of χ-calculus. However the
naked bisimilarity is not a good equivalence relation since it is not closed under
the parallel composition. For instance one has a[x]|b[y] ≈ a[x].b[y]+b[y].a[x] but
not (a[x]|b[y])|(c[a]|c[b]) ≈ (a[x].b[y]+b[y].a[x])|(c[a]|c[b]). Process equivalence isobservational equivalence. One of the defining properties for an observational
equivalence is that the equivalence should be closed under parallel composition.
In [1–4], it has been argued that bisimulation equivalences for χ-calculus areclosed under substitution. This suggests to introduce the following definition:
Let R be a symmetric binary relation on the set of χ-processes that isclosed under substitution. It is called an open bisimulation if wheneverbλλP RQ and P −→ P 0 then some Q0 exists such that Q =⇒ Q0 RP 0 . The
open bisimilarity ≈o is the largest open bisimulation.
The open bisimilarity ≈o has been studied in [1–4] in both the symmetric andthe asymmetric frameworks. It must be pointed out that the investigations
carried out in [1–4] are for the χ-calculus without the mismatch combinator.
For the χ-calculus with the mismatch operator, one should ask the question
whether the open bisimilarity ≈o is a sensible equivalence. In [5] the present
authors have given a negative answer to the question. As it turned out the
open bisimilarity defined above is not closed under parallel composition in χ6= calculus! One has [x6=y]a[x].P + a[x].[x6=y]τ.P ≈o a[x].[x6=y]τ.P but it is clear

that a[y]|([x6=y]a[x].P + a[x].[x6=y]τ.P ) 6≈o a[y]|(a[x].[x6=y]τ.P ). This is a serious
problem because closure under parallel composition is an intrinsic property ofobservational equivalence. In [5] we have studied the problem and introduced two
modified open congruences. These are early open congruence and late open congruence. Their relationship strongly recalls that between the weak early equivalence and the weak late equivalence ([6]). It should be said however that boththe early open congruence and the late open congruence are the obvious modifications with motivation from π-calculus. They are not the open congruence
for the χ-calculus with the mismatch operator. What is then the principal open
congruence for χ-calculus with the mismatch combinator? We will give our answer to the question in this paper. The way to arrive to the definition of theopen congruence is via a particular naked bisimulation. In order to define thisrelation we need the notion of contexts defined as follows: (i) [] is a context; (ii)
If C[] is a context then α[x].C[], C[]|P , P |C[], (x)C[] and [x=y]C[] are contexts.
Definition 2. The ground bisimilarity ≈g is the largest naked bisimulation thatis closed under context.
In the above definition the requirement of closure under the prefix operator isreasonable since it is equivalent to that of closure under substitution. We will
give an equivalent characterization of ≈g in the style of open semantics, which
we argue is the principal open bisimilarity.
As it turns out the equivalence ≈g is very similar to the barbed bisimilarityof the χ-calculus with the mismatch operator. The difference is very subtle. The
barbed bisimilarity also has an equivalent open characterization. The similarity
and the difference between the ground bisimilarity and the barbed bisimilarity
are revealed through their open characterizations.
This paper continues the work of [5] by studying the ground congruence andthe barbed congruence for the χ6= -calculus. The main contributions of this paper
are as follows:– We give an alternative characterization of the weak barbed bisimilarity. This
characterization points out the complex nature of the weak barbed bisimilarity. Many unknown equalities are discovered. A complete system for the
weak barbed congruence is provided. The new tau laws used to establish thecompleteness result are surprisingly complex.
– We study what we call ground open bisimilarity. A complete system for the
ground open congruence is given. The relationship between the ground open
congruence and the weak barbed congruence is revealed.
Due to space limitation, all proofs have been omitted.

2

Barbed Congruence

The barbed equivalence is often quoted as a universal equivalence relation forprocess algebras. For a specific process calculus barbed equivalence immediately

gives rise to an observational equivalence. For two process calculi barbed equivalence can be used to compare the semantics of the two models. Despite theuniversal nature, barbed equivalence can have quite different displays in different process calculi. The barbed equivalence for the χ-calculus has brought some
new insight into the calculi of mobile processes. In this section we demonstratethat the barbed equivalence for the χ6= -calculus is even more different. A characterization theorem for the barbed bisimilarity on χ6= -calculus is given. Some
illustrating pairs of barbed equivalent processes are given. First we introduce
the notion of barbedness.
α(x)Definition 3. A process P is strongly barbed at a, notation P ↓a, if P −→ P 0
α[x]or P −→ P 0 for some P’ such 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.
From the point of view of barbed equivalence an observer can not see the content
of a communication. What an observer can detect is the ability of a process tocommunicate at particular channels. Two processes are identified if they cansimulate each other in terms of this ability.
Definition 4. Let R be a barbed symmetric relation on C closed under context.
τThe relation R is a barbed bisimulation if whenever P RQ and P −→ P 0 thenQ =⇒ Q0 RP 0 for some Q0 . The barbed bisimilarity ≈b is the largest barbed
bisimulation.
The trade-off of the simplicity of the above definition is that it provides
little intuition about equivalent processes. We know that it is weaker than mostbisimulation equivalences. But we want to know how much weaker it is. We first
give some examples of barbed equivalent processes. To make the examples moredefreadable, we will write A = P R(A+Q) for P R(P +Q), where R is a binary
relation on processes. The first example of an equivalent pair is this:def

A1 = α[x].(P1 +[x=y1 ]τ.Q)+α[x].(P2 +[x6=y1 ]τ.Q) ≈b A1 + α[x].Q
If α[x].Q on the right hand side is involved in a communication in which x is
replaced by y1 then α[x].(P1 +[x=y1 ]τ.Q) can simulate the action. Otherwise
α[x].(P2 +[x6=y1 ]τ.Q) would do the job. The second example is more interesting:def

A2 = (z)α[z].(P1 +[z=y2 ][z|x].Q)+α[x].(P2 +[x6=y2 ]τ.Q[x/z])≈b A2 + α[x].Q[x/z]τThe communication α[y2 ]|(x)(A2 +α[x].Q[x/z]) −→ 0|Q[x/z][y2 /x] for instanceττ
can be matched up by α[y2 ]|(x)A2 −→0|(x)(P1 [y2 /z]+[y2 =y2 ][y2 |x].Q[y2 /z]) −→0|Q[y2 /z][y2 /x]. The third example is unusual:def

A3 = α[y3 ].(P1 +[y3 |x].Q)+α[x].(P2 +[x6=y3 ]τ.Q) ≈b A3 + α[x].Q

If α[x].Q participates in a communication in which x exchanges for y3 then its
role can be simulated by α[y3 ].(P1 +[y3 |x].Q). The fourth is similar:
def

A4 = [y4 |x].(P1 +α[y4 ].Q)+α[x].(P2 +[x6=y4 ]τ.Q) ≈b A4 + α[x].Qτ

If (y4 )((A4 +α[x].Q)|α[y4 ].O) −→ Q[x/y4 ]|O[x/y4 ] then the simulation is:ττ(y4 )(A4 |α[y4 ].O)−→(P1 [x/y4 ]+α[x].Q[x/y4 ])|α[x].O[x/y4 ]−→Q[x/y4 ]|O[x/y4 ]The fifth example is the combination of the fourth and the second:def

A5 = [y5 |x].(P1 +(z)α[z].(P10 +[z=y5 ]τ.Q))+α[x].(P2 +[x6=y5 ]τ.Q[x/z])≈b A5 + α[x].Q[x/z]
Notice that the component [y5 |x].(P1 +(z)α[z].(P10 +[z=y5 ]τ.Q)) is operationallythe same as the process [y5 |x].(P1 +(z)α[z].(P10 +[z=y5 ][z|x].Q)).
In the above examples, all the explicit mismatch operators contain the namex. In general there could be other conditions. The treatment of match operator
is easy. The mismatch operator is however nontrivial. Suppose δ is a sequenceof mismacth operators such that all names in δ are different from both x and z.
An example more gerneral than A1 is this:def

A01 = α[x].(P1 +δ[x=y1 ]τ.Q)+α[x].(P2 +δ[x6=y1 ]τ.Q) ≈b A01 + [x6∈n(δ)]δα[x].Q
We need to explain the mismatch sequence in [x6∈n(δ)]δα[x].Q. The δ before
α[x].Q is necessary for otherwise an action of ([x6∈n(δ)]α[x].Q)σ may not be
simulated by any action from A01 σ when σ invalidates δ. The [x6∈n(δ)] is necessary because otherwise it would not be closed under substitution. A counterexample is the pair α[x].[y6=z][x=y1 ]τ.Q+α[x].[y6=z][x6=y1 ]τ.Q+[y6=z]α[x].Q and
α[x].[y6=z][x=y1 ]τ.Q+α[x].[y6=z][x6=y1 ]τ.Q. If we substitute x for z in the twoprocesses we get two processes that are not barbed bisimilar. Similarly the example A2 can be generalized to the following:def

A02 = (z)α[z].(P1 +[x6∈n(δ)]δ[z=y2 ][z|x].Q)+α[x].(P2 +δ[x6=y2 ]τ.Q[x/z])≈b A02 + [x6∈n(δ)]δα[x].Q[x/z]The general form of A3 is more delicate:def

A03 = [x6=y3 ]α[y3 ].(P1 +[x6∈n(δ)]δ[y3 |x].Q)+α[x].(P2 +δ[x6=y3 ]τ.Q)≈b A03 + [x6=y3 ][x6∈n(δ)]δα[x].Q
In both [x6=y3 ]α[y3 ].(P1 +[x6∈n(δ)]δ[y3 |x].Q) and [x6=y3 ][x6∈n(δ)]δα[x].Q there is
the mismatch [x6=y3 ]. If this operator is removed from A03 one hasdef

B30 = α[y3 ].(P1 +[x6∈n(δ)]δ[y3 |x].Q)+α[x].(P2 +δ[x6=y3 ]τ.Q)
6≈b B30 + [x6∈n(δ)]δα[x].Q

The inequality is clearer if one substitutes x for y3 in the above:def

C30 = α[x].(P1 +[x6∈n(δ)]δ[x|x].Q)+α[x].(P2 +δ[x6=x]τ.Q)
6≈b C30 + [x6∈n(δ)]δα[x].Q
The component [x6∈n(δ)]δα[x].Q may be involved in a communication in which x
is replaced by a name in δ. This action can not be simulated by C30 . The generalforms of A4 and A5 are as follows:def

A04 = [y4 |x].(P1 +δα[y4 ].Q)+α[x].(P2 +δ[x6=y4 ]τ.Q) ≈b A04 + [x6∈n(δ)]δα[x].Q
def

A05 = [y5 |x].(P1 +(z)α[z].(P10 +δ[z=y5 ]τ.Q))+α[x].(P2 +δ[x6=y5 ]τ.Q[x/z])≈b A05 + [x6∈n(δ)]δα[x].Q[x/z]
If we replace the second summand α[x].(P2 +δ[x6=y1 ]τ.Q) of A01 by (z)α[z].(P2 +[x6∈n(δ)]δ[z6=y1 ][z|x].Q) and Q by Q[x/z], we get an interesting variant of A01 as
follows:
def

A001 = α[x].(P1 +δ[x=y1 ]τ.Q[x/z])+(z)α[z].(P2 +[x6∈n(δ)]δ[z6=y1 ][z|x].Q)≈b A001 + [x6∈n(δ)]δα[x].Q[x/z]The bisimilar pairs A02 through A05 have similar variants:
def

A002 = (z)α[z].(P1 +[x6∈n(δ)]δ[z=y2 ][z|x].Q)+O2≈b A002 + [x6∈n(δ)]δα[x].Q[x/z]def

A003 = [x6=y3 ]α[y3 ].(P1 +[x6∈n(δ)]δ[y3 |x].Q[x/z])+O3≈b A003 + [x6=y3 ][x6∈n(δ)]δα[x].Q[x/z]def

A004 = [y4 |x].(P1 +δα[y4 ].Q[x/z])+O4≈b A004 + [x6∈n(δ)]δα[x].Q[x/z]def

A005 = [y5 |x].(P1 +(z)α[z].(P10 +δ[z=y5 ]τ.Q[z/x]))+O5≈b A005 + [x6∈n(δ)]δα[x].Q[x/z]
where Oi is (z)α[z].(P2 +[x6∈n(δ)]δ[z6=yi ][z|x].Q) for i ∈ {2, 3, 4, 5}. The mostcomplicated situation arises when all the five possibilities as described by A001
through A005 happen at one go:def

A = (z)α[z].(P2 +[x6∈n(δ)]δ[z6∈{y1 , y2 , y3 , y4 , y5 }][z|x].Q)+α[x].(P1 +δ[x=y1 ]τ.Q[x/z])+(z)α[z].(P1 +[x6∈n(δ)]δ[z=y2 ][z|x].Q)+[x6=y3 ]α[y3 ].(P1 +[x6∈n(δ)]δ[y3 |x].Q[x/z])+[y4 |x].(P1 +δα[y4 ].Q[x/z])+[y5 |x].(P1 +(z)α[z].(P10 +δ[z=y5 ]τ.Q[z/x]))≈b A + [x6=y3 ][x6∈n(δ)]δα[x].Q[x/z]Similarly the examples A01 through A05 can be combined into one as follows:def

A0 = α[x].(P2 +δ[x6∈{y1 , y2 , y3 , y4 , y5 }]τ.Q[x/z])+α[x].(P1 +δ[x=y1 ]τ.Q[x/z])+(z)α[z].(P1 +[x6∈n(δ)]δ[z=y2 ][z|x].Q)+[x6=y3 ]α[y3 ].(P1 +[x6∈n(δ)]δ[y3 |x].Q[x/z])+[y4 |x].(P1 +δα[y4 ].Q[x/z])+[y5 |x].(P1 +(z)α[z].(P10 +δ[z=y5 ]τ.Q[z/x]))≈b A0 + [x6=y3 ][x6∈n(δ)]δα[x].Q[x/z]Having seen so many bisimilar pairs of processes, the reader might wonder how
we have discovered them. As a matter of fact these examples are all motivated byan alternative characterization of the barbed bisimilarity. This characterization
is given by an open bisimilarity as defined below.
Definition 5. Let R be a binary symmetric relation on C closed under substitution. The relation R is a barbed open bisimulation if the following properties
hold for P and Q whenever P RQ:bλλ(i) If λ is an update or a tau and P −→ P 0 then Q0 exists such that Q =⇒ Q0 RP 0 .
α[x](ii) If P −→ P 0 then one of the following properties holds:
α[x]– Q0 exists such that Q =⇒ Q0 RP 0 ;α(z)– Q0 and Q00 exist such that Q =⇒−→ Q00 and Q00 [x/z] =⇒ Q0 RP 0 ;and, for each y different from x, one of the following properties holds:
α[x]– Q0 and Q00 exist such that Q =⇒−→ Q00 and Q00 [y/x] =⇒ Q0 RP 0 [y/x];
α(z)

[y/x]

– Q0 and Q00 exist such that Q =⇒−→ Q00 and Q00 [y/z] =⇒ Q0 RP 0 [y/x];α[y] [y/x]– Q0 exists such that Q =⇒ =⇒ Q0 RP 0 [y/x];[y/x] α[y]– Q0 exists such that Q =⇒ =⇒ Q0 RP 0 [y/x];[y/x] α(z)– Q0 and Q00 exist such that Q =⇒ −→ Q00 and Q00 [y/z]=⇒Q0 RP 0 [y/x].
α(x)(iii) If P −→ P 0 then, for each y, one of the following properties holds:α(x)– Q0 and Q00 exist such that Q =⇒−→ Q00 and Q00 [y/x]=⇒Q0 RP 0 [y/x];α[y]– Q0 exists such that Q =⇒ Q0 RP 0 [y/x].
The barbed open bisimilarity ≈bopen is the largest barbed open bisimulation.
With a definition as complex as Definition 5, it is not very clear if the relation
it introduces is well behaved. The next lemma gives one some confidence on thebarbed open bisimilarity.
Lemma 6. ≈bopen is closed under localization and composition.

Since ≈bopen is closed under substitution, it must also be closed under prefix
operation. It is also clear that ≈bopen is closed under match operation. However
the relation is closed neither under the mismatch operation nor under the summation operation. For instance [x6=y]P ≈bopen [x6=y]τ.P does not hold. To obtainthe largest congruence contained in ≈bopen we use the standard approach.
Definition 7. Two processes P and Q are barbed congruent, notation P 'b Q,
τ
if P ≈bopen Q and for each substitution σ whenever P σ −→ P 0 then Q0 existsτsuch that Qσ =⇒ Q0 ≈bopen P 0 and vice versa.
The notation 'b is not confusing because it is also the largest congruence contained in ≈b . This is guaranteed by the next theorem.
Theorem 8. ≈bopen and ≈b coincide.

3

Axiomatic System

In this section we give a complete system for the barbed congruence on thefinite χ6= -processes. In order to prove the completeness theorem, we need some
auxiliary definitions.
Definition 9. Let V be a finite set of names. We say that ψ is complete on V
if n(ψ) ⊆ V and for each pair x, y of names in V it holds that either ψ ⇒ x=yor ψ ⇒ x6=y. A substitution σ is induced by ψ, and ψ induces σ, if σ agrees withψ and σσ = σ.
We now begin to describe a system complete for the barbed congruence.
Let AS denote the system consisting of the rules and laws in Figure 2 plus thefollowing expansion law:
πi =ai [xi ]P |Q =XiX

φi (x̃)πi .(Pi |Q) +φi ψj (x̃)(ỹ)[ai =bj ][xi |yj ].(Pi |Qj ) +γj =bj [yj ]πi =ai [xi ]Xjψj (ỹ)γj .(P |Qj ) +X

φi ψj (x̃)(ỹ)[ai =bj ][xi |yj ].(Pi |Qj )γj =bj [yj ]PPwhere P is i φi (x̃)πi .Pi and Q is j ψj (ỹ)γj .Qj , πi and γj range over {α[x] |α ∈ N ∪ N , x ∈ N }.
Using axioms in AS, a process can be converted to a process that contains
no occurrence of composition operator, the latter process is of special form as
defined below.
Definition
10. A processP
P P is in normal form
P on V ⊇ f n(P ) if P is of theform i∈I1 φi αi [xi ].Pi + i∈I2 φi (x)αi [x].Pi + i∈I3 φi [zi |yi ].Pi such that x does
not appear in P , φi is complete on V for each i ∈ I1 ∪ I2 ∪ I3 , Pi is in normal
form on V for i ∈ I1 ∪ I3 and is in normal form on V ∪ {x} for i ∈ I2 . Here I1 ,I2 and I3 are pairwise disjoint finite indexing sets.

T1
T2
T3
T4
T5
T6
T7
TD1

λ.τ.P = λ.P
P +τ.P = τ.Pλ.(P +τ.Q) = λ.(P +τ.Q)+λ.Q
τ.P = τ.(P +ψτ.P )[y|x].(P +δτ.Q) = [y|x].(P +δτ.Q)+ψδ[y|x].Q
F F = F F +[x6∈Y3 ][x6∈n(δ)]δα[x].Q[x/z]F R = F R+[x6∈Y3 ][x6∈n(δ)]δα[x].Q[x/z]RO = RO+δ(x)α[x].Q

C(ψ, δ)z6∈n(δ)z6∈n(δ)x6∈n(δ)Fig. 1. Tau Laws

The depth of a process measures the maximal length of nested prefixes in theprocess. The structural definition goes as 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 ),d([x6=y]P ) = d(P ); (vi) d(P +Q) = max{d(P ), d(Q)}.
Lemma 11. For a process P and a finite set V of names such that f n(P ) ⊆ V
there is a normal form Q on V such that d(Q) ≤ d(P ) and AS ` Q = P .
In order to obtain a complete system for the barbed congruence, we need some
tau laws, some of which are new and complex. Figure 1 contains seven tau laws
used in this paper. T4, introduced by the first author in previous publication, isa necessary law for open congruences. T5 holds under the condition C(ψ, δ):
If δ ⇒ [u6=v] then either ψ ⇒ [x=u][y6=v] or ψ ⇒ [x=v][y6=u] or ψ ⇒[y=u][x6=v] or ψ ⇒ [y=v][x6=u] or ψ ⇒ [x6=u][x6=v][y6=u][y6=v].
This law was used for the first time in [5]. The laws T6 and T7 are equational
formalization of the examples given in Section 2 in a more general form. In theseaxioms, F F (respectively F R) stands for
α[x].(P +δ[x6∈Y1 ∪ . . . ∪ Y5 ]τ.Q[x/z])(respectively (z)α[z].(P +[x6∈n(δ)]δ[z6∈Y1 ∪ . . . ∪ Y5 ][z|x].Q))+Σy∈Y1 α[x].(Py +δ[x=y]τ.Q[x/z])+Σy∈Y2 (z)α[z].(Py +[x6∈n(δ)]δ[z=y][z|x].Q)+Σy∈Y3 [x6=y]α[y].(Py +[x6∈n(δ)]δ[y|x].Q[x/z])+Σy∈Y4 [y|x].(Py +δα[y].(Py0 +δτ.Q[x/z]))+Σy∈Y5 [y|x].(Py +δ(z)α[z].(Py0 +δ[z=y]τ.Q))
These two laws are new. In TD1, which is derivable from T6, RO isΣy∈Y1 α[y].(Py +δτ.Q[y/x]) + Σy∈Y2 (x)α[x].(Py +δ[x=y]τ.Q)+ (x)α[x].(P +δ[x6∈Y1 ∪ Y2 ]τ.Q)
Let AS ∪ {T 1, T 2, T 3, T 4, T 5, T 6, T 7} denote ASob . Without further ado, we
state the main result of this section.
Theorem 12. ASob is sound and complete for 'b .

4Ground Congruence

In this section we sketch some main properties about ≈g . First of all the groundbisimilarity can be characterized by an open bisimilarity called ground open
bisimilarity, notation ≈gopen . The definition of the ground open bisimilarity is
obtained from Defintion 5 by replacing clause (ii) by
α[x]

α[x]

(ii’) If P −→ P 0 then Q0 exists such that Q =⇒ Q0 RP 0 .
It is easy to prove that ≈gopen is closed under localization and composition andthat ≈gopen coincides with ≈g . By definition the ground open bisimilarity is contained in the barbed one. The inclusion is strict because T7 is not valid for≈gopen .
Let 'g be the largest congruence contained in ≈gopen . Its formal definition iscompletely similar to that of 'b . Let ASog stand for AS∪{T 1, T 2, T 3, T 4, T 5, T 6}.
It can be similarly proved that ASog is sound and complete for 'g .

5

RemarkParrow and Victor have studied fusion calculus ([7]). It is a polyadic versionof χ6= -calculus. The main observational equivalence they have studied is what
they call weak hyperequivalence. The weak hyperequivalence is essentially apolyadic version of the open bisimilarity ≈o we have defined in the introduction.
Since χ6= -calculus is a monadic version of the fusion calculus and therefore is asubcalculus of the latter, the counter example given in the introduction is valid
in fusion calculus as well. One of the motivations of the ground bisimilarity is
to rectify the weak hyperequivalence. Apart from its theoretical interest, thebarbed bisimilarity is introduced partly to study the ground bisimilarity.

References
1. Y. Fu. A Proof Theoretical Approach to Communications. ICALP’97 , Lecture
Notes in Computer Science 1256, Springer, 325–335, 1997.
2. Y. Fu. Bisimulation Lattice of Chi Processes. ASIAN’98 , Lecture Notes in Computer Science 1538, Springer, 245–262, 1998.
3. Y. Fu. Variations on Mobile Processes. Theoretical Computer Science, 221: 327368, 1999.
4. Y. Fu. Open Bisimulations of Chi Processes. CONCUR’99 , Eindhoven, The
Netherlands, August 24-27, Lecture Notes in Computer Science 1664, Springer,
304-319, 1999.
5. Y. Fu, Z. Yang. Chi Calculus with Mismatch. CONCUR 2000 , Pennsylvania, USA,
August 22-25, Lecture Notes in Computer Science 1877, Springer, 2000.
6. R. Milner, J. Parrow, D. Walker. A Calculus of Mobile Processes. Information andComputation, 100: 1-40 (Part I), 41-77 (Part II), Academic Press.
7. J. Parrow, B. Victor. The Fusion Calculus: Expressiveness and Symmetry in Mobile
Processes.
8. J. Parrow, D. Sangiorgi. Algebraic Theories for Name-Passing Calculi. Journal of
Information and Computation, 120: 174-197, 1995.

E1
P =P
E2
P =Q
if Q = P
E3
P =R
if P = Q and Q = R
C1
α[x].P = α[x].Q
if P = Q
C2(x)P = (x)Q
if P = Q
C3a[x=y]P = [x=y]Q
if P = Q
C3b[x6=y]P = [x6=y]Q
if P = Q
C4
P +R = Q+R
if P = Q
C5
P0 |P1 = Q0 |Q1
if P0 = Q0 and P1 = Q1
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)[x=y]P = 0x6=yL7(x)(P +Q) = (x)P +(x)QL8(x)[y|z].P = [y|z].(x)Px 6∈ {y, z}L9(x)[y|x].P = τ.P [y/x]y 6= xL10(x)[x|x].P = τ.(x)P
M1
φP = ψP
if φ ⇔ ψM2[x=y]P = [x=y]P [y/x]M3a [x=y](P +Q) = [x=y]P +[x=y]Q
M3b [x6=y](P +Q) = [x6=y]P +[x6=y]QM4
P = [x=y]P +[x6=y]PM5[x6=x]P = 0
S1
P +0 = P
S2
P +Q = Q+P
S3
P +(Q+R) = (P +Q)+R
S4
P +P = PU1[y|x].P = [x|y].P
U2[y|x].P = [y|x].[x=y]P
U3[x|x].P = τ.P

Fig. 2. Axiomatic System AS

LD1 (x)[x|x].P = [y|y].(x)PU3 and L8
LD2 (x)[y6=z]P = [y6=z](x)P
L5, L7 and M4
LD3 (x)[x6=y]P = (x)P
L6, L7 and M4
MD1[x=y].0 = 0
S1, S4 and M4
MD2 [x=x].P = P
M1
MD3
φP = φ(P σ) where σ is induced by φ
M2
SD1
φP +P = P
S-rules and M4
UD1[y|x].P = [y|x].P [y/x]U2 and M2

Fig. 3. Some Laws Derivable from AS