On Quasi Open Bisimulation∗
Yuxi Fu†
Department of Computer Science
Shanghai Jiaotong University, Shanghai 200030, China

Abstract
Quasi open bisimilarity is a variant of the open bisimilarity based on a closer examination of theobservationality of local names. The paper investigates two alternative characterizations of the quasi
open bisimilarity and provides a complete system for the weak quasi open congruence.

1

Introduction

In the theory of process calculus, mobility is formalized by the communication mechanism that allows
names to be sent and received by the communicating processes. This idea was formally investigatedby Milner, Parrow and Walker in [10] for the first time within the framework of the π-calculus. For
an expository introduction to the π-calculus and its variants, see [15]. Through name updates, mobile
processes may change their communication topologies during their evolutions. This dynamic feature adds
to the difficulties of defining the equivalence relations for the mobile processes.
Equivalence relations on mobile processes are observational, meaning that two processes are equated
if no environments can observe any difference by interacting with them. Formally the environments
are represented by the contexts. When a process P is placed in an environment C[ ], it is observed by
the environment by letting the environment interact with it. Intuitively P and Q are observationallyequivalent if an arbitrarily chosen environment C[ ] can not tell which of the two is placed within it.
Now the input prefixes in C[ ] might bind free names in the process placed within it. Consequently
observational equivalences on mobile processes are closed under substitution. One such equivalence is theopen bisimilarity proposed by Sangiorgi [13]. This relation differs from other bisimulation equivalencesin that it is closed under substitution in every bisimulation step. This stronger requirement is reasonablefrom the point of view of modern computing framework. In the scenario of internet computing, not only
the programmes are mobile and therefore must be robust enough to survive in different environments, butalso that the environments are changing all the time and programmes are under constant attacks fromthe environments. What it implies to the process equivalences is that the environments are dynamic in
the sense that after an environment has made an observation it might become randomly different. Let’ssee a well-known example: We have two π-processes defined as follows:
A
B

def

=

def

=

aa.bb + aa
A + aa.[x=y]bb

They are not open bisimilar. Suppose C[ ] is a context and that it is ready to interact with A and Bτthrough channel a. Clearly the observation C[B] −→ C 0 [[x=y]bb] is admissible. Now A admits the sameττ
observation in two manners: Either C[A] −→ C 0 [bb] or C[A] −→ C 0 [0]. In the π-calculus, C 0 [ ] can notobserve any difference between [x=y]bb and 0 if x 6= y and between [x=y]bb and bb if x = y. But according
to the above analysis, we should not take for granted that after the first observation the environment is
C 0 [ ]. It might well have changed into C 00 [ ] that contains a prefix ‘c(x).’ in front of the hole. It is possiblethat a sequence of observations of C 00 [[x=y]bb] is admissible neither by C 00 [bb] nor by C 00 [0]. From the∗ The paper has appeared in Theoretical Computer Science, 338: 96-126, 2005.
† The author is supported by The NNSFC for Distinguished Young Scholars (60225012) and The National 973 Project(2003CB316905).

aabisimulation point of view, the inequivalence can be explained as follows: The action B −→ [x=y]bb can
not be simulated by any action from A. A substitution either identifies x with y or leaves them distinct.
In the former case bb can be fired while in the latter case bb cannot be activated. So there is a choice forthe environment. However the choice of the environment is void after A has performed an aa action.
In retrospect one of the selling points of bisimulations is that they have taken into account themalicious nature of the environments. The zigzag property of the bisimulation is what is necessary to
uphold the soundness of the bisimulation equivalences against the dynamic environments. The weakbisimulation equivalence in CCS ([9]) can be understood in this interpretation. It is our personal belief
that the open bisimilarity can claim to be the bisimulation equivalence on the mobile processes.
A more interesting counter example to the open bisimilarity is given by Sangiorgi and Walker [14].
Consider the pair of the π-processes:
C
D

def

=

def

=

(z)az.(a(w) + a(w).zz + a(w).[w=z]zz)(1)(z)az.(a(w) + a(w).zz)(2)a(z) a(w)According to the definition of the open bisimulation C −→−→ [w=z]zz cannot be simulated by D. But
from an observational viewpoint, C and D should be equivalent. In an interacting environment thecomponent a(w).[w=z]zz could receive a name. This name could be one of the three kinds:• It is z. In this case [w=z]zz is equivalent to zz.
• It is a free name x. In this case [w=z]zz is equivalent to 0. This is because in the π-calculus thefree name x is never identified with the local name z.
• It is a local name different from z. In this case [w=z]zz is also equivalent to 0. This is because in
the π-calculus two distinct local names can never be identified.
So the component a(w).[w=z]zz could be simulated either by a(w).zz or by a(w). From a context pointof view the observations a context makes on (z)az.(a(w) + a(w).zz + a(w).[w=z]zz) and (z)az.(a(w) +a(w).zz) are the same. After the observation these two processes have evolved into a(w) + a(w).zz +a(w).[w=z]zz and a(w) + a(w).zz respectively. By the above analysis, the following observationτC[a(w) + a(w).zz + a(w).[w=z]zz] −→ C 0 [[x=z]zz]
by the context C[ ] can be made to a(w) + a(w).zz as well. This counter example points out a deficiencyof the open bisimilarity: The open semantics imposes too strong a requirement on names ‘opened up’ by
the bound output actions, which has hardly any practical significance. In order to rectify this deficiency,
Sangiorgi and Walker proposed quasi open bisimilarity in [14]. The quasi open bisimilarity is weaker thanthe open bisimilarity. For instance the processes defined in (1) and (2) are quasi open bisimilar although
they are not open bisimilar. Sangiorgi and Walker have worked out the relationship of the quasi open
bisimilarity to some of the well known bisimilarities. They have shown that the quasi open bisimilarity
coincides with the open barbed bisimilarity, where the open barbed bisimilarity differs from the barbed
equivalence in that the former is closed under substitution in every bisimulation step. In the light of theabove discussions this result definitely adds weight to the importance of the quasi open bisimilarity.
In summary, the open bisimilarity has a more authentic role to play than either the early bisimilarityor the late bisimilarity. Our previous work has shown that the open bisimulations are more subtle thanthey appear to be ([2]). As the rectification of the open bisimilarity, the quasi open bisimilarity definitely
calls for more attention.
In this paper we study the algebraic theory of the quasi open bisimilarity. The main contributions of
the paper are as follows:• We demonstrate the importance of the quasi open bisimilarity by showing that it is what one obtains
if one formalizes the idea of observations of the dynamic environments.
• We introduce an operation that removes match/mismatch operators involving local names that havejust been opened up. By using this operation we propose the Q-open bisimilarity that makes room
for a proof of a completeness result for the quasi open congruence. The equational system contains
a schematic rule that captures the difference between the open bisimilarity and the quasi open
bisimilarity. Thus we provide a full picture on the equality defined by the quasi open bisimulations.
2The paper is organized as follows. Section 2 introduces the preliminaries. Section 3 reviews thedefinitions and some basic properties of the quasi open bisimilarity. Section 4 does the same for the open
barbed bisimilarity. Section 5 and Section 6 provide two alternative characterizations of the quasi open
bisimilarity. Section 7 proposes a complete system for the quasi open congruence. Section 8 concludes.

2

Preliminary

The process calculus we focus in this paper is the full π-calculus equipped with the mismatch operator.
The abstract syntax of the calculus is given below:
P := 0 | π.P | P | P 0 | (x)P | [x=y]P | [x6=y]P | P +P 0 | !P
In the above definition π ranges over the set {a(x), ax | a, x ∈ N } ∪ {τ } and the small letters range overthe set N of names. In both a(x).P and (x)P the name x is bound. The bound output prefix is defined
as follows:defa(x).P = (x)ax.P
The notations n( ), f n( ) and bn( ) represent the sets of names, respectively free names and bound names,
in a syntactical object.
The operational semantics of the calculus is defined by the standard approach using a labelled transition system. In the following semantic rules, λ ranges over the set {ax, ax, a(x) | a, x ∈ N } ∪ {τ }.
Prefixayτax

τ.P −→ P

ax.P −→ P

a(x).P −→ P {y/x}Composition
λay

P −→ P 0ayax

P −→ P 0 Q −→ Q0
τP | Q −→ P 0 | Q0

λ

P | Q −→ P 0 | Q
Restriction
λP −→ P 0a(x)P −→ P 0 Q −→ Q0
τP | Q −→ (x)(P 0 | Q0 )ax

P −→ P 0

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

ConditionλλP −→ P 0

P −→ P 0λλ[x=x]P −→ P 0[x6=y]P −→ P 0

ChoiceλP −→ P 0λ

P +Q −→ P 0
Replication
λP | !P −→ P 0
λ!P −→ P 0
In the above transition system, we have left out all the symmetric rules. In the third composition rule, one
needs to use the α-conversion to rename a bound name so that the new name x does not occur in P . The
second condition rule says that for distinct names x and y the process [x6=y]P behaves in the same way
as the process P . In this paper we take the view that two names are different if they are syntacticallydistinct. To go along with this view, we assume that all bound names are pairwise distinct and are
different from the global names. This is why we have dropped the side condition bn(λ) ∩ f n(Q) = ∅ on
the first composition rule. The notation {y/x} stands for a substitution that replaces x by y throughout
the term it applies. Formally a substitution σ is a map from N to N such that {x | σ(x) 6= x ∧ x ∈ N }is finite. The notation P σ denotes the process obtained by replacing the free names in P according
to σ. A substitution is often written as {y1 /x1 , . . . , yn /xn }, indicating that it maps xi onto yi , fordefi ∈ {1, . . . , n}, and is constant elsewhere. If σ = {y1 /x1 , . . . , yn /xn } then n(σ) = {x1 , . . . , xn , y1 , . . . , yn }
def

def

and rng(σ) = {y1 , . . . , yn }. The composition σ1 σ2 of σ1 and σ2 is defined as follows: P σ1 σ2 = (P σ1 )σ2 .
3

The operational semantics we have defined is the early semantics, which is clear from the transition
a(x)

ay

a(x).P −→ P {y/x}. In the early semantics one has that a(x).P −→ P . The difference is that in theformer the instantiations of the input actions happen at the level of the observable actions while in thelatter they occur in the unobservable internal communications.
τλλLet =⇒ be the reflexive and transitive closure of −→. We will write =⇒ for =⇒−→=⇒. We will alsob
λ
λwrite =⇒ for =⇒ if λ 6= τ and for =⇒ otherwise.
A context is a process with a hole. Formally a context C[] is• either [];• or π.C 0 [] for some context C 0 [] and some prefix π;• or C 0 [] | P , or symmetrically P | C 0 [], for some strong context C 0 [] and some process P ;• or (x)C[] for some context C 0 [] and some name x;• or [x=y]C 0 [] for some context C 0 [] and some names x and y.
A strong context is either a context, or of the form C 0 [] + P , or symmetrically P + C 0 [], for some strong
context C 0 [] and some process P , or of the form [x6=y]C 0 [] for some strong context C 0 [] and names x, y.
We will abbreviate a sequence x1 , . . . , xn of names to xe. Accordingly (x1 ) . . . (xn )P will be abbreviatedto (ex)P . When the length of x
e is zero, (ex)P is just P . By abuse of notation, we will also write xe for the set{x1 , . . . , xn }. When the lengths of xe and ye are the same, we sometimes write {ey /ex} for the substitutionthat replaces each x ∈ xe by the corresponding y ∈ ye.
The following definition will play an important role in some major proofs of the paper. It is slightly
different from what is introduced in [14].
Definition 1. A substitution σ respects x
e if ∀x ∈ xe.xσ = x and ∀y 6∈ xe.yσ 6∈ xe.
It is clear that if both σ1 and σ2 respect x
e then σ1 σ2 respects x
e. This definition will be typicallyapplied to a sequence x
e of local names that have been opened up, as it were, by bound output actions.
A substitution respecting x
e pretends that x
e were still local names.
In the rest of this paper φ, ψ, φ0 , ψ 0 , . . . denote finite lists of match and/or mismatch conditions.
Consequently we will write φP and ψP etc.. If φ logically implies ψ, we write φ ⇒ ψ; and if both φ ⇒ ψand ψ ⇒ φ we write φ ⇔ ψ. If φ is an empty list, it plays the role of the logical truth, denoted by >, inwhich case φP is just P . Let ⊥ denote the logical false operator. One then has for example x6=y ⇔ ⊥.
When reasoning with process equality we sometimes write ⊥P for 0. Clearly φ defines an equivalence
relation on the set N of names. We write sφ to denote an arbitrarily chosen substitution that sends all
the members of an equivalence class to a representative of that class.
Lemma 2. Suppose σ is a substitution and ϕ is a sequence of matches and/or mismatches. For arbitrarily
chosen sϕσ and sϕ there exists some substitution σ 0 such that σsϕσ = sϕ σ 0 σ.
Proof. For any name a one has the following observations:• a is mapped by sϕ onto a representative a0 of the equivalence class [a], where the equivalence relation
is induced by ϕ;• a is mapped by σ onto aσ and then by sϕσ onto a representative a00 σ of the equivalence class [aσ],where the equivalence relation is induced by ϕσ.
Now define a substitution σ 0 as follows:
For each name a, let aσ 0 be a00 .
This substitution has the following property:
If a1 and a2 are in the same equivalence class [a] of the equivalence relation induced by ϕthen a1 σ 0 = a2 σ 0 .
This is because a1 σ, a2 σ must be in the same equivalence class of the equivalence relation induced by ϕσ.
It then follows easily that σsϕσ = sϕ σ 0 σ.
4

λ

λσ

In the full π-calculus, P −→ P 0 does not necessarily imply that P σ −→ P 0 σ. But the following
property clearly holds, which we will be using without explicitly referring to.
λ σ

λ

1
Lemma 3. If P σ −→ P 0 then there exist P1 and λ1 such that P σ −→P1 σ ≡ P 0 and λ = λ1 σ.

In some later proofs we will assume that the reader is familiar with the strong open bisimilarity ∼([13]) and the proof technique of bisimulation up to ∼ ([9]).

3Quasi Open Bisimulation

Sangiorgi and Walker introduced the quasi open bisimulations for the π-calculus with the motivations
explained in the introduction. The π-calculus they considered in [14] is the sub calculus without themismatch operator. For the open bisimulations, the presence of the mismatch operator slightly complicates the observational theory. It is pointed out in [2] that there are two principal definitions of the open
bisimulations which give rise to the early open bisimulations and the late open bisimulations. Here is an
example that distinguishes the two: Let P bea(x).(P0 +[x=y]τ.Q) + a(x).(P1 +[x6=y]τ.Q)
Then P +a(x).Q is early open bisimilar to P . But the two processes are not late open bisimilar. In thispaper we focus on the early open bisimilarity. Hencefourth we will leave out the adjective “early”.
Definition 4. A quasi open bisimulation is a family of symmetric relations {Rze}ze⊆f N on processes suchthat, for all P and Q, if P RzeQ and σ respects ze then the following properties hold:bλ(i) If P σ −→ P 0 , where λ is not a bound output action, then some Q0 exists such that Qσ =⇒ Q0 RzeP 0 .
λ(ii) If P σ −→ P 0 then Qσ =⇒ Q0 for some Q0 such that P 0 Rzex Q0 .
We write {≈zqe}ze⊆f N for the largest quasi open bisimulation and refer to ≈zqe as the quasi open ze-bisimilarity.
The quasi open bisimilarity ≈q is the quasi open ∅-bisimilarity ≈∅q .
a(x)

a(x)

The above definition is taken from [15]. Had we used a late operational semantics as in the paper [15]of Sangiorgi and Walker, then the input actions would call for a special treatment since the calculus
is equipped with the mismatch operator. The following simulating property, in the late operationalsemantics,“if P σ −→ P 0 then some Q0 exists such that Qσ =⇒ Q0 RzeP 0 ”
a(x)

a(x)

is good for the calculus without the mismatch operator but wrong for the present calculus. We refer thereader to [2] for detailed treatment.
A quasi open bisimulation is a family of binary relations indexed by the finite sets of names. Intuitively
P ≈zqe Q if P and Q are open bisimilar under the assumption that the names z̃ are not subject to attacks
from the environments. In other words, P ≈zqe Q if P and Q are open bisimilar assuming that theenvironments can neither replace a name in z̃ by another name nor identify any two names in z̃. So when
we assert that P ≈zqe Q, we regard the free names in f n(P | Q) ∩ z̃ as previous local names that havebeen opened up, as it were. It is easy to see that P ≈zqe Q implies that (ez )P ≈q (ez )Q. But the converse
implication does not hold.
For open bisimilarities, it is very important that they are closed under substitutions. Thus the next
lemma should be stated first.
Lemma 5. Suppose σ respects ze. If P ≈zqe Q then P σ ≈zqe Qσ.
Proof. It is easy to show that the relation Rze = {(P σ, Qσ) | P ≈zqe Q, σ respects ze} is a quasi open
bisimulation.
def

So the quasi open bisimilarity ≈q is indeed preserved by substitution. The other closure properties
follow from Lemma 5, whose proof is routine and therefore is omitted1 .
Lemma 6. The relation ≈q is an equivalence relation and is closed under all but the choice combinator.
1 Lemma 6 is misstated in [1].

5

Next we prove a couple of technical results to be used later on.
Lemma 7. If P ≈zqex Q and x 6∈ f n(P | Q) then P ≈zqe Q.
Proof. Suppose P ≈zqex Q and x 6∈ f n(P | Q). If for instance P σ −→ P 0 for some σ respecting ze thenτP σ 0 −→ P 0 by assumption, where σ 0 may differ from σ only in that σ 0 (x) = x. Clearly σ 0 respects zex. It
follows from P ≈zqex Q that some Q0 exists such that Qσ 0 =⇒ Q0 ≈zqex P 0 . Thus Qσ =⇒ Q0 ≈zqex P 0 andx 6∈ f n(P 0 | Q0 ). This is enough to show how the bisimulation argument can be completed.
τ

Corollary 8. Suppose P ≈zqex Q. Then for each A it holds that (x)(P | A) ≈zqe (x)(Q | A).

4

Open Barbed Bisimulation

This section serves to introduce a result in [15]. The result is to be used in the next section to establish
an alternative view of the quasi open bisimilarity.
The barbed bisimulations are proposed in [11] as a general method to define an observational equivalence. The idea is that two processes are equivalent if they can simulate each other’s ability to communicate at particular channels. This ability is characterized as a relation between the processes and thechannel names. For simplicity we will bypass this relation. The barbed relation defined below is nonstandard. But it is equivalent to the standard one ([11]) in the sense that the largest barbed bisimulations
they give rise to are the same.
Definition 9. A symmetric relation R is a barbed bisimulation if whenever hP, Qi ∈ R then the following
properties hold:τ(i) If P −→ P 0 then Q =⇒ Q0 RP 0 for some Q0 .
λλ(ii) If P −→ P 0 for λ 6= τ then Q =⇒ Q0 for some Q0 .
The barbed bisimilarity ≈b is the largest barbed bisimulation.
It is clear that if two processes are barbed bisimilar then they can simulate each other’s next observableactions. So the philosophy of the barbed bisimilarity can be stated as follows:
Two processes are equivalent if no matter what a state one process has evolved into the otherprocess can always reach to a state such that the two processes in the new states can simulate
each other’s next observable actions.
The barbed bisimilarity is too loose to be useful in practice. To refine the relation one must take
into account the environments. There are two ways to make use of the environments. One is the static
approach. Milner and Sangiorgi used this approach in [11] in their definition of the barbed equivalence.
Definition 10. Two processes P, Q are barbed equivalent, notation P ≈eb Q, if C[P ] ≈b C[Q] for every
context C[ ].
The barbed equivalence is a tricky one. There are proofs, say the ones in [15], of the coincidence of≈eb with the early equivalence under some conditions, but the general coincidence result has not beenλestablished. It is easy to show that if Q ≈eb P −→ P 0 for a non-bound action λ then there is some Q0b
λsuch that Q =⇒ Q0 ≈eb P 0 . But this bisimulation property has not been established for the bound output
a(x)

a(x)

actions. What one has proved is that whenever Q ≈eb P −→ P 0 then Q =⇒ Q0 such that C[P 0 ] ≈eb C[Q0 ]for some Q0 and for all contexts C[ ] that localize x.
The other is the dynamic approach. This is the one adopted in the next definition due to Sangiorgi
and Walker, see [15].
Definition 11. An open barbed bisimulation is a barbed bisimulation closed under context. The open
barbed bisimilarity ≈ob is the largest open barbed bisimulation.
The open barbed bisimilarity is closed under context at every bisimulation step. The property implies
that it is closed under substitution as well. This leads to the following result due to Sangiorgi and Walker,
see [15].
Proposition 12. The equivalence relations ≈ob and ≈q coincide.
6

The inclusion ≈q ⊆≈ob is easy. For the converse inclusion the intuition is to show that the relations
R , for finite sequence x
e of names, defined below constitute a quasi open bisimulation:xee.C[P ] ≈ob C[Q]}{(P, Q) | ∀C[ ] bounds x
As a matter of fact one only has to consider contexts of the special form(x1 ) . . . (xn )(!a1 x1 | . . . | !an xn | )Proposition 12 provides an interesting characterization of the quasi open bisimilarity. The easy proofof this coincidence result is a support to the quasi open bisimulations.

5

Q-Open Bisimulation

A quasi open bisimulation is a family of relations indexed by sets of names. Often a single relation istechnically more convenient than a family of relations. This section sets out to provide an alternative
characterization to the quasi open bisimulations. This alternative is a single relation rather than a familyof indexed relations, satisfying the condition that the largest such relation coincides with the quasi open
bisimilarity. The trade-off for a single relation is that we need to introduce a new construction, noted( )ze, that operates on conditions and processes. The effect of this operation on conditions is defined asfollows:()ze

def([x=y]ψ)ze

def([x6=y]ψ)ze

def

>

 [x=y]ψ ze,
ψ ze,

⊥,

 [x6=y]ψ ze,
⊥,
 ze
ψ ,

=

=

=

if ze ∩ {x, y} = ∅if ∃z ∈ ze.x = z = yotherwise
if ze ∩ {x, y} = ∅if ∃z ∈ ze.x = z = yotherwise

Intuitively the condition ψ z is obtained by removing the matches and the mismatches in ψ that involve aname in z̃. If we think of a name z in z̃ as a special name that can never be replaced by or identified to any
other name, then a condition of the form [x=z]ψ 0 or of the form [z6=z]ψ 0 is as good as 0 and a conditionof the form [x6=z]ψ 0 or of the form [z=z]ψ 0 behaves just like ψ 0 . This explains the clause concerning thematch and the mismatch. When the operation ( )ze applies to an empty list of match/mismatch operators
it returns the logical truth. The proof of the next lemma is a simple structural induction.
Lemma 13. If σ respects ze then ψ zeσ = (ψσ)ze.
The structural definition of the operation on processes is given below:
(0)ze

def

=

0

z
e

def

X
a(x).( [x=z](P {z/x})ze + [x6∈ze]P ze), where x 6∈ ze(τ.P )zedef

τ.P ze((x)P )zedef

(P +Q)ze(x)P ze, where x 6∈ ze

def=

P ze+Qze([x=y]P )ze

def=([x=y])zeP ze([x6=y]P )ze

def=([x6=y])zeP ze(!P )ze

def

!P ze

(a(x).P )

=

z∈z
e

=
=

=

To appreciate the clause about the input prefix, one only has to notice that P z {z/x} 6≡ (P {z/x})z . For
instance let P be [z=x]aa. Then P z {z/x} is 0 whereas (P {z/x})z is aa. Had we defined (a(x).P )ze asfollows:def(a(x).P )ze = a(x).P ze
7then (a(x).[z=x]aa)ze would be a(x).0. This is apparently wrong since the input might receive the namez and the action aa can then be fired.
In the above definition we have not considered the parallel composition operator. In the rest of thepaper we shall assume that a process is free of composition operator when applying ( )ze to it. It should
be noticed that none of the names in ze appears in any of the match/mismatch in P ze.
As a warming-up exercise, we prove the following lemma.
Lemma 14. Suppose a is fresh. Then (x)(P | ax) ≈q (x)(P x | ax).
Proof. We prove by structural induction that (x)(C[P ] | ax) ≈q (x)(C[P x ] | ax), where C[ ] is a context
and x is not bound by C[]. We take a look at two cases:• P ≡ [u=v]P1 . There are three cases:– x 6∈ {u, v}. Then(x)(C[P ] | ax) ≈q
≈q
≈q
≈q

(x)(C[[u=v]P1 ] | ax)(x)(C[[u=v]P1x ] | ax)(x)(C[([u=v]P1 )x ] | ax)(x)(C[P x ] | ax)(x)(C[P ] | ax) ≈q
≈q
≈q
≈q
≈q

(x)(C[[x=x]P1 ] | ax)(x)(C[P1 ] | ax)(x)(C[P1x ] | ax)(x)(C[([x=x]P1 )x ] | ax)(x)(C[P x ] | ax)– u = x = v. Then– x ∈ {u, v} and u 6= v. Then(x)(C[P ] | ax) ≈q
≈q
≈q
≈q

(x)(C[[u=v]P1 ] | ax)(x)(C[0] | ax)(x)(C[([u=v]P1 )x ] | ax)(x)(C[P x ] | ax)• P ≡ c(z).P1 . Then(x)(C[P ] | ax) ≈q
≈q
≈q
≈q
≈q
≈q
≈q

(x)(C[c(z).P1 ] | ax)(x)(C[c(z).([z=x]P1 + [z6=x]P1 )] | ax)(x)(C[c(z).([z=x]P1 {x/z} + [z6=x]P1 )] | ax)(x)(C[c(z).([z=x](P1 {x/z})x + [z6=x]P1 )] | ax)(x)(C[c(z).([z=x](P1 {x/z})x + [z6=x]P1x )] | ax)(x)(C[(c(z).P1 )x ] | ax)(x)(C[P x ] | ax)

This completes the proof.
We now establish the key property for the operation ( )ze, which states that P ≈zqe Q if and only if
P ≈q Qze. In some sense the operation ( )ze transfers an external judgement to an internal assertion.
Putting in different words, P ≈zqe Q is a judgement with the assumption on the names z̃ whereas P ze ≈q Qze
is an assertion made by working out the conditions in P, Q that involve names in z̃. The proof of thisproperty makes use of the following four lemmas whose proofs are routine structural inductions.
zeLemma 15. If σ respects ze then P zeσ ≡ (P σ)ze.
8Lemma 16. Suppose σ respects ze and λ is not an input prefix. Then the following properties hold:λλ(i) If P σ −→ P1 then P zeσ −→ P1ze.

(ii) If P zeσ −→ P 0 then some P1 exists such that P σ −→ P1 and P1ze ≡ P 0 .
λλLemma 17. If (ψP )zeσ −→ P 0 for some σ respecting ze then P zeσ −→ P 0 .
λλAll the three lemmas deal with properties about P zeσ if the substitution σ leaves the names ze unchanged and untouched. Lemma 15 says that a ze-respecting substitution commutes with the operation( )ze. Lemma 16 states that if a ze-respecting substitution enables an action in P it also enables the sameaction in P ze, and vice versa. Lemma 17 states similar property. All are based on Lemma 13.
Proposition 18. Suppose ye ∩ ze = ∅. Then P ≈yqeze Q if and only if P ye ≈zqe Qye.
Proof. Let Rze be{(P yeσ, Qyeσ) | P ≈yqeze Q ∧ ze ∩ ye = ∅ ∧ (σ respects ze)}

Suppose σ 0 respects ze and P yeσσ 0 −→ P 0 . Then σσ 0 respects ze. For each y ∈ ye, let y 0 be a distinct freshname not in f n(P σσ 0 ) ∪ f n(Qσσ 0 ). Let σ1 be defined as follows:
if x = y ∈ ye
 y,
def
y0 ,
if (x 6∈ ye) ∧ (σ 0 (σ(x)) = y ∈ ye) ∧ (x ∈ f n(P ) ∪ f n(Q))σ1 (x) = 0
σ (σ(x)), if (x 6∈ ye) ∧ (σ 0 (σ(x)) 6∈ ye)
λThe substitution σ1 is modified from σ 0 σ in such a way that it respects ze as σ does and that it respects
ye even if σ does not. It is clear that σσ 0 and σ1 {ey /ye0 , yeσσ 0 /ey } coincide on f n(P ) ∪ f n(Q).

Now suppose P yeσσ 0 −→ P 0 is induced by a summand ψi λi .Pi of P . If λ is not an input action
then clearly λ = λi σσ 0 . By the fact that σσ 0 satisfies the head condition of (ψi λi .Pi )ye and that the head
λi 1
condition of (ψi λi .Pi )ye does not contain any name in ye, one infers that σ1 satisfies ψi . Then P σ1 −→Pi σ1 .
Now λ could be a free output action, a bound output action or a tau action. We consider them in turn:λ σ• λ is a tau action or a free output action. By Lemma 15,
P 0 ≡ Piyeσσ 0 ≡ Piyeσ1 {ey /ye0 , yeσσ 0 /ey } ≡ (Pi σ1 )ye{ey /ye0 , yeσσ 0 /ey}i 1By definition some Q0 exists such that Qσ1 =⇒Q0 σ1 ≈yqeze Pi σ1 . This sequence of actions must be
induced by a summand ψj λj .Qj of Q. Now the head condition in (ψi λi .Pi )ye is satisfied by σσ 0 .
λi σσ 0
Therefore Qyeσσ 0 =⇒(Q0 σ1 )ye{ey /ye0 , yeσσ 0 /ey }. Henceλ σ(Pi σ1 )ye{ey /ye0 , yeσσ 0 /ey }Rze(Q0 σ1 )ye{ey /ye0 , yeσσ 0 /ey}since {ey /ye0 , yeσσ 0 /ey } respects ze.
• λ is a bound output action a(x). By Lemma 15,
P 0 ≡ Piyeσσ 0 ≡ Piyeσ1 {ey /ye0 , yeσσ 0 /ey } ≡ (Pi σ1 )ye{ey /ye0 , yeσσ 0 /ey}i 1By definition some Q0 exists such that Qσ1 =⇒Q0 σ1 and Pi σ1 ≈yqezex Q0 σ1 . This sequence of actions
must be induced by a summand ψj λj .Qj of Q. Now the head condition in (ψi λi .Pi )ye is satisfied byλi σσ 0
σσ 0 . Therefore Qyeσσ 0 =⇒(Q0 σ1 )ye{ey /ye0 , yeσσ 0 /ey }. Henceλ σ(Pi σ1 )ye{ey /ye0 , yeσσ 0 /ey }Rzex (Q0 σ1 )ye{ey /ye0 , yeσσ 0 /ey}
If λ is an input action aw then λi = ai (x), for some ai and fresh x, and λ = ai σσ 0 w. It is clear thatP 0 ≡ Piyeσσ 0 {w/x} ≡ Piyeσ1 {ey /ye0 , yeσσ 0 /ey }{w/x} ≡ (Pi σ1 )ye{ey /ye0 , yeσσ 0 /ey}
By definition some Q1 , Q2 exist such thatQσ1 =⇒ −→ Q1 σ1 {w/x} =⇒ Q2 σ1 {w/x} ≈yqeze Pi σ1 {w/x}(aσ1 )w

9Without losing generality we may assume that
P yeσ1(aσ1 )w−→

X( [x=y](Pi {y/x})ye + [x6∈ye]Piye)σ1 {w/x}
y∈y
e

and
Qyeσ1

X
( [x=y](Q1 {y/x})ye + [x6∈ye]Qy1e)σ1 {w/x}(aσ1 )w

=⇒ −→

y∈y
e

To proceed notice that there are two subcases:• w = y ∈ ye. ThenX
( [x=y](Q1 {y/x})ye + [x6∈ye]Qy1e)σ1 {w/x}≡. . . + [x=y](Q1 {y/x})yeσ1 {w/x} + . . .

≡. . . + [y=y]Qy1eσ1 {w/x} + . . .

y∈ye=⇒ Qy2eσ1 {w/x}

because x is a bound name. It follows thatX
(aσ1 )w
Qyeσσ 0 =⇒ −→ ( [x=y](Q1 {y/x})ye + [x6∈ye]Qy1e)σσ 0 {w/x}
y∈y
e

and

X
( [x=y](Q1 {y/x})ye + [x6∈ye]Qy1e)σσ 0 {w/x} =⇒ (Q2 σ1 {w/x})ye{ey /ye0 , yeσσ 0 /e
y}
y∈y
e

• w 6∈ ye. ThenX
( [x=y](Q1 {y/x})ye + [x6∈ye]Qy1e)σ1 {w/x}≡. . . + [x=y](Q1 {y/x})yeσ1 {w/x} + . . .

≡. . . + [w6∈ye]Qy1eσ1 {w/x}y∈ye=⇒ Qy2eσ1 {w/x}
So in this case we also haveQyeσσ 0(aσ1 )w=⇒(Q2 σ1 {w/x})ye{ey /ye0 , yeσσ 0 /ey}

We conclude that Rze is a quasi open bisimulation. Consequently P ≈yqeze Q implies P ye ≈zqe Qye.
To prove the reverse implication, let S yeze be {(P, Q) | P ye ≈zqe Qye ∧ ze ∩ ye = ∅}. Suppose P S yezeQ and σrespects yeze. Suppose further that P σ −→ P1 . Then P yeσ −→ P1ye.
λλ• λ is a tau action or a free output action. Since P ye ≈zqe Qye one has some Q1 such that Qyeσ =⇒λQy1e ≈zqe P1ye. Now Qσ =⇒ Q1 because σ respects ye. Also P1 S yezeQ1 by definition.
λ• λ is an input action aw and λi = ai (x), for some ai , x, and λ = ai σσ 0 w. Some Q1 exists such thatX
λQyeσ =⇒−→ ( [x=y](Q1 {y/x})ye + [x6∈ye]Qy1e){w/x}
y∈y
e

and

X
( [x=y](Q1 {y/x})ye + [x6∈ye]Qy1e){w/x} =⇒ Qy2e{w/x} ≈zqe P1ye{w/x}y∈ye

It follows that Qσ =⇒−→ Q1 {w/x}, Q1 {w/x} =⇒ Q2 {w/x} and (P1 {w/x})ye ≈zqe (Q2 {w/x})ye.
Thus P1 {w/x}S yezeQ2 {w/x}.
λ

10• λ is a bound output action a(x). Some Q1 exists such that Qyeσ =⇒ Qy1e and P1ye ≈zqex Qy1e. NowλQσ =⇒ Q1 because σ respects ye and P1 S yezex Q1 by definition.
λThis completes the proof.
The lemma says that ()ze is an internalization operator as it were. Using this operator one cangive an alternative characterization of the quasi open bisimilarity. Now in Definition 4 only the clauseon the restricted output actions introduces the indexes on the quasi open bisimulations. According
to Proposition 18, the indexed equivalence P ≈zqe Q can be transposed to a non-indexed equivalence
P ze ≈q Qze. These observations suggest to use the operation ()ze in place of the index ze in the definition of
the quasi open bisimulations. The selling point of the new definition is that it introduces a single relation
rather than an indexed family of relations. This has advantage when it comes to axiomatization.
Definition 19. Suppose R is a symmetric binary relation closed under substitution. The relation R isa q-open bisimulation if the following properties hold whenever P RQ:bλλ(i) If P −→ P1 , where λ is not a bound output, then some Q1 exists such that Q =⇒ Q1 RP1 .
a(x)

a(x)

(ii) If P −→ P1 then some Q1 exists such that Q =⇒ Q1 and P1x RQx1 .
The q-open bisimilarity ≈qo is the largest q-open bisimulation.
The following proposition enforces the above definition.
Proposition 20. P ≈zqe Q if and only if P ze ≈qo Qze.
a(x)Proof. (i) By Lemma 5, ≈lq is closed under substitution. Suppose P ≈lq Q. If P −→ P1 then Q1 existsa(x)such that Q =⇒ Q1 and P1 ≈xq Q1 . Using Proposition 18, one has that P1x ≈q Qx1 . It follows that ≈lq is aq-open bisimulation, which implies that ≈lq ⊆≈qo . By Proposition 18, P ≈zqe Q implies P ze ≈lq Qze, which
in turn implies P ze ≈qo Qze.
(ii) Conversely {Rze}ze, where Rze = {(P, Q) | P ze ≈qo Qze}, is a quasi open bisimulation. It is clearthat Rze is closed under substitution respecting ze. So we do not have to consider substitutions in thefollowing argument. Now suppose P RzeQ.
def• If P −→ P1 then P ze −→ P1ze by Lemma 16. Since P ze ≈qo Qze, there must exist some Q1 such that
a(x)

a(x)

Qze =⇒ Q0 and P1zex ≈qo (Q0 )x . By Lemma 16, Q =⇒ Q1 for some Q1 such that Qz1e ≡ Q0 . It follows
that P1 Rzex Q1 .
a(x)

a(x)

aw

• If P −→ P10 then, by the definition given on page 7, one has, without losing generality, thatXaw
P ze −→ P 0 ≡ ( [x=z](P1 {z/x})ze + [x6∈ze]P1ze){w/x}z∈zefor some P1 such that P10 ≡ P1 {w/x}. Since P ze ≈qo Qze, there must exist some Q0 such thataw
Qze =⇒−→ Q0 =⇒ Q00 and P 0 ≈qo Q00 . Again by the definition given on page 7, Q0 must be of theformX( [x=z](A{z/x})ze + [x6∈ze]Aze){w/x}
z∈z
e

aw

Then clearly Q =⇒−→ A{w/x}. By Lemma 16, some A1 exists such that A{w/x} =⇒ A1 andAz1e ≡ Q00 . We need to show that A1 RzeP10 , which is the same as to showing that Az1e ≈qo (P10 )ze.
Since P 0 ≈qo Q00 and Az1e ≡ Q00 , it amounts to showing thatX
[w=z](P1 {z/x})ze + [y6∈ze]P1ze{w/x} ≈qo (P10 )ze
(3)
z∈z
e

If we can prove thatand[w6∈ze]P1ze{w/x} ≈qo [w6∈ze](P1 {w/x})ze(4)[w=z](P1 {z/x})ze ≈qo [w=z](P1 {w/x})ze

(5)

11

for each z ∈ ze, then (3) is derivable from
(P1 {w/x})ze ≈qo (P10 )ze
To see (4) observe that if w ∈ ze then both [w6∈ze]P1ze{w/x} and [w6∈ze](P1 {w/x})ze are bisimilar to 0;
if w 6∈ ze then [w6∈ze]P1ze{w/x} ≡ [w6∈ze](P1 {w/x})ze by Lemma 15. For (5) we only have to consider
the situation when w = z. In this case it is obvious that[w=z](P1 {z/x})ze ≡ [w=z](P1 {w/x})ze
Remember that we only have to consider substitutions that respect ze.
• Other cases are simpler.
This completes the proof.
Corollary 21. The two relations ≈q , ≈qo coincide.

6

Local Open Bisimulation

One objection to the standard early and late bisimilarities, as well as the open bisimilarity, is that the
restricted output actions are treated in completely the same manner as the other observable actions.
From the viewpoint of bisimulation equivalence, a free output action of one process must be simulatedby the same free output action of an equivalent process in order for the two processes to exert the sameobservable effect on an environment. For bound output actions, the situation is slightly different. Sincea(x)in π-calculus a local name will remain local forever, it is too much to require that the action P −→ P 0a(x)be simulated by Q =⇒ Q0 for equivalent P and Q. In other words it is too much to say that P 0 and Q0
should be equivalent. The most we could ask for is that P 0 and Q0 to be equivalent in any context inwhich the name x is localized. This brings us to the following definition.
Definition 22. A symmetric relation R on π-processes is a local open bisimulation if it is closed undersubstitution and whenever P RQ then the following properties hold:λλ(i) If P −→ P 0 , where λ is not a bound output, then some Q0 exists such that Q =⇒ Q0 and P 0 RQ0 ;
a(x)

a(x)

(ii) If P −→ P 0 then, for each process A, some Q0 exists such that Q =⇒ Q0 and (x)(P 0 | A)R(x)(Q0 | A).
The local open bisimilarity ≈lo is the largest local open bisimulation.
Definition 22 proposes yet another treatment of the restricted output actions: In the simulation
a(x)

a(x)

Q =⇒ Q0 of P −→ P 0 the equivalence between P 0 and Q0 is tested in ‘local contexts’ of the form(x)( | A). This is more reasonable than requiring that P 0 and Q0 be tested in all contexts.
Like the quasi open bisimilarity, the local open bisimilarity ≈lo enjoys the following closure property.
Lemma 23. The relation ≈lo is closed under prefix, composition, match and restriction operations.
Proof. It is easy to see that the relation is closed under the prefix and match operations. The proofs forthe parallel composition and restriction operations are carried out at one go. Let R be{((x̃)(P | R), (x̃)(Q | R)) | P ≈lo Q}
We show that R is a local bisimulation up to ∼. We take a look at a few cases:λ• If λ is a tau action, an input action or a free output action and (x̃)(P | R) −→ (x̃0 )(P 0 | R0 ) is caused
λλeither by P −→ P 0 or by R −→ R0 , then the simulation is simple.
a(y)

a(y)

a(y)

• (x̃)(P | R) −→ (x̃)(P | R0 ) is caused by R −→ R0 . Then (x̃)(Q | R) −→ (x̃)(Q | R0 ) and for eachprocess A it holds that(y)((x̃)(P | R0 ) | A) ∼ (x̃)(P | (y)(R0 | A)) R (x̃)(Q | (y)(R0 | A)) ∼ (y)((x̃)(Q | R0 ) | A)

12

a(x)

ax

• (x̃)(P | R) −→ (x̃0 )(P | R0 ) is caused by R −→ R0 such that x ∈ x̃. Then the simulation is matcheda(x)up by (x̃)(Q | R) −→ (x̃0 )(Q | R0 ) and, for each process A,(x)((x̃0 )(P | R0 ) | A) ∼ (x̃)(P | (R0 | A)) R (x̃)(Q | (R0 | A)) ∼ (x)((x̃0 )(Q | R0 ) | A)
c(y)

c(y)

• (x̃)(P | R) −→ (x̃)(P 0 | R) is caused by P −→ P 0 . Then, for each process A, some Q0 exists such
c(y)

c(y)

that Q =⇒ Q0 and (y)(P 0 | A) ≈lo (y)(Q0 | A). Clearly (x̃)(Q | R) =⇒ (x̃)(Q0 | R) and(y)((x̃)(P 0 | R) | A) ∼ (x̃)((y)(P 0 | A) | R) R (x̃)((y)(Q0 | A) | R) ∼ (y)((x̃)(Q0 | R) | A)
c(x)

cx

• (x̃)(P | R) −→ (x̃0 )(P 0 | R) is caused by P −→ P 0 such that x ∈ x̃. Then some Q0 exists such that
c(x)

cx

Q =⇒ Q0 ≈lo P 0 . Therefore (x̃)(Q | R) =⇒ (x̃0 )(Q0 | R) and, for each process A,(x)((x̃0 )(P 0 | R) | A) ∼ (x̃)(P 0 | (R | A)) R (x̃)(Q0 | (R | A)) ∼ (x)((x̃0 )(Q0 | R) | A)
The proof is completed.
It appears from Definition 22 that it is very untractable to check if two processes are local open
bisimilar. The universal quantification over all processes in the fourth clause of the definition is a minus
for the equivalence. As a matter of fact the local open bisimilarity is not that untractable. The following
lemma is suggestive.
Lemma 24. If (x)(P | ax) ≈lo (x)(Q | ax) for a 6∈ f n(P | Q) then (x)(P | A) ≈lo (x)(Q | A) for each A.
Proof. Let σ be a substitution and let σ 0 be defined as follows:
σ(x), x 6= adef
0
σ (x) =
x,
x=aThen (x)(P | ax)σ 0 ≈lo (x)(Q | ax)σ 0 . Hence (x)(P σ 0 | ax) ≈lo (x)(Qσ 0 | ax). Thus (x)(P σ | ax) ≈lo(x)(Qσ | ax). Assume that A is a process. Let b, z be fresh names. According to Lemma 23 one has(x)(P σ | ax) | a(x).bz.Aσ ≈lo (x)(Qσ | ax) | a(x).bz.Aσ
Observe that(x)(P σ | ax) | a(x).bz.Aστ−→ (x)((P σ | 0) | bz.Aσ)bz−→ (x)((P σ | 0) | Aσ)
In order to match these actions there must be some Q0 such thatbz(x)(Qσ | ax) | a(x).bz.Aσ =⇒ (x)((Q0 | 0) | A0 ) ≈lo (x)((P σ | 0) | Aσ)
which can obviously be rearranged as(x)(Qσ | ax) | a(x).bz.Aστ−→ (x)((Qσ | 0) | bz.Aσ)bz−→ (x)((Qσ | 0) | Aσ)=⇒ (x)((Q0 | 0) | A0 )Similarly some P 0 , A00 exist such that(x)((P σ | 0) | Aσ) =⇒ (x)((P 0 | 0) | A00 ) ≈lo (x)((Qσ | 0) | Aσ)
It follows easily that(x)(P | A)σ =⇒ (x)(P 0 | A00 ) ≈lo (x)(Q | A)σ(x)(Q | A)σ =⇒ (x)(Q0 | A0 ) ≈lo (x)(P | A)σ
Using this property it is easy to see that {((x)(P | A)σ, (x)(Q | A)σ)}∪ ≈lo is a local open bisimulation.
13

In view of Lemma 24, it is tempting to ‘simplify’ Definition 22 in the following manner:
A symmetric relation R on π-processes is an l-bisimulation if whenever P RQ then the following properties hold:λλ(i) If P −→ P 0 then some Q0 exists such that Q =⇒ Q0 and P 0 RQ0 ;
a(x)

a(x)

(ii) If P −→ P 0 then, for each fresh name b, some Q0 exists such that Q =⇒ Q0 and(x)(P 0 | bx)R(x)(Q0 | bx).
The l-bisimilarity ≈0l is the largest l-bisimulation.
It turns out that the relation ≈0l is not a good one. It identifies for example (x)(ax | bx) and (x)ax | (x)bx
and is therefore not closed under composition. It is clear that, from an observational point of view,
the process a(v).b(w).(v(z).z(u) | wc), where c is fresh, is able to detect the difference between the twoprocesses.
Another implication of Lemma 24 is that if we replace the fourth requirement of Definition 22 by thefollowing stronger requirement (iv’), then we would obtain the same local bisimilarity.
a(x)

a(x)

(iv’) If P −→ P 0 then some Q0 exists such that Q =⇒ Q0 and (x)(P 0 | A)R(x)(Q0 | A) for every
process A.
a(x)The reason could be given as follows: Suppose P ≈lo Q and P −→ P 0 . For a fresh name b, therea(x)must be some Q0 such that Q =⇒ Q0 and (x)(P 0 | bx) ≈lo (x)(Q0 | bx). Now Lemma 24 implies that(x)(P 0 | A) ≈lo (x)(Q0 | A) actually holds for every process A. So ≈lo is a relation that satisfies (iv’). On
the other hand the reverse inclusion is obvious by definition.
Now we show that the local open bisimilarity is another characterization of the quasi open bisimilarity.
Theorem 25. The relations ≈lo and ≈q coincide.
a(x)

a(x)

Proof. Suppose P ≈q Q and P −→ P1 . Then Q1 exists such that Q =⇒ Q1 and P1 ≈xq Q1 . By Lemma 8,(x)(P1 | A) ≈q (x)(Q1 | A)
holds for every A. This should be enough to convince the reader that ≈q is a local open bisimulation.
Now let Rx1 ...xn be(x1 . . . xn )(P | a1 x1 | . . . | an xn ) ≈lo (x1 . . . xn )(Q | a1 x1 | . . . | an xn )(P, Q)
for some a1 , . . . , an 6∈ f n(P | Q)
Suppose σ respects x1 . . . xn . Notice that (ex)(P | a1 x1 | . . . | an xn )σ ≡ (ex)(P σ | a1 x1 | . . . | an xn ). Threecases need be considered:λ• P σ −→ P 0 where λ is a τ , or an input action, or a free output action and n(λ) ∩ x
e = ∅. Thenλ(ex)(P σ | a1 x1 | . . . | an xn ) −→ (ex)(P 0 | a1 x1 | . . . | an xn )It follows that Q0 exists such that
λ(ex)(Qσ | a1 x1 | . . . | an xn ) =⇒ (ex)(Q0 | a1 x1 | . . . | an xn )≈lo (ex)(P 0 | a1 x1 | . . . | an xn )λThen Qσ =⇒ Q0 Rx1 ...xn P 0 .
axi• P σ −→
P 0 where i ∈ {1, . . . , n}. Thena(xi )(ex)(P σ | a1 x1 | . . . | an xn ) −→ (xe0 )(P 0 | a1 x1 | . . . | an xn )where xe0 is obtained from x
e by removing xi . It follows that Q0 exists such thata(xi )(ex)(Qσ | a1 x1 | . . . | an xn ) =⇒ (xe0 )(Q0 | a1 x1 | . . . | an xn )and(ex)(P 0 | a1 x1 | . . . | an xn ) ≈lo (ex)(Q0 | a1 x1 | . . . | an xn )a(xi )

Then Qσ =⇒ Q0 Rx1 ...xn P 0 .
14

c(x)

• P σ −→ P 0 . Thenc(x)x)(P1 | a1 x1 | . . . | an xn )(ex)(P | a1 x1 | . . . | an xn ) −→ (e(6)

0

By definition some Q exists such thatc(x)(ex)(Qσ | a1 x1 | . . . | an xn ) =⇒ (ex)(Q0 | a1 x1 | . . . | an xn )and for fresh ax)(P 0 | a1 x1 | . . . | an xn ) | ax)(x)((ex)(Q0 | a1 x1 | . . . | an xn ) | ax) ≈lo (x)((eConsequently(x)(ex)(Q0 | a1 x1 | . . . | an xn | ax) ≈lo (x)(ex)(P 0 | a1 x1 | . . . | an xn | ax)c(x)It follows that Qσ =⇒ Q0 Rx1 ...xn x P 0 . Notice that (6) can not be matched up byc(x)(ex)(Qσ | a1 x1 | . . . | an xn ) =⇒ (xe0 )(Q0 | a1 x1 | . . . | an xn )cx

induced by a free output action Qσ =⇒ Q0 .
So R is a quasi open bisimulation.

7

Complete System

An algebraic investigation of an equivalence relation would be incomplete without discussing the axiomatization aspect of the corresponding congruence. Given an observational equivalence ≈ one of the mostinteresting questions to ask is if there exists an equational axiomatic system that is both sound andcomplete for ≈. In general one should not expect that a complete system works for all processes due tothe limitation of Turing computability. The restrictions to the finite processes ([9]) or the finite control
processes ([7, 8, 5, 6]) are imposed in order to obtain a completeness result.
In this section we take a look at the equational axioms for the quasi open congruence. The main
result is a complete system for the congruence. This system differs from the system for the weak open
congruence [2] in that it has an additional law S6. The line of our investigation follows closely the one
advocated in [2]. We refer the reader to [2] for a detailed discussion on the axiomatization problems ofthe π-calculus. We begin with some comments on some of the laws for the π-calculus:• Milner, Parrow and Walker proposed, among others, two well known types of equivalences for the
π-processes, the early equivalence and the late equivalence. The difference between the two can beseen from the following fact: a(x).P +a(x) is early equivalent to a(x).P +a(x)+a(x).[x=y]P ; but
the two are not late equivalent. This is because in the late semantics the actiona(x)a(x).P +a(x)+a(x).[x=y]P −→ [x=y]P
can not be simulated by any action from a(x).P +a(x).Q. In the presence of the mismatch operator
this pair can be generalized toa(x).P +a(x).Q
anda(x).P +a(x).Q+a(x).([x=y]P +[x6=y]Q)
They are early equivalent but not late equivalent. For the weak open bisimilarities, there is also a
difference between the early and the late approaches. This early/late dichotomy does not appear
in the π-calculus without the mismatch operator. But it does appear in the π-calculus with themismatch operator, as pointed out by the present author and Yang in [2]. A pair that are early
open bisimilar but not late open bisimilar are the following π-processes:a(x).[x=y]τ.P + a(x).[x6=y]τ.P

15

and
a(x).[x=y]τ.P + a(x).[x6=y]τ.P + a(x).Pa(x)

This is because in the early framework the action a(x).[x=y]τ.P +a(x).[x6=y]τ.P +a(x).P −→ P canbe simulated either by the summand a(x).[x=y]τ.P or by the summand a(x).[x6=y]τ.P , dependingon whether x is y or not. Notice the important role played by the tau prefix. The quasi open
bisimilarity of this paper is the early version.
• A combinator that causes a major concern is the localization operator. Take for instance the πprocess a(x).(P +[x=y]Q). Intuitively this process is equivalent to a(x).P since y will never beidentified to x. From an algebraic point of view, one needs equational law(s) that could support
the inference of such equalities. It is difficult to conceive that there are simple structural laws to
fulfill this. For instance the localization operator (x) in (x)ax.C[[x=y]P ] could not be pushed inside
the output prefix ax but the match operator [x=y] could be very deep inside the context C[ ]. So
obviously the following axiom(x)[x=y]P = 0(7)where x 6= y, is far from sufficient. What we have come up with is the following schematic law:(x)C[[x=y]P ] = (x)C[0](8)where neither x nor y is bound in C[] and x 6= y. In the full π-calculus this law is equivalent to thefollowing law(x)C[[x6=y]P ] = (x)C[P ](9)under the same condition, the proof of which can be found in [2].
• Since the quasi open bisimilarity is looser than the open bisimilarity, there must be equalities thatare valid for the former but are invalid for the latter. We are looking for a law or laws that could
characterize the difference between the two equivalences. For this purpose we propose the following
axiom:(y)C[a(x).P ] = (y)C[a(x).([x=y]P +[x6=y]P y )](10)
where P is composition free. Here the most important thing to notice is that y is local. When it is
the time for the input prefix a(x) to act, it may receive a name z. After the action the subprocessa(x).P becomes P {z/x} and the subprocess a(x).([x=y]P +[x6=y]P y ) becomes[z=y]P {z/x} + [z6=y]P y {z/x}(11)There are two cases:– z = y. Then (11) is actually [y=y]P {y/x} + [y6=y]P y {y/x}, which is equivalent to P {z/x}.
– z 6= y. In this case (11) is equivalent to P y {z/x} using (8) and (9). Here we have used in an
essential way that y is local. But if y is local then P y is operationally the same as P .
So (10) is sound for the quasi open bisimilarity.
• In process algebra Miler’s three tau laws are well known for their role in characterizing the observational aspect of the equivalences. Without paying any attention to the match/mismatch operators,
these laws are as follows:
π.τ.P = π.P
P +τ.P = τ.Pπ.(P +τ.Q) = π.(P +τ.Q) + π.Q

(12)
(13)
(14)

In the presence of the mismatch operator the law (14) should be generalized toπ.(P +ψτ.Q)= π.(P +ψτ.Q) + ψπ.Q

(15)

Now (14) and (15) are equivalent in the equational systems that admit the following two laws:[x=y]π.P[x6=y]π.P= [x=y]π.[x=y]P= [x6=y]π.[x6=y]P
16

(16)
(17)

For the early and the late equivalences both (16) and (17) are valid. But for the open bisimilarities(17) is not admissible. Another complication that the open bisimilarities add to the algebraic theoryis that Milner’s three tau laws are not sufficient to obtain a completeness result. It is discovered by
Fu in [2] that the following tau law is crucial:
τ.P = τ.(P +[x=y]τ.P )For the π-calculus with the mismatch operator, the above law should be generalized toτ.P = τ.(P +ψτ.P )(18)

For the early and the late equivalences the above tau laws are derivable. In the open semantics
it has been shown indispensable in some special case [2]. In more complicated languages, theestablishment of such a negative result has not been achieved. The most complex tau law used inthis paper is the following one, where I is a finite indexing set and x 6∈ n(ψ)XX
a(x).(Pi + ψi τ.Q) =a(x).(Pi + ψi τ.Q) + ψa(x).Q
(19)
i∈I

i∈I

The above axiom holds under the condition:_

ψi ⇔ ψ

i∈I

The point is that ψi might contain the bound name x W
but ψ does not. The intuition behind (19)is this: Suppose the substitution σ validatesψ.
Theni∈I ψi σ ⇔ >. If ψσaσ(x).Qσ receives theWname y through communication, then i∈I ψi σ{y/x} ⇔ > and therefore there must be some i ∈ Isuch that ψi σ{y/x} ⇔ >. So the summand (a(x).(Pi + ψi τ.Q))σ can put into action.
We are now in a position to present the equational system. The basic laws for the quasi open
congruence are summarized in Figure 1. These laws are valid for the strong open congruence. We willrefer to this set of laws as AS. Apart from L8 and S6, the laws of AS have appeared in [12]. Some
derived laws of AS are stated in Figure 2. The proofs that they are derivable can be found in [10, 13, 2].
Figure 3 lists all the tau laws used in this paper.
For the π-calculus with the mismatch the normal forms defined in the standard manner are not quite
useful in the algebraic investigation. One needs the complete normal forms defined below.
Definition 26. Let V be a finite set of names. A condition ψ is complete on V if for any condition φsuch that n(φ) ⊆ V either ψφ ⇔ ψ or ψφ ⇔ ⊥.
A complete condition on V is a maximal condition on V that can not be extended or strengthenedby any condition on V .
Definition 27. Let V be a finite set of names. A process P is a complete normal form on V if it is of
the formXψi λi .Pii∈I

such that for each i ∈ I the following conditions are met:
• bn(λi ) ∩ V = ∅;• ψi is complete on V ;• and Pi is a complete normal form on V ∪ bn(λi ).
The standard property required for normal forms, irrespective of their definitions, is that every finite(or finite control) process is convertible to a normal form process. This is established by the next lemma,
whose proof is routine using structural induction.
Lemma 28. For every process P there is a complete normal form P 0 such that AS ` P = P 0 .
The next lemma describes a useful equational property about the operation ( )ze.
17

E1
E2
E3
C1
C2
C3
C4
C5
L1
L2
L3
L4
L5
L6
L7
L8
M1
M2
M3
M4
M5
S1
S2
S3
S4
S5
S6

P
Q
P
π.P
[x=y]P[x6=y]P
P +R
(x)P
(x)0
(x)(y)P(x)(P +Q)(x)π.P(x)π.P(x)[y=z]P(x)[x=y]P(x)C[[x=y]P ]φP[x=y]P[x=y](P +Q)[x6=y](P +Q)[x6=x]P
P +0
P +Q
P +(Q+R)[x=y]P +P[x=y]P +[x6=y]P(y)C[a(x).P ]

=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=
=

P
P
R
π.Q
[x=y]Q[x6=y]Q
Q+R(x)Q
0(y)(x)P(x)P +(x)Q
π.(x)P0[y=z](x)P0(x)C[0]ψP[x=y]P {y/x}[x=y]P +[x=y]Q[x6=y]P +[x6=y]Q
0P
Q+P(P +Q)+RPP(y)C[a(x).([x=y]P +[x6=y]P y )]if P = Q
if P = Q = R
if P = Q
if P = Q
if P = Q
if P = Q
if P = Q

if x 6∈ n(π)
if x ∈ subj(π)
if x 6∈ {y, z}
if x 6= yx, y 6∈ bn(C[]) and x6=yif φ ⇔ ψy 6∈ bn(C[])

Figure 1: AS: Basic Rules and Axioms for the Full Pi Calculus
Lemma 29. Suppose that none of the free names appearing in the match/mismatch operations of P isbound by an input prefix in C[]. Then AS ` (z)C[P z ] = (z)C[P ].
Proof. The proof is carried out by an induction on P . We take a look at the major cases:• P is of the form [x=y]P1 . There are three subcases:
I.H.

– z 6∈ {x, y}. Then (z)C[P z ] = (z)C[[x=y]P1z ] = (z)C[[x=y]P1 ] = (z)C[P ] where “I.H.” means“induction hypothesis”.
I.H.

– x = z = y. Then (z)C[P z ] = (z)C[P1z ] = (z)C[P1 ] = (z)C[P ].
L8– z ∈ {x, y} and x 6= y. Then (z)C[P z ] = (z)C[0] = (z)C[P ].
• P is of the form [x6=y]P1 . The situation is similar, using D8.
• P is of the form a(x).P1 . Then(z)C[P z ]=(z)C[a(x).([x=z](P1 {z/x})z + [x6=z]P1z )]I.H.

(z)C[a(x).([x=z]P1 {z/x} + [x6=z]P1z )](z)C[a(x).([x=z]P1 + [x6=z]P1z )]

=
=

S6

=
=

(z)C[a(x).P1 ](z)C[P ]This completes the proof.

18

D1
D2
D3
D4
D5
D6
D7
D8

ψP +P
[x=x]P[x=y]0[x6=y]0(x)[y6=z]P(x)[x6=y]P(x)P(x)C[[x6=y]P ]

=
=
=
=
=
=
=
=

P
P
0
0
[y6=z](x)P(x)PP(x)C[P ]if x 6∈ {y, z}
if x 6= y
if x 6∈ f n(P )x, y 6∈ bn(C[]) and x6=yFigure 2: Some Laws Derivable from AS
T1
T2
T3
T4
T5

π.τ.P
P + τ.P
π.(P + ψτ.Q)
τ.P
P
a(x).(P
+
ψ
τ.Q)
i
i
i∈I

=
=
=
=
=

π.P
τ.P
π.(P + ψτ.Q) + ψπ.Q
τ.(PP + ψτ.P )i∈I a(x).(Pi + ψi τ.Q) + ψa(x).Q

bn(π) ∩ n(ψ) = ∅Wi∈I ψi ⇔ ψ,

x 6∈ n(ψ)

Figure 3: Tau Laws
In the rest of this paper, we will let ASq be the set AS ∪ {T 1, T 2, T 3, T 4, T 5}. The purpose of
the remaining section is to prove that ASq is a complete system for the quasi open congruence. The
congruence is defined in the standard manner ([10, 13]):
Definition 30. P and Q are quasi open congruent, notation P 'lq Q, if P ≈q Q and the following
properties hold:ττ(i) If P −→ P 0 then Q =⇒ Q0 ≈q P 0 for some Q0 ;ττ(ii) If Q −→ Q0 then P =⇒ P 0 ≈q Q0 for some P 0 .

7.1

Saturation

Saturation properties say that additional internal actions (tau actions) can be ironed out by equational
rewriting. In CCS this property takes the following form:λIf P =⇒ P 0 then P +λ.P 0 and P are provably equal (in some equational system).
λλIntuitively the property suggests that one can think of P =⇒ P 0 as a single step action P −→ P 0 fromthe viewpoint of an equational theory that is rich enough. When one has established this property for an
equational system, one is half way through in proving a completeness result. For the π-calculus without
the match operator the property is termed as follows:λ

If σ is a substitution induced by ψ and P σ =⇒ P 0 then P +ψλ.P 0 and P are provably equal(in some equational system).
In the presence of the mismatch operator it should be refined to the following:λIf σ is a substitution induced by ψ, ψ is complete on n(P ) and P σ =⇒ P 0 then P +ψλ.P 0 and
P are provably equal (in some equational system).
def

The completeness requirement can not be left out. Take for instance A = aa.(bb+[x6=y]τ.cc). ObviouslyaaccA =⇒ cc. But A+cc can not be equal to A since (A+cc){y/x} −→ 0 can not be matched up by any
action of A.
The next lemma establishes some basic saturation properties that are independent of any particularobservational equality, meaning that they hold of all the observational equalities we are aware of.
Lemma 31 (saturation 1). Suppose Q is a complete normal form on some V ⊇ f n(Q), ψ is completeon V , and σ is a substitution that is induced by ψ. Then the following properties hold:τ(i) If Qσ =⇒ Q0 then ASq ` Q = Q + ψτ.Q0 .
19ax(ii) If Qσ =⇒ Q0 then ASq ` Q = Q + ψax.Q0 .
a(x)(iii) If Qσ =⇒ Q0 then ASq ` Q = Q + ψa(x).Q0 .
ax(iv) If Qσ =⇒−→ Q0 , for x 6∈ f n(Qσ), then ASq ` Q = Q + ψa(x).Q0 .
Proof. The proofs are routine inductions on the lengths of the action sequences. We sketch a proof ofa(x)τ(iii). Suppose Qσ =⇒−→ Q00 σ =⇒ Q0 . It is easy to show thatAS ∪ {T 1, T 2, T 3} ` Q = Q + ψa(x).Q00
It is clear that f n(Q00 ) ⊆ f n(Q) ∪ {x}, [x6∈V ]ψ is complete on V ∪ {x} ⊇ f n(Q00 ) and σ is induced by[x6∈V ]ψ. If Q00 σ ≡ Q0 we are done. Otherwise
AS ∪ {T 1, T 2, T 3} ` Q00 = Q00 + [x6∈V ]ψτ.Q0
ThereforeQ==

Q + ψa(x).Q00
Q + ψa(x).(Q00 + [x6∈V ]ψτ.Q0 )L8=

Q + ψa(x).(Q00 + ψτ.Q0 )T3=

Q + ψ(a(x).(Q00 + ψτ.Q0 ) + ψa(x).Q0 )M1

Q + ψa(x).(Q00 + ψτ.Q0 ) + ψa(x).Q0
Q + ψa(x).Q0==

We are done.
Notice that the (iv) of Lemma 31 can not be strengthened toax(iv’) If Qσ =⇒ Q0 , for x 6∈ f n(Qσ), then ASq ` Q = Q + ψa(x).Q0 .
This is because Q0 might contain x free and therefore in general the substitution σ is not induced by acondition ψ complete on V ∪ {x}. A careful analysis of the input actions leads to the following lemma.
Lemma 32 (saturation 2). Suppose Q is a complete normal form on some V = {y1 , . . . , yk } ⊇ f n(Q),ψ is complete on V , and σ is a substitution that is induced by ψ. Then the following saturation properties
hold: Ifax

Qσ=⇒ −→ Q0 σ for x 6∈ f n(Qσ),
Q0 σ{y1 /x} =⇒ Q1 ,Q0 σ{y2 /x} =⇒ Q2 ,..
.
Q0 σ{yk /x} =⇒ Qk ,Q0 σ =⇒ Qk+1
then ASq ` Q = Q + ψa(x).(τ.Q0 + ψPk

j=1 [x=yj ]τ.Qj + ψ[x6∈V ]τ.Qk+1 ).

Proof. By the assumption of the lemma and Lemma 31
Q = Q + ψa(x).Q0 σ = Q + ψa(x).τ.Q0 σ = Q + ψa(x).τ.Q0
τFor each j ∈ {1, . . . , k}, if Q0 σ{yj /x} =⇒ Qj thenτ.Q0 = τ.(Q0 + ψ[x=yj ]τ.Qj ) = τ.Q0 + ψ[x=yj ]τ.Qj
otherwise
τ.Q0 σ{yj /x} = τ.Qj = τ.Qj + ψ[x=yj ]τ.Qj
In the former case
Q = Q + ψa(x).τ.Q0 = Q + ψa(x).(τ.Q0 + ψ[x=yj ]τ.Qj )20

In the latter caseQ=

Q + ψa(x).τ.Q0 σ

D1=

Q + ψa(x).(τ.Q0 σ + [x=yj ]τ.Q0 σ)

M2

=
=
=

Q + ψa(x).(τ.Q0 σ + [x=yj ]τ.Q0 σ{yj /x})Q + ψa(x).(τ.Q0 σ + [x=yj ](τ.Qj + ψ[x=yj ]τ.Qj ))Q + ψa(x).(τ.Q0 σ + ψ[x=yj ]τ.Qj )M2

Q + ψa(x).(τ.Q0 + ψ[x=yj ]τ.Qj )=So in either case one has
Q = Q + ψa(x).(τ.Q0 + ψ[x=yj ]τ.Qj )It follows by induction that0

Q = Q + ψa(x).(τ.Q +kX

ψ[x=yj ]τ.Qj )j=1
τIf Q0 σ =⇒ Qk+1 thenQ0 = Q0 + ψ[x6∈V ]τ.Qk+1

otherwise
τ.Q0 σ = τ.Qk+1 = τ.Qk+1 + ψ[x6∈V ]τ.Qk+1 = τ.Q0 σ + ψ[x6∈V ]τ.Qk+1
Putting everything together, one gets the required result.
Intuitively the saturation property for an input action of Q must be based upon the knowledge ofwhat the process evolves into after receiving a name in f n(Q) and what it evolves into after receivinga name not in f n(Q). In other words, the saturation property must take into account all the possible
consequences the input action might incur.

7.2

Promotion

Promotion refers to the fact that a pair of observable processes can be lifted to a closely related pair of
proof theoretical equal processes. This fact is crucial to the proof of the completeness theorem.
Lemma 33 (promotion). If P ≈qo Q then ASq ` τ.P = τ.Q.
Proof. Suppose P ≈qo Q. By Lemma 28, we may assume that both P and Q are complete normalPP
def
forms on V = f n(P +Q)={y1 , . . . , yk }. Let them be i∈I φi λi .Pi and j∈J ψj λj .Qj respectively. Thenλ σ

(ai σ)xi
P σ −→Pi σ for a non input action and P σ −→ Pi σ for input action with fresh x. Let σ be a substitution
induced by φi .

aσ(x)• λi is a restricted output action a(x). Then Q0 exists such that Qσ =⇒ Q0 and (Pi σ)x ≈qo (Q0 )x . By
induction hypothesis one has ASq ` τ.(Pi σ)x = τ.(Q0 )x . By Lemma 29, one has a(x).P = a(x).P x .
Therefore by Lemma 31 one gets
ASq ` Q+φi a(x).Pi

=
=
=
=
=

Q+φi aσ(x).Pi σ
Q+φi aσ(x).τ.(Pi σ)xQ+φi aσ(x).τ.(Q0 )xQ+φi aσ(x).Q0
Q(ai σ)x• λi is an input action (ai σ)x. It follows from P ≈qo Q that Q0 exists such that Qσ =⇒ −→ Q0 σ
and the following conditions hold:– For each l ∈ {1, . . . , k}, Qil exists such that Q0 σ{yl /x} =⇒ Qil ≈qo Pi σ{yl /x}.
21

– Qik+1 exists such that Q0 σ =⇒ Qik+1 ≈qo Pi σ.
It follows by induction hypothesis that τ.Qil = τ.Pi σ{yl /x} for l ∈ {1, . . . , k} and τ.Qik+1 = τ.Pi σ.
Now by Lemma 32 one gets
ASq ` Q=Q + φi ai (x).(τ.Q0 +kX

φi [x=yl ]τ.Qil σ{yl /x}+φi [x6∈V ]τ.Qik+1 σ)

l=1=Q + φi ai (x).(τ.Q0 +kX

φi [x=yl ]τ.Pi σ{yl /x}+φi [x6∈V ]τ.Pi σ)

l=1=

Q + φi ai (x).(τ.Q0 +kX

φi [x=yl ]τ.Pi +φi [x6∈V ]τ.Pi )

l=1

=
T3

=

Q + φi ai (x).(τ.Q0 +φi τ.Pi )Q + φi ai (x).Pi

Wk
where the fourth equality holds because x6∈V ∨ ( l=1 x=yl ) is a tautology.
The other cases are simpler. The rest of the proof is standard. We refer the reader to [2] for details.

7.3

Completeness

Using the fact that P ≈qo Q iff τ.P 'qo τ.Q, one can rephrase the promotion lemma as follows:
If τ.P 'qo τ.Q then ASq ` τ.P = τ.Q.
This reiteration makes it obvious that promotion is a restricted form of completeness. As it turns out theproof of the promotion lemma can be modified slightly to a proof of the following completeness theorem.
The modification follows the following slogan:“Wherever we use the induction hypothesis in the proof of the promotion lemma, we use thepromotion lemma in the proof of the completeness theorem.”
The reader who is not quite familiar with the routine is referred to [2].
Theorem 34 (completeness). If P 'qo Q then ASq ` P = Q.

8

Conclusion

The bisimulation approach was first applied to the pure CCS ([9]) and later to the value-passing CCS([3, 4]). It is fair to say that the former is generalized, in the framework of the π-calculus, to the open
bisimulation whereas the latter is related to the early/late bisimulation equivalence. The value passing
calculi can be classified into two groups according to what can be communicated. For the calculi inthe first group, the contents of communications may contain anything but channel names. The value
passing CCS is one such calculus. For those in the second group the situation is the opposite. The πfamily belong to the second group. For the (first order) π-calculus, the contents of communications canbe nothing but channel names. Now for the value passing CCS the only way environments may affectprocesses is through exchanging data. Data may change the control flow of the computation but not
the communication topology. On the other hand environments have a much stronger impact in the πcalculus. A consequence of this stronger observation power is that bisimulations must be closed under
every bisimulation step. This also points out that the value passing view does not give rise to equivalencesthat take into account of the dynamic updating power of the environments. So the open bisimulations
have the edge. The only problem is that it assumes that an environment has something it really does nothave, that is the ability to modify local names. If we rectify this, we arrive at the authentic equivalence
for the π-calculus, the quasi open bisimilarity. In this paper we have achieved a better understanding of
the equivalence.

22References[1] Y. Fu, On Quasi Open Bisimulation, Theoretical Computer Science, 338 (2005) 96-126.
[2] Y. Fu and Z. Yang, Tau Laws for Pi Calculus, Theoretical Computer Science, 308 (2003) 55-130.
[3] M. Hennessy, H. Lin, Proof Systems for Message Passing Process Algebra, CONCUR ’93, Lecture
Notes in Computer Science 715 (Springer-Verlag, 1993) 202-216.
[4] M. Hennessy, H. Lin, Symbolic Bisimulations, Theoretical Computer Science, 138 (1995) 137-161.
[5] H. Lin, Unique Fixpoint Induction for Mobile Processes, CONCUR ’95, Lecture Notes in Computer
Science 962 (Springer-Verlag, 1995) 88-102.
[6] H. Lin, Complete Proof Systems for Observation Congruences in Finite-Control π-Calculus,
ICALP ’98, Lecture Notes in Computer Science 1443 (Springer-Verlag, 1998) 443-454.
[7] R. Milner, A Complete Inference System for a Class of Regular Behaviours, Journal of Computerand System Science, 28 (1984) 439-466.
[8] R. Milner, A Complete Axiomatization System for Observational Congruence of Finite State Behaviours, Information and Computation, 81 (1989) 227-247.
[9] R. Milner, Communication and Concurrency (Prentice Hall, 1989).
[10] R. Milner, J. Parrow and D. Walker, A Calculus of Mobile Processes, Information and Computation,
100 (1992) 1-40 (Part I), 41-77 (Part II).
[11] R. Milner and D. Sangiorgi, Barbed Bisimulation, ICALP ’92, Lecture Notes in Computer Science
623 (Springer-Verlag, 1992) 685-695.
[12] J. Parrow and D. Sangiorgi, Algebraic Theories for Name-Passing Calculi, Information and Computation, 120 (1995) 174-197.
[13] D. Sangiorgi, A Theory of Bisimulation for π-Calculus, Acta Informatica, 3 (1996) 69-97.
[14] D. Sangiorgi and D. Walker, On Barbed Equivalence in π-Calculus, CONCUR ’01, 2001.
[15] D. Sangiorgi and D. Walker, The Pi Calculus–A Theory of Mobile Processes, CUP, 2001.

23