Tau Laws for Pi Calculus
Yuxi Fu ∗Zhenrong Yang

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

Abstract
The paper investigates the non-symbolic algebraic semantics of the weak bisimulation congruences
on finite pi processes. The weak bisimulation congruences are studied both in the absence and in
the presence of the mismatch operator. Some interesting phenomena about the open congruences are
revealed. Several new tau laws are discovered and their relationship is discussed. The contributionsof the paper are mainly as follows:
1. It is proved that Milner’s three tau laws fail to lift a complete system for the strong open
congruence to a complete system for the weak open congruence in the absence of both themismatch operator and the restriction operator. A fourth tau law is proposed to deal with thematch operator under the prefix operation. It is shown that for this calculus a complete system
for the strong open congruence extended with all the four tau laws is complete for the weak
open congruence.
2. It is verified that the four tau laws are also enough for the weak open congruence of the pi calculus
without the mismatch operator. Two complete systems are given, one using distinctions andthe other using a schematic law for the restriction operator.
3. It is pointed out that the standard definition of the weak open congruence gives rise to a bad
equivalence relation in the presence of the mismatch operator. Two alternatives are proposed.
These are the late open congruence and the early open congruence. Their difference is similar
to that between the weak late congruence and the weak early congruence. Complete axiomatic
systems for the two weak open congruences are given.

Key Words: Process Algebra, Mobile Process, Bisimulation, Axiomatization∗ The author is supported by the NNSFC (69873032), the 863 Hi-Tech Project (863-306-ZT06-02-2), the Young Scientist

Research Fund and the University Scholar Funding Scheme. He is also supported by BASICS, Center of Basic Studies in
Computing Science, sponsored by Shanghai Education Commission. BASICS is affiliated to the Department of Computer
Science of Shanghai Jiaotong University.

Contents
1 State of Art

3

2 The Calculus of Nondeterministic Mobile Processes
2.1 Open Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 Equational System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.3 The Insufficiency of Milner’s Tau Laws for Open Semantics . . . . . . . . . . . . . . . . .
2.4 The Failure of Hennessy Lemma for Mobile Processes . . . . . . . . . . . . . . . . . . . .
2.5 The Fourth Tau Law . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.6 Saturation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.7 Promotion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.8 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.9 Remark . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7
8
10
12
13
14
15
15
16
17

3 The Pi Calculus without Mismatch
3.1 Parallel Composition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2 Restriction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.3 System Using Distinction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.4 A Schematic Law for Restriction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

17
17
18
19
21

4 The Full Pi Calculus
4.1 Bisimulation Theory of the Full Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.1 Late and Early Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.2 Strong Open Bisimilarity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.3 Weak Open Bisimilarities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.4 Weak Open Bisimilarities are Equivalence Relations . . . . . . . . . . . . . . . . .
4.1.5 Weak Congruence Revisited . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Laws of the Full Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.1 Basic Laws . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.2 Additional Laws . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.3 Tau Laws . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Completeness Results for the Full Calculus . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3.1 Saturation Property . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3.2 Promotion Lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3.3 Completeness Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4 An Alternative to the Law S6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

21
22
23
24
25
27
28
29
29
31
32
35
35
38
38
39

5 Comment and Related Issue

42

A Proofs
A.1 The Proof of Lemma 55
A.2 The Proof of Lemma 62
A.3 The Proof of Lemma 69
A.4 The Proof of Lemma 70
A.5 The Proof of Lemma 73
A.6 The Proof of Lemma 77
A.7 The Proof of Lemma 79
A.8 The Proof of Lemma 80
A.9 The Proof of Lemma 81

47
47
47
49
49
50
51
51
53
53

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

1

State of Art

For more than ten years various calculi of mobile processes, notably the π-calculus ([32]), have been
the focus of research in concurrency theory. These calculi are distinguished from the process calculi like
CCS ([21, 31]) in that they are capable of dealing with processes whose communication structures canchange during their evolution. This ability of dynamic creation of communication link lies at the heartof mobility. In the calculi of mobile processes mobility is achieved by passing a channel name from one
process to another. The process that receives the channel name may communicate to a third process
through that received channel name. As it turns out the name-passing communication mechanism is apotent one. This can be seen from the following facts: Firstly name-passing calculi are able to simulate
process-passing calculi in a non-distributed framework ([44, 40, 45, 46]). The idea is simply that, insteadof sending a process to another, the sender may pass to the other a name through which one can accessto the process. Secondly many variants of the π-calculus, the asynchronous π-calculus ([6, 22, 23, 24, 2]),the πI-calculus ([41, 5]), the local π-calculus ([34]) have all been shown to be able to simulate each otherto a more or less degree. Even the χ-calculus ([9, 10, 13]) and Fusion Calculus ([39]), which departs
from the π-calculus more than any of the above variants, does not seem to add any additional expressive
power to the name-passing communication mechanism. One gets the feeling that all name-manipulating
mechanisms are more or less equivalent in terms of expressive power.
Apart from the variants of the π-calculus many other process calculi for mobility have been proposedin literature. One recent example is the Calculus of Mobile Ambients ([7]). While it is important to give
formal frameworks to capture the rich concept of modern computation, it is equally important, if not
more important, to achieve a deep understanding of these frameworks from a mathematical perspective.
It is in the latter aspect that sustained efforts are called for. Most people would agree that the theoryof π-calculus should be far richer than that of λ-calculus. Yet we know a lot more about the λ-calculus
than about the π-calculus.
The name-passing mechanism introduces significant difference between the algebraic theory of calculi
of mobile processes and that of CCS ([31]). The difference is mainly caused by three operators:
1. The first is the restriction operator. In CCS this operator is simple. In π-calculus however it comeswith complications. Operationally there must be labeled transition rules to take care of namemigration. Algebraically distinctions are introduced to define open bisimulations. The restriction
operator allows one to abstract away from internal communications. It localizes, so to speak,possible actions so that they do not have global impact. This is a fundamental operator since thetheory of process calculus is largely observational.
2. The second is the match operator. This operator is useful at least in two aspects: First it has a very
natural motivation from a programming point of view and is necessary in modelling programming
phenomena. Second it makes possible an expansion law for π-calculus. One aspect of the match
operator is to keep track of the mobility in a nondeterministic fashion. Subsequent research has
shown that the match operator plays a crucial role in the axiomatic theory of the π-calculus.
3. The third is the mismatch operator. Compared to the restriction and the match operators, thisoperator is more debatable. The argument is not to do with its practical motivation for in reality
one really needs this operator in a variety of situations where one uses calculi of mobile processes([38, 39, 1]). It is about if one should introduce such an operator into a basic model for concurrent
computation at all. The mismatch operator complicates the algebraic theory because it renders thedefinitions of observational equivalences more involved. On the other hand it also simplifies thealgebraic theory in the sense that it allows to accomplish what otherwise can only be achieved byintroducing more gadgets, like distinction, in the meta theory. The main reason to introduce theoperator is to make easy the axiomatization of the early and late equivalences. On the other hand,as we shall see later, the open semantics is definitely made more difficult by it.
The match and the mismatch operators help to internalize a lot of meta theory. For instance a condition,
which consists of a set of equality and inequality assumptions, and a distinction, which declares a setof names to be pairwise distinct, are two meta theoretic gadgets often used in the investigation of thealgebraic theory of mobile processes. Neither a condition nor a distinction is part of the syntax of the
π-calculus. They are extralogical entities. In a lot of cases one can do without them by working withthe match and the mismatch operators. Now these operators are entities of the π-calculus. It is in this3

6=strongweak

early congruence
Boreale, De Nicola
Linlate congruence
Boreale, De NicolaLin

open congruenceLi?

Figure 1: Symbolic Axiomatization with Mismatch=
strongweak

early congruence
Lin
Lin

late congruence
Lin
Lin

open congruence
Li
Li

Figure 2: Symbolic Axiomatization without Mismatch
way these two operators raise the expressive power of the π-calculus. Our personal opinion is that noneof the three operators has been studied in depth. This is sad because, to our understanding, the theoryof the π-calculus is largely a theory about these three operators.
The name-passing mechanism renders bisimulation equivalences more interesting. The idea of bisimulation is the most influential one in process algebra. It has been widely used in mathematical logics andgame theory. The introduction of bisimulation to concurrency theory is due to the work of Park ([35]) and
Milner ([31]). Equality relations based on bisimulation are usually finer than any observational equivalence one finds useful in practice. The virtue of them is that they are subject to algebraic investigation
in a more or less standard manner and that it is usually easy to establish the equality of two processes
by presenting a bisimulation relation. For π-calculus people have introduced early and late bisimulationequivalences ([32]), barbed equivalences ([33]) and open congruences ([42]), to name a few. It has to besaid however that although a lot of attention has been paid to these equivalences our knowledge about
them are still preliminary.
The difficulty of bisimulation equivalences is often to do with the weak versions of these relations.
A weak bisimulation equivalence ignores internal (tau) actions, which are deemed unobservable. Twoprocesses are equivalent if they can simulate each other’s observable actions. A tau law is an equalitythat manipulates unobservable internal actions. The three well known tau laws people usually refer towere proposed by Milner ([31]). They are the following axioms:
α.τ.P = α.P
P + τ.P = τ.Pα.(P +τ.Q) = α.(P +τ.Q) + α.Q
where α is a prefix capable of inducing an α-action whereas τ is a prefix that codes up an internal action.
The tau laws have been widely used in the theory of process algebra.
There are two main approaches to the semantics of mobile processes:• One is the symbolic approach ([20, 4]). This approach has been used to study the observational
equivalences of π-calculus. In [26] Lin has constructed complete systems for the strong early equivalence, the strong late equivalence, the weak early congruence and the weak late congruence. The
symbolic approach applies to π-calculus both with and without the mismatch operator. Prior to
Lin’s work, Boreale and De Nicola has studied the strong early equivalence and the strong lateequivalence in the symbolic framework. In [25] Li has worked out the complete systems for thestrong open bisimilarity and the weak open congruence of the π-calculus without the mismatch
operator and for the strong open bisimilarity of the π-calculus with the mismatch operator. The
situation is summarized in Figure 1 and Figure 2. The picture is almost complete, except for thecase of weak open congruence in the presence of the mismatch operator.
• The other is the non-symbolic approach that has been the major choice in semantic investigation.
When it comes to axiomatic investigation of π-calculus, the non-symbolic approach presents a lessclear picture. Here are the status quos of some related issues:– In the first published paper ([32]) on π-calculus Milner, Parrow and Walker defined four bisimulation congruences. They are early equivalence, late equivalence, weak early congruence and46=strongweak

early congruence
Parrow, Sangiorgi
Parrowlate congruence
Parrow, Sangiorgi
Parrow

open congruence?
?

Figure 3: Non-Symbolic Axiomatization with Mismatch=
strongweak

early congruence?
?

late congruence?
?

open congruence
Sangiorgi?

Figure 4: Non-Symbolic Axiomatization without Mismatch
weak late congruence. No complete system was given for any of the four congruences. In [37]Parrow and Sangiorgi improved the situation by giving complete systems for both the early
equivalence and the late equivalence. The π-calculus used in [37] has the mismatch operator.
Only recently Parrow has provided a proof that adding Milner’s three tau laws to the complete
system of the strong early, respectively late, equivalence is enough to get a complete system
for the weak early, respectively late, congruence ([36]). The approach Parrow has used is totranslate Lin’s symbolic system to a non-symbolic system in a uniform manner.
– We know even less about axiomatization for the π-calculus without the mismatch operator. In
this case the definitions of the early equivalence, the late equivalence, the weak early congruenceand the weak late congruence remain the same. But no axiomatic system for any of the four
has been discovered. The same problem is also open for testing congruence ([8, 3]).
– From a slightly different motivation Sangiorgi proposed open bisimilarities ([42]). His investigation focused on the strong open bisimilarity for the π-calculus without the mismatch
operator. A complete system for the congruence was presented using distinction indexed laws.
The theory of the weak open congruence was left undiscussed. In particular one does not haveany clue about the tau laws for the weak open congruence except the fact that Milner’s threetau laws are valid for it.
– The open semantics for the π-calculus with the mismatch operator is virtually unknown. For
one thing nobody even knows how to define weak open bisimilarity in this case. If one uses themismatch operator in the study of the late and the early congruences, s/he has little reason
to reject the operator in the open semantics.
We summarize the status quo of non-symbolic axiomatization in Figure 3 and Figure 4.
There are many more open problems, in the theory of π-calculus, than we have listed above. We give
below two of them that have been known for several years:• One fundamental question is about the very definition of bisimulation. If we restrict our attention to
the fragment of the π-calculus with none of the choice, match, mismatch and replication operators,
we could define a strong bisimulation equivalence for this fragment completely the same as we havedefined the strong bisimilarity for CCS processes. Our intuition tells us that this is a congruence
relation! But a proof of this conjecture has been so far beyond our reach. A proof of similar result
for the asynchronous π-calculus is available though ([2]).
• Another well-known unsettled problem is about the relationship between the weak barbed equivalence and the weak early equivalence. Sangiorgi has proved in his PhD thesis that thePtwo relations
coincide for the π-calculus with the mismatch operator and the big sigma operator , where the
big sigma operator refers to the choice operator that can be applied to an arbitrary number ofoperands. For the π-calculus with only the binary choice operator, the problem is still open. Although most people believe that the coincidence does hold for π-calculus with binary choice, andsome even stated the conjecture as a theorem, the fact remains that nobody has come up with aproof! All we know so far is that the coincidence holds for the image-finite processes and for the
asynchronous π-processes ([2]). By the way, the relationship of the barbed equivalence to other5equivalences in some calculi of mobile processes is much more subtle than most people would think.
In χ-calculus for example the barbed congruence is very different from the ‘standard bisimulation
congruence’. See [12, 14] for details.
In present the biggest problem with the theory of process calculus is that it lacks of proof techniques.
We know how to prove a relation to be some bisimulation using inductions on the complexity of thestructures of processes or on the height of derivations. But that seems to be all we know. Experimentswith mobile processes have told us that a finer-tuned analysis of the operational semantics, as well as
the algebraic semantics, of process calculus is called for. Attacking the open problems in process calculi
may well help us in this direction. Results and proof methodologies obtained in the study of one process
calculus are very likely to be useful to the study of another process calculus.
This paper does not claim to provide any novel techniques for solving problems in process calculus.
Its contribution is to solve some of the problems raised in the above, and therefore to provide someinsight into the weak observational equivalences and the tau laws for π-calculus. Some of the results are
surprising, others are interesting. Our contributions can be summarized as follows:• We formally prove that Milner’s three tau laws are sufficient to lift the complete systems for thestrong early equivalence and the strong late equivalence to complete systems for the corresponding
weak early congruence and weak late congruence. Our approach is different from Parrow’s andshows that the mismatch operator plays a crucial role in the resulting systems. This part of work
was carried out independently from Parrow’s.
• We show that Milner’s three tau laws are definitely not enough for the weak open congruence. We
propose a simple and powerful tau law
τ.P = τ.(P +[x=y]τ.P )that reveals more of the dynamic aspect of mobile processes than any of Milner’s tau laws. With
the help of this fourth tau law, we are able to construct a complete system for the weak open
congruence. This part of work should not be understood within the framework of open semantics.
The message it conveys has broader implication: For a calculus of mobile processes, one needs the
fourth tau law in general, although in some cases the law is derivable from other laws.
• We point out that the definition of the weak open bisimilarity for the π-calculus without themismatch operator can not be applied to the full π-calculus with the mismatch operator. We
propose two solutions. They give rise to early open bisimilarity and late open bisimilarity. So evenin the framework of open semantics there is an early/late dichotomy. The early open congruenceand the late open congruence are completely axiomatized using some new tau laws.
In this paper a lot of attention is paid to the tau laws. Some interesting relationship among the tau
laws used in this paper is revealed. Each of the tau laws is used in one of the complete systems studied
in this paper. There are altogether five complete systems for respective five weak congruences of the full
π-calculus. Three complete systems for strong congruences are also covered. Two of which are presented
for completeness. The other, the complete system for the strong open bisimilarity in the presence of themismatch operator, is the first of such system. The proofs of all the completeness results are structured
to bring out a general picture of the completeness proofs.
The main body of the paper is structured into three parts:
1. Section 2 studies the calculus of nondeterministic mobile processes ([42]). It is essentially the
π-calculus without the parallel composition, the restriction and the mismatch operators. Somegeneral preliminaries, like the open bisimilarity, equational system, Hennessy Lemma, saturation
lemma, promotion property, completeness theorem, are introduced in terms of this calculus. It is
pointed out that Milner’s three tau laws fall short of characterizing the weak open congruence as
far as the calculus of nondeterministic mobile processes is concerned. It is also pointed out thatthe well-known Hennessy Lemma fails for the calculus of nondeterministic mobile processes. This
fact is related to the failure of Milner’s tau laws. A fourth tau law is introduced. It is proved thatthe four tau axioms are enough to support a promotion lemma for the weak open congruence, fromwhich the completeness theorem follows easily.

6

2. Section 3 takes a look at the π-calculus without the mismatch operator. The impact of the restriction
operator on both the definitions of the open bisimilarities and the equational systems is discussed.
Two complete systems for the weak open congruence are established: One uses distinction indexed
equality laws. This is essentially Sangiorgi’s system ([42]) extended with the four tau laws. The
other uses a schematic law in favour of the indexed equality laws. In both systems the fourth tau
law plays a crucial role.
3. Section 4 focuses on the full π-calculus with the mismatch operator. This part consists of threesubparts:(a) Section 4.1 introduces equivalence relations for the full π-calculus. A construction central tolater definitions of open bisimilarities is defined. The definition of strong open bisimilarity isgiven by making use of the mismatch operator. It is shown that this equivalence coincides
with Sangiorgi’s open bisimilarity on the set of π-processes without the mismatch operator.
Three weak open bisimilarities for the full π-calculus are introduced. They are the same as
Sangiorgi’s weak open bisimilarity when restricted to the π-processes without the mismatch
operator. For completeness the definitions of strong/weak early and late equivalences are also
given.
(b) Section 4.2 investigates equalities for the full π-calculus and their inter-dependent relationship.
These equalities include those for the mismatch operator and various tau laws. Using theseequalities, eight axiomatic systems are defined for the eight congruence relations. Some ofthese systems are included for completeness.
(c) Section 4.3 establishes the completeness result for each of the eight systems, introduced in theprevious section, with respect to the corresponding congruence relation. The proofs of theseresults are given in a systematic manner.
The rest of the paper complements the main body in two aspects:
1. Section 5 makes a few comments and discusses some related issues.
2. Appendix A collects some proofs omitted in Section 4.
Section 2 is taken from an unpublished paper ([15]) by the first author. The technical results in
Section 3 are also due to him. The rest deal with bisimulation equivalences for the full π-calculus withthe mismatch operator, which is the joint work of both authors. A related piece of work is reported in
two extended abstracts ([18, 19]), also by the present authors, which discusses the χ-calculus with themismatch operator.

2

The Calculus of Nondeterministic Mobile Processes

The π-calculus of Milner, Parrow and Walker ([32]) is the most widely studied calculus of mobile processes.
Communications in π-calculus incur changes in topological structures of the participating processes,
causing the configuration of channel connections to evolve dynamically. This kind of mobility is supportedby the simple mechanism of confining the contents of communications to the set of channel names.
For the moment the full π-calculus is unnecessarily large. In this section we will be using a calculus ofnondeterministic mobile processes ([42]), obtained from π-calculus by omitting the composition operator
and the restriction operator.
Let N be a set of names, ranged over by lower case letters; and let N denote the set of conames{x | x ∈ N }. The union N ∪ N will be ranged over by α. The processes are defined by BNF as follows:
P := 0 | π.P | P +P | [x=y]P
where π ∈ {a(x), ax | a, x ∈ N } ∪ {τ }. Here 0 is the inactive process. A trailing 0 in prefix forms isoften omitted. The process a(x).P is in input prefix form. It must receive a name at a to instantiate x
throughout P before P can be activated. On the other hand ax.P is a process in output prefix form. Itemits x at a first and then evolves as P . The process τ.P can become P after performing an internal
communication. The process [x=y]P behaves like either P or 0, depending on whether x = y or not.
The constructor [x=y] is often referred to as a match operator. The choice operator ‘+’ is well-known.
7

The process P +Q acts either as P or as Q exclusively, with the choice being made nondeterministically.
The name x in a(x).P is bound. A name appearing in P is free if it is not bound. The notations bn(P ),f n(P ) and n(P ) denote respectively the set of bound names, the set of free names and the set of names
appeared in P .
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 (P + C 0 []) for some context C 0 [] and some process P , or [x=y]C 0 [] for somecontext C 0 [] and some names x and y.
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 , 1 ≤ i ≤ n, and is constant elsewhere. If
def

def

σ = [y1 /x1 , . . . , yn /xn ] then n(σ) = {x1 , . . . , xn , y1 , . . . , yn } and rng(σ) = {y1 , . . . , yn }.
The operational semantics is defined by the following labeled transition system:
Prefixππ.P −→ P
Matchπ

P −→ P 0π[x=x]P −→ P 0

Choiceππ

P −→ P 0π
P +Q −→ P 0

Q −→ Q0π
P +Q −→ Q0

In the above rules, π ranges over the set {a(x), ax | a, x ∈ N } ∪ {τ }. So we have confused the meta
notation for action labels and that for prefixes.
τππ
Let =⇒ be the reflexive and transitive closure of −→. We will write =⇒ for =⇒−→=⇒. We will alsoπbπ
write =⇒ for =⇒ if π 6= τ and for =⇒ otherwise.
We will need to deal with a sequence of match constructs concatenated one after another. It isconvenient to have a meta symbol for such a sequence. In the rest of this paper µ, µ0 , . . . denote finite
lists of match equalities. Suppose µ is x1 =y1 , . . . , xn =yn . Then µP denotes [x1 =y1 ] . . . [xn =yn ]P . If µ
logically implies µ0 , we write µ ⇒ µ0 ; and if both µ ⇒ µ0 and µ0 ⇒ µ we write µ ⇔ µ0 . If µ is an empty
list, it plays the role of logical truth, in which case µP is just P . Clearly a list µ of match equalities
defines an equivalence relation on the set N of names. We write σµ to denote an arbitrary substitutionthat sends all members of an equivalence class to a representative of that class.
We will use the widely adopted α-convention saying that a bound name in a process can be replaced
by a fresh name, a name that does not appear in the process, without changing the syntax of the process.
We will assume throughout this paper that different bound names appeared in a process expression area(x)distinct. When we write P σ −→ P 0 for instance, the reader should understand that we have applied thenecessary α-conversion so that x appears neither in σ nor in P as a free name. The same assumption
will be applied to the names introduced by the restriction operator studied later on.

2.1

Open Congruence

The main focus of the algebraic theory of process calculi is on equivalences of processes. These equivalences are extensional, or observational, in the sense that two processes are deemed to be equal if nodifference between them can be detected by other processes. Many observational equivalence relations
have been proposed in literature. They differ in the way observations are carried out and the extent
observations are made.
In an interleaving framework there are basically two approaches to detect difference between processes.
In the static approach two processes are placed in a same environment and the behaviours of the two
resulting systems are observed to the extent required by a particular application. Here the environmentis assumed static in the sense that it is not affected by external factors. The environment evolves only
as the result of its interactions with the subject processes. This approach is very much influenced by
the traditional view of equivalence of sequential programmes. The most well known equivalence relation
using the static approach is probably the testing equivalence ([8, 3]). The other approach is based ona dynamic viewpoint. In this latter approach environments are subject to the influence of the outside
8

world and therefore can change all the time. This open world view is a reasonable one in the lightof modern development of the concept of computation. For mobile computing, distributed computing,Internet computing or global computing, it is safer to regard the environment as dynamic. Now for two
processes to be indistinguishable in the dynamic viewpoint, not only that the operational behaviours of
the two processes should simulate each other in every environment but also that the descendants of thetwo processes after the simulation should be able to simulate each other in every possible environment.
Equivalence relations enjoying the above conditions are various bisimulation equivalence relations on CCS
processes. The idea of Park ([35]) and Milner ([31]) is that two (strongly) bisimilar processes P and Q
should meet the zigzag property:
P and Q are bisimilar if and only if the following two conditions are satisfied:λλ(i) If P −→ P 0 then Q −→ Q0 for some Q0 such that P 0 and Q0 are bisimilar.
λλ(ii) If Q −→ Q0 then P −→ P 0 for some P 0 such that P 0 and Q0 are bisimilar.
Here λ stands for an arbitrary action. The zigzag argument guarantees that whenever P performs anaction and evolves to P 0 in an environment then Q can perform the same action and become Q0 suchthat P 0 and Q0 are subject to the same zigzag argument. This bisimulation property is strong enough toensure that bisimilar processes are observational equivalent in a dynamic computational environment. It
is clear that the above clauses are the description of a property rather than the prescription of a definition.
There are many relations that enjoy the zigzag property. Any one of them gives rise to an equivalence
relation. So what one is looking for is the largest such relation, which is often called bisimilarity. The
strong bisimilarity of CCS is defined as follows:
Let R be a binary relation on the set of CCS processes. R is said to be a strong bisimulation
if P RQ implies the following properties:λλ(i) If P −→ P 0 then Q −→ Q0 for some Q0 such that P 0 RQ0 .
λλ(ii) If Q −→ Q0 then P −→ P 0 for some P 0 such that P 0 RQ0 .
The strong bisimilarity is the largest strong bisimulation.
Studies on π-calculus for example have inherited a lot of techniques and ideas from previous investigations on CCS. There is however many phenomena in π-calculus that call for completely new treatment.
The very definition of bisimulation of π-processes for instance poses problems not known in the studies of
CCS. For example, if one simply transplants the definition of strong bisimilarity for CCS to π-calculus,
one would obtain a relation too weak to be practical.
Definition 1. Let R be a binary relation on the set of nondeterministic mobile processes. R is said tobe a strong ground bisimulation if P RQ implies the following properties:ππ(i) If P −→ P 0 then Q −→ Q0 for some Q0 such that P 0 RQ0 .
ππ0(ii) If Q −→ Q then P −→ P 0 for some P 0 such that P 0 RQ0 .
The strong ground bisimilarity ∼g is the largest strong ground bisimulation.
For one thing the strong ground bisimilarity is not closed under the prefix operation. For a binary
relation on the set of nondeterministic mobile processes to be closed under input operator, it is necessarythat the relation be closed under substitutions of names. One solution is to take the largest bisimulation
closed under substitution to be the equivalence relation. This is precisely the approach adopted by
Sangiorgi ([42]).
Definition 2. The strong open bisimilarity ∼o is the largest strong ground bisimulation that is closed
under substitution.
In a standard manner we can define weak open bisimilarity.
Definition 3. Let R be a binary relation on the set of nondeterministic mobile processes. R is said tobe a weak open bisimulation if it is closed under substitution and if whenever P RQ then the following
properties hold:ππb(i) If P −→ P 0 then Q =⇒ Q0 for some Q0 such that P 0 RQ0 .
ππb(ii) If Q −→ Q0 then P =⇒ P 0 for some P 0 such that P 0 RQ0 .
The weak open bisimilarity ≈o is the largest weak open bisimulation.

9

M1
M2
M3
S1
S2
S3
S4

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

=
=
=
=
=
=
=

µ0 P
[x=y]P [y/x][x=y]P +[x=y]Q
PQ+P(P +Q)+RP

if µ ⇔ µ0

Figure 5: The Core System ASc
The relation ≈o is not a congruence relation; it is not closed under the choice operator. From both aprogramming point of view and an algebraic point of view one is interested in congruence relations. The
canonical way to obtain a congruence from a bisimulation equivalence is to take the largest congruence
relation contained in the bisimulation equivalence. This approach was adopted by Milner in the studyof CCS ([31]) and is now widely used in process algebra. Alternatively one can define the congruencein terms of the bisimulation equivalence. For π-calculus this alternative definition can be given in a
uniform manner. In the following definition we assume that ≈ is an arbitrary bisimulation equivalenceon π-processes.
Definition 4. Two processes P and Q are weakly congruent, notation P ' Q, if P ≈ Q and, for each
substitution σ, the following conditions are satisfied:ττ(i) If P σ −→ P 0 then Q0 exists such that Qσ =⇒ Q0 and P 0 ≈ Q0 .
ττ(ii) If Qσ −→ Q0 then P 0 exists such that P σ =⇒ P 0 and P 0 ≈ Q0 .
We will write 'o for the open congruence defined from ≈o in the manner of Definition 4.

2.2

Equational System

For each equivalence, one searches for an inference system consisting of a finite set of equalities and afinite set of rules. A useful inference system should be both sound and complete for the observational
equivalence. Soundness means that all derivable equalities are equivalent whereas completeness says that
all equivalent processes can be proved equal in the system. A completeness theorem for an equivalence
is a landmark in our understanding of the relation.
In [32] Milner, Parrow and Walker propose four bisimulation congruence relations, which are respectively strong early equivalence, strong late equivalence, weak early congruence and weak late congruence.
To study the axiomatization of the π-calculus, they introduce the match operator and formulate theexpansion law in terms of this new operator. The importance of the match operator is that it enables
one to code up concurrency of mobile processes in terms of nondeterminism in an interleaving framework,
using the well-known expansion law. In the same paper Milner, Parrow and Walker have initiated thestudy of complete systems for mobile processes. Technically speaking the systems they propose are forthe strong late bisimilarity and the strong early bisimilarity. These two relations are not congruence
relations. In the systems for the two bisimilarities there is a noteworthy inference rule:
If P [y/x] = Q[y/x] for every name y free in either P or Q then a(x).P = a(x).Q.
For systems of congruence relations the above inference rule can be simplified to the following rule:
If P = Q then a(x).P = a(x).Q.
In this paper all axiomatic systems are for congruence relations.
A complete system for a weak observational equivalence consists of two parts. One is the subsystemcomplete for the corresponding strong observational equivalence. The other contains the so-called tau
laws. In this section we give an equational system that is the core of all the systems studied in this paper.
This system is given in Figure 5, which was first used by Sangiorgi in [42]. It is actually the complete
system for the strong open bisimilarity on the finite nondeterministic mobile processes.
Suppose R1 , . . . , Rn are equational laws. Provability in system ASc ∪ {R1 , . . . , Rn } is defined asfollows: ASc ∪ {R1 , . . . , Rn } ` P = Q if one of the followings holds:• P ≡ Q, meaning that P and Q are the same syntactical object;
10

MD1
MD2
MD3
SD1
SD2

[x=y]0[x=x]P
µP
P +P
µP +P

=
=
=
=
=

0
P
µ(P σµ )P
P

Figure 6: Derived Laws of ASc• Some context C[] and processes A, B exist such thatP ≡ C[A]C[B] ≡ Q
and either A = B or B = A is an instance of one of the axioms in ASc ∪ {R1 , . . . , Rn };• Some contexts C1 [], . . . , Cn [] and processes A1 , . . . , An , B1 , . . . , Bn , for n ≥ 2, exist such thatP ≡ C1 [A1 ]C1 [B1 ] ≡ C2 [A2 ]..
.
Cn−1 [Bn−1 ] ≡ Cn [An ]Cn [Bn ] ≡ Q
and, for all i ∈ {1, . . . , n}, either Ai = Bi or Bi = Ai is an instance of one of the axioms in
ASc ∪ {R1 , . . . , Rn }.
A more popular way to define the provability in ASc is to introduce equivalence and congruence
rules. The equivalence rules say that the provability relation is reflexive, symmetric and transitive. The
congruence rules declare that the provability relation is closed under all the operators of the calculus.
For instance from P = Q one can derive that π.P = π.Q, P +R = Q+R and [x=y]P = [x=y]Q. Write
ASc `0 P = Q to mean that the equality P = Q is derivable from the axioms of ASc together with theequivalence and congruence rules. The following lemma can be proved by simple induction.
Lemma 5. ASc `0 P = Q if and only if ASc ` P = Q.
From now on we will confuse the two notations and use only `.
When ASc ∪ {R1 , . . . , Rn } ` P = Q we say that P = Q is provable in ASc ∪ {R1 , . . . , Rn } or that
R1 ,...,Rn

P = Q is a derived law of ASc ∪ {R1 , . . . , Rn }. We will write P=
Q to indicate that R1 , . . . , Rn are
the major laws and/or rules in the derivation of P = Q. Some derived laws of ASc are given in Figure 6,
which have all been used by Sangiorgi in [42].
For a finite collection {Pi }i∈{1,...,n} of processes, we writeXPii∈{1,...,n}for the process(. . . ((P1 +P2 )+P3 )+ . . .)+Pn
In view of S2 and S3 the order of the occurrence of Pi in the above expression does not matter. As amatter of fact we will often write
P1 +P2 +P3 + . . . +Pn
without any parenthesis since it does not cause any confusion in the algebraic investigation.
A process P is in normal form if it is of the shapeX
X
Xµi τ.Piµi ai (x).Pi +µi ai xi .Pi +
i∈I1

i∈I2

11

i∈I3

T1
T2
T3

π.τ.P
P + τ.P
π.(P + τ.Q)

=
=
=

π.P
τ.P
π.(P + τ.Q) + π.Q

Figure 7: Milner’s Tau Laws
in which x does not appear free in P and I1 , I2 , I3 are pairwise distinct. The depth of a normal form
def
def
def
process, notation d(P ), is defined as follows: (i) d(0) = 0; (ii) d(π.P ) = 1 + d(P ); (iii) d(P +Q) =def

max{d(P ), d(Q)}; (iv) d([x=y]P ) = d(P ).
In ASc a process can be converted to a normal form process without increasing its depth. Its proof isstandard.
Lemma 6. A process P is provably equal to a normal form process P 0 in the system ASc such thatd(P 0 ) ≤ d(P ).
The proof of the following completeness theorem can be found in [42].
Theorem 7. ASc is sound and complete for ∼o .

2.3

The Insufficiency of Milner’s Tau Laws for Open Semantics

In view of the fact that in CCS Milner’s three tau laws are capable of promoting a complete system
for the strong congruence to a complete system for the weak congruence, one is tempted to think thatthe same is true for the calculus of nondeterministic mobile processes. Figure 7 gives the tau laws in
π-calculus. The soundness is obvious.
Theorem 8. ASc ∪ {T 1, T 2, T 3} is sound for 'o .
The popular view would have us believe that the corresponding completeness theorem also holds. In
the rest of this section we prove that this is not the case.
A process P is a t-process if it contains neither input prefix nor output prefix. For instance [x=y](τ +[a=b]τ.τ ) is a t-process, but [x=y]a(x) is not. In the following proof, we need to work with t-processes
with holes. For that purpose we introduce the notion of t-context defined as follows: (i) [] is a t-context;(ii) if C[] is a t-context then C[] + P , P + C[], τ.C[] and [x=y]C[] are t-contexts, where P is a t-process.
In other words t-contexts are contexts with neither input prefix nor output prefix. With the help of tcontexts, it is easy to indicate an occurrence of τ in a t-process. Suppose P is a t-process and P ≡ C[τ.Q]
for some t-context C[] and some t-process Q. Then the explicit τ in C[τ.Q] is an occurrence of τ in P . In
what follows we will simply say that P ≡ C[τ.Q] is a tau occurrence in P . A terminating tau occurrenceis a tau occurrence P ≡ C[τ.Q] such that Q contains no occurrence of τ .
Definition 9. The match guard of a t-context C[], written M (C[]), is a list of equalities defined asdeffollows: (i) M ([]) is the empty list; (ii) M (C[]) = M (C 0 []) if C[] is C 0 []+P , or P +C 0 [], or τ.C 0 []; (iii)defM ([x=y]C[]) = x=y, M (C[]).
We will say that the match guard of a (terminating) tau occurrence P ≡ C[τ.Q] in P is the match
list M (C[]).
Definition 10. A process P is in t4-form if it is a t-process and for some distinct x and y the following
properties hold:
1. There exists some tau occurrence P ≡ C[τ.Q].
2. For every terminating tau occurrence P ≡ C 0 [τ.Q0 ] it holds that M (C 0 []) ⇒ x=y.
If a process has a tau occurrence it has a terminating tau occurrence. It follows that a process in
t4-form contains at least one match operator.
Lemma 11. Suppose P is a process in t4-form and ASc ∪ {T 1, T 2, T 3} ` P = Q. Then Q is also in
t4-form.
12

Proof. Suppose P is a process in t4-form. Suppose further that ASc ∪ {T 1, T 2, T 3} ` P = Q is ASc ∪{T 1, T 2, T 3} ` C[A] = C[B] for some t-context C[], obtained by applying one of the axioms.
• ASc ∪ {T 1, T 2, T 3} ` C[A] = C[B] is ASc ∪ {T 1, T 2, T 3} ` C[µR] = C[µ0 R], obtained by applying
M1. Suppose that for a particular terminating tau occurrence in R its match guard in C[µR] andC[µ0 R] are µ1 and µ01 respectively. Then µ1 ⇔ µ01 because µ ⇔ µ0 . It follows from µ1 ⇒ x=y thatµ01 ⇒ x=y. If R has no occurrence of τ then C[µR] has a terminating tau occurrence in C[]. So
C[µR] has a terminating tau occurrence. Thus C[µ0 R] satisfies the two conditions of Definition 10
and therefore is in t4-form.
• ASc ∪{T 1, T 2, T 3} ` C[A] = C[B] is ASc ∪{T 1, T 2, T 3} ` C[[a=b]R] = C[[a=b]R[b/a]], obtained byapplying M2. If a = b then C[[a=b]R[b/a]] ≡ C[[a=b]R]. Otherwise let µ, a = b, a1 = b1 , . . . , an = bn
be the match guard in C[[a=b]R] of a terminating tau occurrence in R. Then the match guardµ0 of that particular terminating tau occurrence in C[[a=b]R[b/a]] is the list µ, a = b, a1 [b/a] =b1 [b/a], . . . , an [b/a] = bn [b/a]. It should be clear thatµ0

⇔ µ, a = b, a1 [b/a] = b1 [b/a], . . . , an [b/a] = bn [b/a]⇔ µ, a = b, a1 = b1 , . . . , an = bn
⇒ x = y.

Therefore C[[a=b]R[b/a]] is in t4-form.
• ASc ∪ {T 1, T 2, T 3} ` C[A] = C[B] is ASc ∪ {T 1, T 2, T 3} ` C[[a=b](R + S)] = C[[a=b]R + [a=b]S],
obtained by applying M3. Then the match guard in C[[a=b](R+S)] of a terminating tau occurrencein R is the same as the match guard in C[[a=b]R + [a=b]S] of the terminating tau occurrence in R.
It follows that C[[a=b](R + S)] is in t4-form if and only if C[[a=b]R + [a=b]S] is in t4-form.
• ASc ∪ {T 1, T 2, T 3} ` C[A] = C[B] is obtained by applying S1, or S2, or S3. In these cases C[B] isobviously in t4-form.
• ASc ∪ {T 1, T 2, T 3} ` C[A] = C[B] is ASc ∪ {T 1, T 2, T 3} ` C[[x=y]R + R] = C[R], obtained byapplying S4. If R contains a tau occurrence, then all terminating tau occurrences in [x=y]R + R
are also terminating tau occurrences in C[[x=y]R + R]. As C[[x=y]R + R] is in t4-form, all theseterminating tau occurrences satisfy the second condition in Definition 10. It follows that C[R] alsosatisfies the second condition in Definition 10. Thus C[R] is in t4-form.
• ASc ∪ {T 1, T 2, T 3} ` C[A] = C[B] is obtained by applying T1. If P has no occurrence of tau,then both τ.τ.P and τ.P have only one terminating occurrence. Otherwise a tau occurrence in P
is terminating in τ.τ.P if and only if it is terminating in τ.P . This is enough to show that C[B] isin t4-form.
• ASc ∪ {T 1, T 2, T 3} ` C[A] = C[B] is obtained by applying T2 or T3. The situation is similar tothe previous one.
This completes the proof.
Theorem 12. τ.[x=y]τ = τ is not provable in ASc ∪ {T 1, T 2, T 3}.
Proof. It is clear that τ.[x=y]τ is in t4-form. If ASc ∪ {T 1, T 2, T 3} ` τ.[x=y]τ = Q then, by Lemma 11,
Q is in t4-form. So Q contains at least one match operator, which means that it can not be τ .

2.4

The Failure of Hennessy Lemma for Mobile Processes

In the proof of completeness theorem for the weak congruence in CCS, the following result, which is
attributed to Hennessy in [31], plays a crucial role:
Lemma 13 (Hennessy Lemma). If P ≈ Q then either τ.P ' Q or P ' Q or P ' τ.Q.
Here ≈ is the weak bisimilarity and ' is the largest congruence relation contained in ≈. In the proofof the completeness theorem by induction, Hennessy Lemma helps to lift P ≈ Q to either τ.P ' Q or
P ' Q or P ' τ.Q, thus allowing the induction hypothesis to apply.
13

T4

τ.P

=

τ.(P + [x=y]τ.P )Figure 8: The Fourth Tau Law
In π-calculus however Hennessy Lemma does not hold in general! For a counter example, consider
the following three propositions
τ.[x=y]τ
[x=y]τ
[x=y]τ

=o
=o
=o

0
0
τ

(1)
(2)
(3)

None of them holds although [x=y]τ ≈o 0 is true. In (1) a tau action from τ.[x=y]τ can not be matched
up by any tau action from 0. In (2) a tau action from ([x=y]τ )[x/y] can not be matched up by any
tau action from 0[x/y]. And in (3) a tau action from τ can not be matched up by any tau action from[x=y]τ .
In the calculus of mobile processes, local version of Hennessy Lemma does hold. Let’s explain what
we mean by that using the above example. Assuming x = y then (3) is valid. If x 6= y then (2) is true.
In the symbolic approach ([20, 4]), complete systems for weak congruence relations can be achieved by
exploiting the local Hennessy Lemma.
A provability judgement in the symbolic approach is of the form C `AS P = Q, where AS is anaxiomatic system and C is a set of equalities and/or inequalities on names. Among the non-symbolic
approach, Sangiorgi’s open semantics is the simplest ([42]). Provability in Sangiorgi’s system is of theform `AS P = Q for at least the part of π-calculus without the restriction operator. Axiomatization ofopen congruences has been discussed in the strong case, but not in the weak case. The failure of Hennessy
Lemma is another way to say that the three tau laws fail to lift a complete system for the strong open
bisimilarity to a complete system for the weak open congruence as the resulting system is not capable ofproving the equality τ.[x=y]τ = τ .

2.5

The Fourth Tau Law

We need to extend ASc ∪ {T 1, T 2, T 3} to achieve a complete system for the weak open congruence. We
will show that it is sufficient to add a single law, the fourth tau law. The new axiom, T4 in Figure 8,
involves a match operator. It is the simplest among all the alternatives we have come up with. Some of
the consequences of T4 are discussed below.
Lemma 14. ASc ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.(P + µτ.P ).
Proof. When µ is empty, the result follows from T1 and T2. So the base case holds. Now observe that
τ.P

T4

=

SD2

=

I.H.

=

M2

=

M1

=

M2

=

T4

=

τ.(P + [x=y]τ.P )τ.(P + µ[x=y]τ.P + [x=y]τ.P )τ.(P + µ[x=y]τ.P + [x=y]τ.(P + µτ.P ))τ.(P + µ[x=y]τ.P + [x=y]τ.(P + µτ.P )[y/x])
τ.(P + µ[x=y]τ.P + [x=y]τ.(P + µ[x=y]τ.P )[y/x])
τ.(P + µ[x=y]τ.P + [x=y]τ.(P + µ[x=y]τ.P ))τ.(P + µ[x=y]τ.P )So the proof can be completed by induction on the number of match operators in µ.
PLemma 15. ASc ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.(P + i∈I µi τ.P ) for a finite nonempty indexing set I.

14

Proof. Lemma 14 provides the base step, and the following derivation provides the induction step:
X
X
X
I.H.
τ.(P +µi τ.P + µτ.P ) = τ.(P +µi τ.P + µτ.(P +µi τ.P ))
i∈I

i∈I

=

τ.(P +

Xi∈Iµi τ.P )

i∈I
I.H.

=

τ.P

where the second equality holds by Lemma 14.

2.6

Saturation

The proof of completeness is always much harder than that of soundness. In the standard proof ofcompleteness theorem for the weak congruence on finite CCS processes ([21, 31]), one verifies first thatevery normal form process is provably equivalent to a saturated normal form process using the three tauααlaws. Recall that a process P is saturated if, for every α, P −→ P 0 whenever P =⇒ P 0 . It follows thatα00
P is in saturated normal form if and only if whenever P =⇒ P then α.P is a summand of P . Now if Pααand Q are weakly congruent saturated normal form processes and P −→ P 0 then Q =⇒ Q0 for some Q0α000such that Q ≈ P , where ≈ denotes the weak equivalence. By saturation, Q −→ Q and therefore α.Q0
is a summand of Q. If, and this is a nontrivial if, we can deduce by induction hypothesis that α.P 0 isprovably equal to α.Q0 , which is much weaker than saying that P 0 is provably equal to Q0 , then we canconclude that every summand of P is provably equal to a summand of Q, and vice versa. This gives us
the required completeness.
If one is only interested in completeness proof, then the notion of saturated process is not needed.
What is really necessary is the following saturation property:α

If P =⇒ P 0 and P is in normal form then P and P + α.P 0 are provably equal.
From the point of view of axiomatization, the role of saturation property is to relate operational semantics
to equational rewriting.
For π-calculus the situation is a little bit more complex.
Lemma 16 (saturation). Suppose Q is in normal form. The following saturation properties hold:ax(i) If Qσµ =⇒ Q0 then ASc ∪ {T 1, T 2, T 3} ` Q = Q + µax.Q0 .
a(x)(ii) If Qσµ =⇒ Q0 then ASc ∪ {T 1, T 2, T 3} ` Q = Q + µa(x).Q0 .
τ(iii) If Qσµ =⇒ Q0 then ASc ∪ {T 1, T 2, T 3} ` Q = Q + µτ.Q0 .
Proof. A standard exercise using Milner’s tau laws.
In the proof of the saturation lemma, the role of Milner’s tau laws is to systematically remove tau
prefixes which only induce operationally unobservable actions.

2.7

Promotion

A careful examination of the role of Hennessy Lemma in the completeness proof for CCS shows that what
it really comes down to is the following property:
If P ≈ Q then either τ.P = Q, or P = Q, or P = τ.Q is provable.
So Hennessy Lemma helps to transfer a semantic statement to a proof theoretical one. As a matter offact, as far as completeness is concerned, the following weaker property is all one needs:
If P ≈ Q then τ.P = τ.Q is provable.
We will call it promotion property. Although the Hennessy Lemma does not hold in the calculus ofnondeterministic mobile processes, the promotion property does hold.
Lemma 17 (promotion). If P ≈o Q then ASc ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.Q.

15

Proof. Suppose P ≈o Q. The proof is carried out by induction on the sum of the depths of P and Q. By
Lemma 6 we may concentrate on normal form processes. Suppose P is of the form
X
X
X
µi τ.Piµi ai (x).Pi +µi ai xi .Pi +
i∈I1

i∈I3

i∈I2

and Q is of the formXµj aj (x).Qj +

j∈J1

X

X

µj aj xj .Qj +j∈J2µj τ.Qjj∈J3
ai σµ (x)ai σµ (x)ii
If µi ai (x).Pi is a summand of P then (µi ai (x).Pi )σµi −→Pi σµi must be matched up by Qσµi =⇒0000Q such that Pi σµi ≈o Q . Both Pi σµi and Q are in normal form and d(Pi σµi ) + d(Q ) < d(P ) + d(Q).
So by induction hypothesis ASc ∪ {T 1, T 2, T 3, T 4} ` τ.Pi σµi = τ.Q0 . It follows thatASc ∪ {T 1, T 2, T 3, T 4} ` µi ai (x).Pi

M D3

=

T1

µi ai σµi (x).Pi σµi=µi ai σµi (x).τ.Pi σµi

I.H.

=

µi ai σµi (x).τ.Q0

T1µi ai σµi (x).Q0=

Therefore ASc ∪ {T 1, T 2, T 3, T 4} ` µi ai (x).Pi + Q = µi ai σµi (x).Q0 + Q = Q by Lemma 16. Similarly
one proves that ASc ∪ {T 1, T 2, T 3, T 4} ` µi ai xi .Pi + Q = Q whenever µi ai xi .Pi is a summand of P .
τ
Now suppose µi τ.Pi is a summand of P . Then (µi τ.Pi )σµi −→ Pi σµi . Some Q0 must exist such thatτPi σµi ≈o Q0 and either Qσµi =⇒ Q0 or Qσµi ≡ Q0 . By induction hypothesis ASc ∪ {T 1, T 2, T 3, T 4} `τ.Pi σµi = τ.Q0 is provable. In the first case it can be easily shown that ASc ∪ {T 1, T 2, T 3, T 4} `µi τ.Pi + Q = Q, using Lemma 16. In the second case one has
ASc ∪ {T 1, T 2, T 3, T 4} ` µi τ.Pi

M D3

=
=

M D3

=

P

µi τ.Pi σµiµi τ.Qσµiµi τ.QP

In summary ASc ∪ {T 1, T 2, T 3, TP
4} ` i∈I3 µi τ.Pi + Q = i∈I µi τ.Q + Q for some subset I of I3 . So
ASc ∪{T 1, T 2, T P
3, T 4} ` P +Q = i∈I µi τ.Q+Q. It follows from Lemma 15 that ASc ∪{T 1, T 2, T 3, T 4} `τ.(P +Q) = τ.( i∈I µi τ.Q + Q) = τ.Q. Symmetrically ASc ∪ {T 1, T 2, T 3, T 4} ` τ.(P +Q) = τ.P .
Therefore ASc ∪ {T 1, T 2, T 3, T 4} ` τ.P = τ.Q.
The promotion lemma relates the algebraic semantics to equational rewriting. It promotes a pair ofsemantically equivalent processes to a pair of proof theoretically equal processes.

2.8

CompletenessThe saturation and promotion properties suffice to establish the following absorption property:
If P and Q are congruent then P + Q is provably equal to P .
Of course, under the same assumption, P + Q is also provably equal to Q. Hence the completeness.
Theorem 18 (completeness). ASc ∪ {T 1, T 2, T 3, T 4} is sound and complete for =o .
Proof. The soundness part is clear. The proof of completeness is almost the same as that of Lemma 17.
Suppose P =o Q for normal form processes P and Q and that µi τ.Pi is a summand of P . Thenττ(µi τ.Pi )σµi −→ Pi σµi must be matched up by Qσµi =⇒ Q0 for some Q0 such that Pi σµi ≈o Q0 . By
Lemma 17, ASc ∪ {T 1, T 2, T 3, T 4} ` τ.Pi σµi = τ.Q0 . Therefore ASc ∪ {T 1, T 2, T 3, T 4} ` µi τ.Pi + Q = Q.
Thus ASc ∪{T 1, T 2, T 3, T 4} ` P +Q = Q. Symmetrically ASc ∪{T 1, T 2, T 3, T 4} ` P +Q = P . Therefore
ASc ∪ {T 1, T 2, T 3, T 4} ` P = Q.
The proof of the completeness theorem is very similar to that of promotion lemma. The difference is to
do with the induction step. In the latter proof one uses induction hypothesis whereas in the former proof
one refers to the promotion lemma. This is a general phenomenon. As a matter of fact the difference
between the proof of a promotion property and that of the associated completeness theorem is so minor
and routine that in most cases the latter proof can be safely omitted.
16

2.9

RemarkThe previous sections convey three pieces of information. The first is that Hennessy Lemma does nothold in calculi of mobile processes. The second is that Milner’s three tau laws are insufficient for weak
open congruence on mobile processes. And the third is that a new tau law is necessary to deal withmatch operator under prefix operation. The first two are closely related. All the three observations havewide implications to non-symbolic approach to axiomatization.
It has come a long way to settle down on the axiom T4. The first solution, proposed by Fu in an
early version of [14], is a conditional equation rule formulated as follows:PP
P + i∈I µi τ.P = Q+ j∈J µi τ.Q
τ.P = τ.Q
The premises of the rule is an equational formalization of P ≈o Q. The role of the rule is to promote
P ≈o Q to τ.P = τ.Q, which is necessary to allow the proof of Lemma 17 to go through. In the final
version of [14] Fu made an observation that the rule is equivalent to the following law:Xτ.P = τ.(P +µi τ.P )i∈I

It was after the submission of the final version of [14] that he realized that, in the presence of ASc ∪{T 1, T 2, T 3}, the above equality can be simplified toτ.P = τ.(P +µτ.P )which can be further simplified to T4. It is difficult to imagine an equivalent axiom that is simpler
than T4. This fourth tau law pinpoints the places where Milner’s three tau laws fail. In the presenceof the match operator, Milner’s tau laws fail to cover all the aspects of mobility incurred by internal
communication.
In [14] the following equality is given as an equality that holds semantically but is possibly not provableby Milner’s tau laws:(4)
τ.(ax + [x=y]ay) = τ.ax
Notice that (4) is an instance of T4. The discovery of T4 led us immediately toτ.[x=y]τ = τ(5)This is probably the simplest counter example. Thanks to its simplicity, we are able to formally justify
our intuition that (5) is not provable using only Milner’s tau laws.

3

The Pi Calculus without Mismatch

The π-calculus without the mismatch operator is the calculus of nondeterministic mobile processes extended with the parallel composition operator and the restriction operator. In this section we investigate
some aspects of the algebraic theory of this language. The novelty of this section is as follows: (i) We
give a complete system for the weak open congruence of the π-calculus without the mismatch operator
using distinction. (ii) We give an alternative complete system without using distinction.

3.1

Parallel Composition

Syntactically if P and Q are processes then P |Q is a process of the parallel composition form. Semanticallythe two components of the processes P |Q can either evolve independently or communicate throughcommon names. In π-calculus the operational semantics of the operator is defined as follows:
Composition
λP −→ P 0bn(λ) ∩ f n(Q) = ∅λ

P |Q −→ P 0 |Q

a(x)

ay

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

17

a(x)

a(x)

P −→ P 0
Q −→ Q0τP |Q −→ (x)(P 0 |Q0 )We have left out the symmetric rules. This operator does not have any effect on the definition ofopen bisimilarity. Definition 22 remains valid. From the point of view of axiomatization, the parallel
composition operator can be easily dealt with using the well-known expansion law. In π-calculus the law
takes the following form ([32]):
λi =a(x)P |Q =

Xµi λi .(Pi |Q) +i∈IXµj λj .(P |Qj ) +j∈JXµi µj τ.(Pi [y/x]|Qj ) +λj =ayλXi =ayµi µj τ.(Pi |Qj [y/x])

λj =a(x)PP
where P is i∈I µi λi .Pi and Q is j∈J µj λj .Qj . This law makes most evident the philosophy of interleaving semantics. The expansion law for the full π-calculus with the mismatch operator can be obtainedby replacing the µi and µj in the above law by ϕi and ϕj respectively, where ϕi and ϕj denote arbitrary
finite sequences of mixed match and/or mismatch operators.
In the rest of this paper we ignore the parallel composition operator most of the time. This operator
is significant only in Section 4.1.5.

3.2

Restriction

A restriction process usually takes the form (x)P , where (x) is the restriction operator. The name x in(x)P is also bound. The operational semantics of the subcalculus of π with the prefix, restriction, matchand choice operators is defined below.
Prefixππ.P −→ P
Restriction
λP −→ P 0ax

P −→ P 0

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

Match
λ

P −→ P 0λ[x=x]P −→ P 0
ChoiceλλP −→ P 0

Q −→ Q0λλ

P +Q −→ P 0

P +Q −→ Q0

In the above rules λ ranges over {a(x), ax, a(x) | a, x ∈ N } ∪ {τ }. The label a(x) denotes a restricted
output, where x is bound. We will also use λ to range over the set of extended prefixes, which contains
the tau, the input prefixes, the output prefixes and the restricted output prefixes. A restricted output
prefix is defined as follows:defa(x).P = (x)ax.P
def

The set of the subject names of λ, notation subj(λ), is defined as follows: (i) subj(τ ) = ∅; (ii)
def

def

def

subj(a(x)) = {a}; (iii) subj(ax) = {a}; (iv) subj(a(x)) = {a}. The definition of context has totake into consideration of restriction. Formally we add to the previous definition of context the following
clause: (x)C[] is a context whenever C[] is a context.
The restriction operator adds a lot of expressive power to the calculus of mobile processes. It also
adds complications to semantics. For instance, the definition of the open bisimulation must be modified
since a free name introduced by a restricted output action should be kept distinct from any other name.
In order to formalize the idea, Milner, Parrow and Walker introduced distinctions ([32]). A distinction
imposes permanent inequalities on names.
Definition 19. 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}. The set of distinctions
will be denoted by D.
Definition 20. A substitution σ respects a distinction D if (a, b) ∈ D implies σ(a) 6= σ(b). Similarly, amatch sequence µ respects a distinction D if (a, b) ∈ D implies µ 6⇒ a=b.
18

L1
L2
L3
L4
L5
L6
L7

(x)0
(x)(y)P(x)(P +Q)(x)π.P(x)π.P(x)[y=z]P(x)[x=y]P

=
=
=
=
=
=
=

0
(y)(x)P(x)P +(x)Q
π.(x)P0[y=z](x)P0

if x 6∈ n(π)
if x ∈ subj(π)
if x 6∈ {y, z}
if x 6= yFigure 9: General Axioms for Restriction
Using the above definition, Sangiorgi defined a class of distinction indexed bisimulations in [42].
Definition 21. The set R = {RD }D∈D of binary symmetric relations on processes is a strong open
bisimulation if, for each distinction D ∈ D and for each substitution σ respecting D, P RD Q implies thefollowing 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 strong open bisimilar to Q with respect to D, notation P ∼D
o Q, if there exists a strong open
bisimulation R = {RD }D∈D such that (P, Q) ∈ RD . We say that P is strong open bisimilar to Q if
P ∼∅o Q.
The equivalence ∼∅o will be compared to an alternative definition of strong open bisimilarity for thefull π-calculus with the mismatch operator. Since we will take a close look at the weak version of ∼∅o , wewill not say anything more about it except stating a completeness result at the end of this section.
Definition 22. The set R = {RD }D∈D of binary symmetric relations on processes is a weak open
bisimulation if for each distinction D ∈ D and for each substitution σ respecting D, P RD Q implies thefollowing 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 = {RD }D∈D such that (P, Q) ∈ RD . We say that P is weak open bisimilar to Q if P ≈∅o Q.
In the standard manner one can define the largest congruence '∅o contained in ≈∅o .
The proofs of the two lemmas below use the standard argument ([42]).
00D
Lemma 23. If P ≈Do Q and D ⊆ D then P ≈o Q.
DσµLemma 24. If µ respects D then P σµ ≈o

3.3

Qσµ implies µP ≈Do µQ.

System Using Distinction

We now begin to investigate the weak open congruence. This subsection follows [42] closely. Our contribution is to give a complete system for the weak open congruence. To get a complete system for '∅o , weneed laws that deal with the restriction operator. Now the system actually allows one to derive equalities indexed by distinctions. So there are also some laws that manipulate indexed equalities. Figure 9
summarizes some general laws for restriction, which appeared first in [32]; and Figure 10 provides three
distinction indexed laws due to Sangiorgi ([42]).
Let ASd be ASc ∪ {L1, L2, L3, L4, L5, L6, L7, LI1, LI2, LI3}. Note that the law L7 is derivable fromASd \ {L7} using LI1 and LI3. In some systems without the indexed equalities LI1, LI2 and LI3, the law
L7 is indispensable.
In ASd one can show that every process can be rewritten to a normal form. But since equalities are
now indexed by distinctions, we need to define normal forms with respect to distinctions.
P
Definition 25. Suppose D is a distinction. A process P is a D-normal form, or D-nf, if P ≡ i∈I µi λi .Pi
such that, for each i, µi respects D and Pi σµi is a Dσµi -normal form.
19

LI1
LI2
LI3

[a=b]P
P
(x)P

=D
=D
=D\x

if (a, b) ∈ D
if P =D0 Q and D0 ⊆ D
if P =D Q

0
Q
(x)Q

Figure 10: Distinction Indexed Axioms
The definition of the depth of a process need be modified to take into account of the restriction
operator. Let d((x)P ) be the same as d(P ).
Lemma 26. Suppose D is a distinction and P is a process. Then there is a D-nf H such that ASd `P =D H and d(H) ≤ d(P ).
The proof of the above lemma can be found in [42]. The proof of the saturation properties, stated in
the next lemma, is simple.
Lemma 27. Suppose Q is a normal form. The following saturation properties hold:ax(i) If Qσµ =⇒ Q0 then ASd ∪ {T 1, T 2, T 3} ` Q = Q + µax.Q0 .
a(x)(ii) If Qσµ =⇒ Q0 and x does not appear in µ then ASd ∪ {T 1, T 2, T 3} ` Q = Q + µa(x).Q0 .
τ(iii) If Qσµ =⇒ Q0 then ASd ∪ {T 1, T 2, T 3} ` Q = Q + µτ.Q0 .
a(x)(iv) If Qσµ =⇒ Q0 and x does not appear in µ then ASd ∪ {T 1, T 2, T 3} ` Q = Q + µa(x).Q0 .
The next lemma states the promotion properties.
Lemma 28. If P ≈Do Q then ASd ∪ {T 1, T 2, T 3, T 4} ` τ.P =D τ.Q.
Proof. The proof is similar to that of Lemma 17. By Lemma 26, we can assume that both P and Q
are D-nf’s. We only consider restricted output actions. Suppose µi a(x).Pi is a summand of P and
a(x)

a(x)

0

P σµi −→ Pi σµi . Then Q0 exists such that Qσµi =⇒ Q0 and Pi σµi ≈D
Q0 ≡ Q0 σµi , where D0 =o
Dσµi ∪ {x}×f n(P σµi +Qσµi ) ∪ f n(P σµi +Qσµi )×{x}. Let D00 be D ∪ {x}×f n(P +Q) ∪ f n(P +Q)×{x}.
00
Then µi Pi ≈Dµi Q0 by Lemma 24. So ASd ∪ {T 1, T 2, T 3, T 4} ` τ.µi Pi =D00 τ.µi Q0 by inductionohypothesis. Hence ASd ∪ {T 1, T 2, T 3, T 4} ` ax.µi Pi =D00 ax.µi Q0 , from which it follows from LI3 thatASd ∪ {T 1, T 2, T 3, T 4} ` a(x).µi Pi =D a(x).µi Q0 . Thus
ASd ∪ {T 1, T 2, T 3, T 4} ` Q =D
M2

=D
=D
M2

=D

Q+µi a(x).Q0
Q+µi a(x).µi Q0
Q+µi a(x).µi Pi
Q+µi a(x).Pi

The rest of the proof is similar to that of Lemma 17.
The proof of the completeness theorem is similar to that of Lemma 28.
Theorem 29. ASd ∪ {T 1, T 2, T 3, T 4} is sound and complete for '∅o .
For the purpose of completeness we state a relevant result due to Sangiorgi ([42]).
Theorem 30. ASd is sound and complete for ∼∅o .
We end this section by mentioning that the strong and weak open bisimilarities are conservativeextensions over the ones on nondeterministic mobile processes.
Lemma 31. On the set of nondeterministic mobile processes ∼∅o and ≈∅o coincide respectively with ∼oand ≈o .
The proof of the above lemma amounts to showing that ∼o , respectively ≈o , is a weak, respectively
strong, ∅-open bisimulation and conversely ∼∅o , respectively ≈∅o , is a strong, respectively weak, open
bisimulation. These can be done in a routine manner.

20

L8

(x)C[[x=y]P ]=(x)C[0]x, y are not bound in C[] and x6=yFigure 11: A Schematic Law for Restriction

3.4

A Schematic Law for Restriction

There is an alternative to the complete system studied in the previous subsection. In this new system
one uses a schematic law in favour of the indexed laws LI1, LI2 and LI3. The schematic law, labelled
L8, is given in Figure 11. The reason to call it schematic is that an arbitrary context C[] is used in
the description of the law. When applying L8 one must make sure that neither x nor y is bound in thecontext C[] and that they are distinct names. It is clear that the law L7 is a special case of L8 in thepresence of L1.
The reason to have L8, a law stronger than L7, is to deal with the match operator under restricted
output prefix. For examplea(x).[x=y]P = a(x)is an instance of L8. It is very unlikely that it can be derived from L7.
Let ASr be ASc ∪ {L1, L2, L3, L4, L5, L6, L7, L8}. Then we have the following important result.
Theorem 32. ASr is sound and complete for ∼∅o .
To prove the theorem we need to introduce some additional machinery and establish quite a few
intermediate results. We are not going into these proofs in the present paper. The interested reader isreferred to [17].
The generalization of these proofs to the weak case is a formality.
Theorem 33. ASr ∪ {T 1, T 2, T 3, T 4} is sound and complete for '∅o .

4

The Full Pi Calculus

Complete systems for the strong late congruence and the strong early congruence are given in [37]. The
version of the π-calculus they use has the mismatch operator. Although the operator is debatable froma computational point of view, its role in axiomatization seems indispensable in many places. The full
π-calculus with the mismatch operator has the following abstract syntax:
P := 0 | π.P | (x)P | P +P | [x=y]P | [x6=y]P
where π := a(x) | ax | τ . The operational semantics of the mismatch operator is as follows:
MismatchλP −→ P 0

x 6= yλ[x6=y]P −→ P 0
In the presence of the mismatch operator the operational semantics is no longer preserved by substitution.
In other words the stability property for operational semantics, as stated below, fails:λλσ

If P −→ P 0 then P σ −→ P 0 σ for any substitution σ.
However the next lemma is valid.
λ0

Lemma 34. Suppose P σ −→ P 00 then P 0 and λ exist such that P 00 ≡ P 0 σ and λ0 = λσ.
λσ

So we may write P σ −→ P 0 σ without losing any generality. This fact will be used implicitly later on.
Suppose Y is a finite set {y1 , . . . , yn } of names. The notation [y6∈Y ]P stands for [y6=y1 ] . . . [y6=yn ]P .
When using this notation, the order of the mismatch operators in [y6=y1 ] . . . [y6=yn ]P is not relevant. From
now on we will write φ and ψ to stand for sequences of match and mismatch operators concatenated one
after another, δ for a sequence of mismatch operators, and as before µ for a sequence of match operators.
Consequently we write ψP . When the length of ψ is zero, ψP is just P . The notation φ ⇒ ψ says thatφ logically implies ψ and φ ⇔ ψ that φ and ψ are logically equivalent. The closure of ψ, notation c(ψ),
is defined as follows:21

For x, y such that x 6= y, c(ψ) contains x = y, respectively x 6= y, whenever ψ ⇒ x=y,respectively ψ ⇒ x6=y.
We will write ψ\x for the sequence of match and mismatch operators in c(ψ) that do not involve x. We
will write ¬ψ to mean the disjunction, so to speak, of the negations of the components of ψ. For instanceif ψ is [x=y][a6=b][c=d] then ¬ψP stands for [x6=y]P +[a=b]P +[c6=d]P .
Definition 35. Let V be a finite set of names. We say that ψ is complete on V if n(ψ) ⊆ V and foreach pair x, y of names in V it holds that either ψ ⇒ x=y or ψ ⇒ x6=y.
Suppose ψ is complete on V and n(φ) ⊆ V . Then it should be clear that either ψφ ⇔ ψ or ψφ ⇔ ⊥.
In sequel this fact will be used implicitly.
Definition 36. Suppose σ is a substitution and ψ is a sequence of match/mismatch operators. Thenσ respects ψ if ψ ⇒ x=y implies σ(x) = σ(y) and ψ ⇒ x6=y implies σ(x) 6= σ(y). Dually ψ respects σ
if σ(x) = σ(y) implies ψ ⇒ x=y and σ(x) 6= σ(y) implies ψ ⇒ x6=y. Moreover σ agrees with ψ, andψ agrees with σ, if they respect each other. The substitution σ is induced by ψ if it agrees with ψ andrng(σ) ⊆ n(ψ).
Definition 37. Suppose δ is a sequence of mismatch operators and D is a distinction. Then D respects
δ if δ ⇒ x6=y implies (x, y) ∈ D. Dually δ respects D if (x, y) ∈ D implies δ ⇒ x6=y. Moreover δ agrees
with D if they respect each other.
The proof of the next lemma can be found in [37].
Lemma 38. If φ and ψ are complete on V and both agree with σ then φ ⇔ ψ.
When defining open bisimilarities we need, for every pair x, y of names, an auxiliary operation denotedby ( )[x6=y] . This operation inserts the mismatch operator [x6=y] in front of every prefix operator. The
structural definition goes as follows:(0)[x6=y]

def

=

0

[x6=y]

def=[x6=y]π.P [x6=y] where {x, y} ∩ bn(π) = ∅((z)P )[x6=y]def=(z)P [x6=y] where z 6∈ {x, y}(P +Q)[x6=y]def=

P [x6=y] +Q[x6=y]([u=v]P )[x6=y]def=[u=v]P [x6=y]([u6=v]P )[x6=y]def[u6=v]P [x6=y](π.P )=

When constructing P [x6=y] one must rename the bound names of P to prevent x, y from being captured.
The following lemma records a simple fact about this operation. It says that the presence of a mismatch
operator is irrelevant from an operational point of view if the names involved are free and distinct.
Lemma 39. Suppose bn(λ) ∩ {x, y} = ∅ and x, y are distinct names. Then the following properties hold:λλ(i) If P −→ P 0 and x 6= y then P [x6=y] −→ (P 0 )[x6=y] .
λλ(ii) If P [x6=y] −→ P 00 then P 0 exists such that P −→ P 0 and P 00 ≡ (P 0 )[x6=y] .
For Y = {y1 , . . . , yn }, let P [x6∈Y ] denote (. . . (P [x6=y1 ] )[x6=y2 ] . . .)[x6=yn ] . When this notation is used theorder of applying the operations ( )[x6=y1 ] , . . . , ( )[x6=yn ] is definitely not important.
It should be easy to see that the operation ( )[x6=y] is to make distinctions syntactically explicit.

4.1

Bisimulation Theory of the Full Calculus

The stability of the operational semantics simplifies the theory of the bisimulation equivalence because
it allows one to define bisimilarities that enjoy the following property:
λ

b
λ

λσ

c
λσ

If P −→ P 0 is simulated by Q =⇒ Q0 then P σ −→ P 0 σ is simulated by Qσ =⇒ Q0 σ.

22This property holds for the open bisimilarities of the calculi studied in the previous two sections. If
stability fails, the above property is too strong to be of practical interest. In this case the best one couldbλλ

expect, even though we know that Q =⇒ Q0 simulates P −→ P 0 , is that for each substitution σ some
c
λσ

λσ

Q1 exists such that Qσ =⇒ Q1 simulates P σ −→ P 0 σ provided that P σ can perform the action λσ.
It is therefore natural to anticipate that the bisimulation theory without the stability property is quite
different from what we have seen in the previous two sections.
The full π-calculus fails to hold of the stability property. The algebraic investigation we have carriedout for the π-calculus without the mismatch operator needs to be redone, starting from the very definitionsof bisimulations.
4.1.1

Late and Early Equivalences

It is well-known ([32]) that there are two versions of strong bisimilarity, late and early bisimilarities.
They differ in the treatment of input actions. The early approach regards input as an action that receives
a name at the same time the action happens whereas the late one thinks of input as a commitment ofan action that is to pick up a name before the next observable action occurs. The latter reminds one ofasynchronous communication. It is a rather intentional interpretation of the operational semantics. The
late bisimilarity is strictly stronger than the early one whether the model has mismatch operator or not.
Let’s review the definitions of the strong early equivalence and the strong late equivalence.
Definition 40. Suppose R is a symmetric binary relation on the set of processes. The relation R is astrong late bisimulation if whenever P RQ then the following property holds:λλ(i) If λ is not an input action and P −→ P 0 then some Q0 exists such that Q −→ Q0 RP 0 .
a(x)

a(x)

(ii) If P −→ P 0 then some Q0 exists such that Q −→ Q0 and, for every y, Q0 [y/x]RP 0 [y/x].
The strong late bisimilarity ∼˙ l is the largest strong late bisimulation. Two processes P and Q are strongly
late equivalent, notation P ∼l Q, if P σ ∼˙ l Qσ for every substitution σ.
Definition 41. Suppose R is a symmetric binary relation on the set of processes. The relation R is astrong early bisimulation if whenever P RQ then the following property holds:λλ(i) If λ is not an input action and P −→ P 0 then some Q0 exists such that Q −→ Q0 RP 0 .
a(x)

a(x)

(ii) If P −→ P 0 then, for every y, some Q0 exists such that Q −→ Q0 and Q0 [y/x]RP 0 [y/x].
The strong early bisimilarity ∼˙ e is the largest strong early bisimulation. Two processes P and Q arestrongly early equivalent, notation P ∼e Q, if P σ ∼˙ e Qσ for every substitution σ.
It is easily seen that ∼l is strictly contained in ∼e . The following is an example exhibiting thedifference: One hasa(x).R+a(x)+a(x).[x=y]R ∼e a(x).R+a(x)but nota(x).R+a(x)+a(x).[x=y]R ∼l a(x).R+a(x)Using the mismatch operator a more general counter example can be given: It is clear thata(x).P +a(x).Q+a(x).([x=y]P +[x6=y]Q) ∼e a(x).P +a(x).Q
but nota(x).P +a(x).Q+a(x).([x=y]P +[x6=y]Q) ∼l a(x).P +a(x).Q
As a matter of fact this counter example is so general that it characterizes the difference between earlyand late equivalences.
An interesting equality that holds for both the strong early equivalence and the strong late equivalenceis the followingC[[x=y]P ]+C[0] ∼l [x=y]C[P ]+C[0]where both x and y are free in C[[x=y]P ]. If a substitution σ identifies x and y then C[[x=y]P ]σ can be
simulated by ([x=y]C[P ])σ, otherwise it can be simulated by C[0]σ.
Next we define the corresponding weak equivalences.

23

Definition 42. Suppose R is a symmetric binary relation on the set of processes. The relation R is aweak late bisimulation if whenever P RQ then the following property holds:λbλ(i) If λ is not an input prefix and P −→ P 0 then some Q0 exists such that Q =⇒ Q0 RP 0 .
a(x)

a(x)

(ii) If P −→ P 0 then some Q0 exists such that Q =⇒−→ Q0 and for every y some Q00 exists such thatQ0 [y/x]=⇒Q00 RP 0 [y/x].
˙ lw is the largest weak late bisimulation. Two processes P and Q are weakly
The weak late bisimilarity ≈˙ lw Qσ for every substitution σ.
late equivalent, notation P ≈lw Q, if P σ ≈0

˙ lw be the alternative of ≈˙ lw defined by replacing the clause (ii) by the following requirement
Let ≈
a(x)

a(x)

(ii’) If P −→ P 0 then some Q0 exists such that Q =⇒ Q0 and Q0 [y/x]RP 0 [y/x] for every y.
0

˙ lw is not even an equivalence relation. The following counter example is taken
It is well-known that ≈from [42]. Let α be different from τ and define:
P1
P2
P3

def

=

def

=

def

=

c(a).[a=b]α+c(a).(τ.[a=b]α+τ.α+τ )c(a).(τ.[a=b]α+τ.α+τ )c(a).(τ.α+τ )0

˙ l P3 . On the other hand, P1 ≈˙ lw P2 ≈˙ lw P3 but P1 6≈
˙ lw P2 ≈˙ lw P3 and P1 ≈˙ lw P3 .
Then P1 ≈w
0

0

Definition 43. Suppose R is a symmetric binary relation on the set of processes. The relation R is aweak early bisimulation if whenever P RQ then the following property holds:λbλ(i) If λ is not an input action and P −→ P 0 then some Q0 exists such that Q =⇒ Q0 RP 0 .
a(x)

a(x)

(ii) If P −→ P 0 then for every y some Q0 and Q00 exist such that Q =⇒−→ Q00 and Q00 [y/x]=⇒Q0 RP 0 [y/x].
˙ ew is the largest weak early bisimulation. Two processes P and Q are weakly
The weak early bisimilarity ≈˙ ew Qσ for every substitution σ.
early equivalent, notation P ≈ew Q, if P σ ≈˙ stands
The next two lemmas appeared in [37], in which ≈ stands for either ≈ew or ≈lw , and similarly ≈˙ ew or ≈˙ lw .
for either ≈˙ if and only if P σ ≈Qσ.
˙
Lemma 44. Suppose that σ is injective on f n(P +Q). Then P ≈Q
˙
Lemma 45. Suppose ψ is complete on V ⊇ f n(P +Q) and σ agrees with ψ. Then ψP σ ≈ψQσ
if and˙˙only if ψP ≈ψQ
if and only if (ψP )σ ≈(ψQ)σ
if and only if ψP ≈ ψQ.
˙
Proof. By Lemma 44 we may assume that σ is induced by ψ. It follows easily from [x=y]P ≈[x=y]P
[y/x]
˙
˙
˙
that ψP σ ≈ψQσ
if and only if ψP ≈ψQ.
Now σ is injective on f n(P σ+Qσ). So (ψP σ)σ ≈(ψQσ)σby˙
Lemma 44. Therefore (ψP )σ ≈(ψQ)σ.
Consequently ψP ≈ ψQ.
4.1.2

Strong Open Bisimilarity

The strong open bisimilarity introduced by Sangiorgi makes use of distinctions, whose role is to record
names that should be kept distinct from each other in two relevant simulating processes. Distinctions
formalize the fact that, in π-calculus, a local name in a process is never identified with any other nameduring the evolution of the process. In this paper we show that the distinctions are not necessary in
the presence of the mismatch operator. To start with we show how this can be achieved for strong open
bisimilarity.
Definition 46. Suppose R is a symmetric binary relation on the set of processes. The relation R is astrong open bisimulation if whenever P RQ then the following properties hold for every substitution σ:λλ(i) If P σ −→ P 0 , where λ is not a restricted output action, then some Q0 exists such that Qσ −→ Q0 RP 0 .
a(x)

a(x)

(ii) If P σ −→ P 0 and x 6∈ f n(Q) then some Q0 exists such that Qσ −→ Q0 and (P 0 )[x6∈Y ] R(Q0 )[x6∈Y ] ,where Y is f n(P 0 +Q0 ) \ {x}.
The strong open bisimilarity ∼o is the largest strong open bisimulation.

24

Intuitively a restricted name is kept distinct from any other name by inserting enough mismatch
operators in front of all occurrences of prefix. This is necessary because names can be instantiated atevery bisimulation step in the open semantics. It should be pointed out that in the above definition
0

0

0

0

(P 0 )[x6∈(f n(P +Q )\{x})] R(Q0 )[x6∈(f n(P +Q )\{x})]00should not be replaced by (P 0 )[x6∈(f n(P )\{x})] R(Q0 )[x6∈(f n(Q )\{x})] . Otherwise it would result in a bad
equivalence relation. But for the above definition it is not obvious that ∼o is an equivalence relation. We
are not going to prove this fact here since we will establish the equivalence property for the weak open
bisimilarities.
We have also overloaded the notation ∼o . Some clarification is called for. In what follows we showthat the two definitions of ∼o are consistent. We need two auxiliary lemmas whose proofs we omit, thefirst of which is due to Sangiorgi ([42]).
Lemma 47. Suppose P and Q are processes in the π-calculus without the mismatch operator, D is aDσdistinction and σ is a substitution. If P ∼DQσ.
o Q and σ respects D then P σ ∼oD\xLemma 48. Suppose D is a distinction. If P ∼Do Q and x 6∈ f n(P +Q) then P ∼o

Q.

In order to get our result, we prove a more general result.
Theorem 49. Suppose P and Q are processes in the π-calculus without the mismatch and the distinctionδδ
D agrees with the substitution δ. Then P ∼Do Q if and only if P ∼o Q .
Proof. (i) Let R be {(P δ , Qδ ) | P ∼Do Q and D agrees with δ for distinction D and substitution σ}∪ ∼o .
We prove that R is a strong open bisimulation in the sense of Definition 21. First of all we need to showthat R is closed under substitution. Now suppose P δ RQδ , that is P ∼Do Q and D agrees with δ. If σ
respects δ then σ respects D, therefore P σ ∼Dσ
Qσ
by
Lemma
47,
and
consequently(P σ)δσ R(Qσ)δσ . Ifoδδσ does not respect δ then (P )σ ∼o 0 ∼o (Q )σ.
λδ
00
Now suppose that P ∼Do Q and that D agrees with δ. If P −→ P then, by Lemma 39, one has
λP −→ P 0 and P 00 ≡ P 0δ . There are two cases:
λ

0
D
0
0
• λ is not a restricted output action. It follows from P ∼Do Q that Q −→ Q ∼o P for some Q . By
λLemma 39, Qδ −→ Q0δ RP 0δ .
a(x)

0

0
D
0
0
• λ is a restricted output action a(x). It follows from P ∼Do Q that Q −→ Q ∼o P , where D isa(x)D ∪ {x}×f n(P +Q). Clearly Qδ −→ Q0δ and D0 agrees with δ[x6∈f n(P +Q)]. It is also clear that00
00
f n(P 0 +Q0 ) \ {x} ⊆ f n(P +Q). By Lemma 48, P 0 ∼D
P 0 ∼D
Q0 where D00 is a distinco Q implies
o
0
0
0
0
0
0
0δ[x6∈(f n(P +Q )\{x})]tion that agrees with δ[x6∈(f n(P + Q ) \ {x})]. So P
RQ0δ[x6∈(f n(P +Q )\{x})] .
δδSo R is a strong open bisimulation in the sense of Definition 21. Thus P ∼Do Q implies P ∼o Q .
δδD(ii) The proof that P ∼o Q implies P ∼o Q, where D agrees with δ, is similar to (i). For a
distinction D, let RD be {(P, Q) | P δ ∼o Qδ , δ agrees with D} and let R be {RD }D∈D . It can beproved that R is a strong open bisimulation, in the sense of Definition 46, for the π-calculus without themismatch operator.

Corollary 50. P ∼∅o Q if and only if P ∼o Q for P, Q that do not contain any mismatch operator.
Therefore ∼o of the full π-calculus is a conservative extension of ∼∅o , which by Lemma 31 is a conservative extension of ∼o of the calculus of nondeterministic mobile processes. So the confusions areharmless.
4.1.3

Weak Open Bisimilarities

In the presence of the mismatch operator there are at least three weak versions of open bisimilarity. In
what follows we examine each of the weak open bisimilarity in turn. We first take a look at the mostloose weak open congruence. It is an obvious generalization of the strong open bisimilarity. This is akinto Sangiorgi’s version of weak open congruence he introduced for mobile processes without the mismatch
operator.

25

Definition 51. Suppose R is a symmetric binary relation on the set of processes. The relation R is aweak open bisimulation if whenever P RQ then the following properties hold for every substitution σ:λbλ(i) If P σ −→ P 0 , where λ is not a restricted output action, then some Q0 exists such that Qσ =⇒ Q0 RP 0 .
a(x)

a(x)

(ii) If P σ −→ P 0 and x 6∈ f n(Q) then some Q0 exists such that Qσ =⇒ Q0 and (P 0 )[x6∈Y ] R(Q0 )[x6∈Y ] ,where Y is f n(P 0 +Q0 ) \ {x}.
The weak open bisimilarity ≈wo is the largest weak open bisimulation.
Weak open bisimilarity is a very loose equivalence relation. This can be seen from the following
example:a(x).[x6=y]τ.P +a(x).P ≈wo a(x).[x6=y]τ.Pa(x)a(x) τ

The action a(x).[x6=y]τ.P + a(x).P −→ P is simulated by a(x).[x6=y]τ.P −→−→ P . The equivalenceis reasonable in the absence of the parallel operator. But the combination of the mismatch and thecomposition would render anomalous the weak open bisimilarity. For instance the above equivalence
does not imply the following(a(x).[x6=y]τ.P +a(x).P )|ay ≈wo (a(x).[x6=y]τ.P )|ayτThe action (a(x).[x6=y]τ.P +a(x).P )|ay −→ P [y/x]|0 can not be matched up by any action from theprocess (a(x).[x6=y]τ.P )|ay. In our view (a(x).[x6=y]τ.P +a(x).P )|ay and (a(x).[x6=y]τ.P )|ay should not
be identified by any reasonable bisimulation equivalence.
The anomaly is caused by the delay of instantiation of input actions, which would not have been agreat problem in the absence of the mismatch operator. With the mismatch operator around it seems
better to let the instantiation happen immediately. For that purpose we introduce below two versions ofrefinement of the weak open bisimilarity. The first one is the late open bisimilarity.
Definition 52. Suppose R is a symmetric binary relation on the set of processes. The relation R is alate open bisimulation if whenever P RQ then the following properties hold for every substitution σ:λ(i) If P σ −→ P 0 , where λ is neither a restricted output action nor an input action, then some Q0 existsb
λsuch that Qσ =⇒ Q0 RP 0 .
a(x)

a(x)

(ii) If P σ −→ P 0 then some Q0 exists such that Qσ =⇒−→ Q0 , and for each y, some Q00 exists such thatQ0 [y/x]=⇒Q00 RP 0 [y/x].
a(x)

a(x)

(iii) If P σ −→ P 0 and x 6∈ f n(Q) then some Q0 exists such that Qσ =⇒ Q0 and (P 0 )[x6∈Y ] R(Q0 )[x6∈Y ] ,where Y is f n(P 0 +Q0 ) \ {x}.
The late open bisimilarity ≈lo is the largest late open bisimulation.
The third open bisimilarity we consider is the early open bisimilarity. The difference between the late
open bisimilarity and the early open bisimilarity is in analogy to that between the weak late bisimilarity
and the weak early bisimilarity.
Definition 53. Suppose R is a symmetric binary relation on the set of processes. The relation R is anearly open bisimulation if whenever P RQ then the following properties hold for every substitution σ:λ(i) If P σ −→ P 0 , where λ is neither a restricted output action nor an input action, then some Q0 existsb
λsuch that Qσ =⇒ Q0 RP 0 .
a(x)

a(x)

(ii) If P σ −→ P 0 then for every y some Q0 and Q00 exists such that Qσ =⇒−→ Q00 and Q00 [y/x] =⇒Q0 RP 0 [y/x].
a(x)

a(x)

(iii) If P σ −→ P 0 and x 6∈ f n(Q) then some Q0 exists such that Qσ =⇒ Q0 and (P 0 )[x6∈Y ] R(Q0 )[x6∈Y ] ,where Y is (f n(P 0 +Q0 ) \ {x}).
The early open bisimilarity ≈eo is the largest early open bisimulation.
As one would expect the late open bisimilarity is stronger than the early open bisimilarity. The next
lemma summarizes the relationship among the three open bisimilarities.
Lemma 54. ≈lo ⊂≈eo ⊂≈w
o and the inclusions are strict.

26

Proof. The first inclusion is by definition. Here is a counter example that justifies the strictness of the
inclusion:a(x).[x6=y]τ.P +a(x).[x=y]τ.P ≈eo a(x).[x6=y]τ.P +a(x).[x=y]τ.P +a(x).P
but
a(x).[x6=y]τ.P +a(x).[x=y]τ.P 6≈lo a(x).[x6=y]τ.P +a(x).[x=y]τ.P +a(x).P
a(x)

a(x)

Suppose P ≈eo Q and P −→ P 0 . Then some Q00 and Q0 exist such that Q =⇒−→ Q00 and Q00 =⇒ Q0 ≈eo P 0 .
a(x)That is Q =⇒ Q0 ≈eo P 0 . Hence P ≈w
o Q. The strictness of the second inclusion is verified by the following
counter example:a(x).[x6=y]τ.P ≈wo a(x).[x6=y]τ.P + a(x).P
but
a(x).[x6=y]τ.P 6≈eo a(x).[x6=y]τ.P + a(x).PThis completes the proof.
4.1.4

Weak Open Bisimilarities are Equivalence Relations

The open bisimilarities are by definition closed under substitution. It is however not obvious that they
are equivalence relations. The next lemma, whose proof can be found in Appendix A.1, is the crux ofthe equivalence proof. It says that the presence or absence of a mismatch operator does not affect thealgebraic equality of two processes if the relevant names are distinct and not both of them appear in theprocesses.
Lemma 55. The following properties hold for ≈o :(i) If P ≈lo Q then P [x6=y] ≈lo Q[x6=y] .
(ii) If P [x6=y] ≈lo Q[x6=y] and {x, y} 6⊆ f n(P +Q) then P ≈lo Q.
(i) and (ii) also hold for ≈eo and ≈w
o.
Now we are ready to show that the weak open bisimilarities are equivalence relations.
Lemma 56. ≈lo , ≈eo and ≈wo are all equivalence relations.
Proof. We prove transitivity and consider only input and restricted output actions. Suppose P ≈lo Q
a(x)

a(x)

and Q ≈lo R. If P −→ P 0 then some Q0 and Q00 exist such that Q =⇒−→ Q00 and, for every y,a(x)Q00 [y/x] =⇒ Q0 ≈lo P 0 [y/x]. As Q ≈lo R, we have R00 and R000 such that R =⇒−→ R00 and, forevery y, R00 [y/x] =⇒ R000 ≈lo Q00 [y/x]. Consequently R000 =⇒ R0 ≈lo Q0 ≈lo P 0 [y/x] for some R0 .
a(x)

a(x)

a(x)

Now suppose P −→ P 0 . Then by definition Q =⇒ Q0 and R =⇒ R0 for some Q0 and R0 such that
0
0
0
0
0
0
0
0
(P 0 )[x6∈(f n(P +Q )\{x})] ≈lo (Q0 )[x6∈(f n(P +Q )\{x})] and (Q0 )[x6∈(f n(R +Q )\{x})] ≈lo (R0 )[x6∈(f n(R +Q )\{x})] .
By (i) of Lemma 55 one gets
0

0

0

0

0

0

0

0

0

(P 0 )[x6∈(f n(P +Q +R )\{x})] ≈lo (Q0 )[x6∈(f n(P +Q +R )\{x})] ≈lo (R0 )[x6∈(f n(P +Q +R )\{x})]
0

0

0

0

It follows from (ii) of Lemma 55 that (P 0 )[x6∈(f n(P +R )\{x})] ≈lo (R0 )[x6∈(f n(P +R )\{x})] .
The proofs of the other two equivalence relations are the same.
It is easily checked that Lemma 47 and Lemma 48 also hold for ≈D
o . This fact is used in the proof of
the following theorem.
∅
Theorem 57. The three relations ≈lo , ≈eo and ≈wo coincide with ≈o on the set of π-processes without themismatch operator.
λλσ

Proof. The π-calculus without the mismatch operator enjoys the property that if P −→ P 0 then P σ −→P 0 σ for each substitution σ. By definition ≈eo , ≈lo and ≈wo are closed under substitution. It is then easy
to see that the three relations coincide with each other on the set of π-processes without the mismatch
operator since it does not matter which instantiation scheme we use. We only have to show that ≈wo alsocoincides with ≈o when restricted to these processes. Notice that ≈wo is closed under parallel composition
for processes without the mismatch operator.

27

'w
o
6

'e
* wH

Y

H

6 HH
e
'o
∼e
'lw
6
6
*

Y
H

H

H
H ∼l
'lo 
YH
H
*

H

H ∼o

Figure 12: The Order Structure of the Eight Congruence Relationsw(i) Let R be {(P δ , Qδ ) | P ≈Do Q for some D such that D agrees with δ}∪ ≈o . We prove that R
w
is a weak open bisimulation up to ≈o on the set of π-processes without the mismatch. First we showthat R is closed under substitution. Suppose P δ RQδ . If σ agrees with δ, it agrees with D as well. By
Lemma 47, we have that P σ ≈DσQσ. So (P σ)δσ R(Qσ)δσ . Otherwise σ does not agree with δ, in which
o
λ

00
w
δ
δ
δ
case (P δ )σ ≈w
o 0 ≈o (Q )σ. Now consider the actions of P . If P −→ P then, by Lemma 39, we have
λP −→ P 0 and P 00 ≡ P 0δ . There are two cases:
b
λ

0
D
0
• If λ is not a restricted output action then it follows from P ≈Do Q that Q =⇒ Q ≈o P for somebλQ0 and, by Lemma 39, Qδ =⇒ Q0δ RP 0δ .
a(x)

0
0
• If λ is a restricted output action a(x) then it follows from P ≈Do Q that Q =⇒ Q ≈D 0 P ,
a(x)

0

0
where D0 is D ∪ {x}×f n(P +Q). Therefore Qδ =⇒ Q0δ . Using the facts that P 0 ≈Do Q and that
00
0
00
0
(f n(P 0 +Q0 ) \ {x}) ⊆ f n(P +Q), one obtains that P 0 ≈D
Q
where
D
is
D
∪
{x}×(fn(P+Q0 ) \o{x}) ∪ (f n(P 0 +Q0 ) \ {x})×{x}. Since D00 agrees with δ[x6∈(f n(P 0 +Q0 ) \ {x})], one gets that0000
P 0δ[x6∈(f n(P +Q )\{x})] RQ0δ[x6∈(f n(P +Q )\{x})] .

If we let D be the empty set then P ≈o Q implies P ≈w
o Q for P and Q without the mismatch operator.
∅(ii) Now we show that ≈w
⊆≈
.
The
proof
is
similarto (i). For a distinction D, define RD to beooδ{(P, Q) | P δ ≈w
o Q , D agrees with δ}and let R be {RD }D∈D . Then R is a weak open bisimulation in the π-calculus without the mismatch∅
operator. By letting D be the empty set one gets that P ≈w
o Q implies P ≈o Q.
This finishes the proof.
4.1.5

Weak Congruence Revisited

It is clear that ≈eo is not a congruence relation. It is preserved neither by the summation operator nor
by the mismatch operator. For instance[x6=y]aa 6≈eo [x6=y]τ.aa
This is because the right hand can perform a tau action and become aa. But aa is not early open bisimilar
to [x6=y]aa. The same can be said about the other two weak open bisimilarities. We will write 'lw and˙ lw and ≈˙ ew in the manner of Definition 4.
'ew for the congruence relations defined respectively from ≈lew
Similarly we will write 'o , 'o and 'o for the congruence relations defined respectively from ≈lo , ≈eo and≈w
o in the manner of Definition 4.
The inclusion structure of the eight congruence relations is described in Figure 12, where an arrow
indicates a strict inclusion.
For the full π-calculus with the parallel operator one can apply the well-known expansion law totransplant its algebraic theory to that of nondeterministic mobile processes with restricted output. The
only exception is the weak open bisimilarity. However we can redefine the weak open congruence 'w
o as
the largest bisimulation congruence relation contained in ≈w
o . In light of the following proposition thisdoes not give rise to a new congruence.
e
Proposition 58. In the full π-calculus with the parallel composition operator, 'w
o coincides with 'o .

28Proof. The proof of 'eo ⊆'w
o is trivial.
Suppose P 'w
o Q. We now prove that it is an open early bisimulation. We only consider thea(x)case of input action as the rest is easier. Suppose P σ −→ P 0 . Because 'w
o is a congruence relation,τ0
Qσ|ay.bb
for
fresh
names
y
and
b.
Now
P
σ|ay.b−→P[y/x]|bb.
This action must be
P σ|ay.bb 'w
oτmatched up by Qσ|ay.bb =⇒ Q1 |ay.bb −→ Q2 |bb =⇒ Q3 |bb 'w
P[y/x]|bb,
from
which
it is easy to see
o
a(x)

w
that Qσ =⇒ Q1 −→ Q0 , Q0 [y/x] ≡ Q2 =⇒ Q3 and Q3 'w
o P [y/x]. Consequently 'o is an open earlywebisimulation. Conclude that 'o ⊆'o .

In what follows we will refer to ∼ls , ∼es , ≈lw , ≈ew as the ground congruences and ∼so , ≈lo , ∼eo , ≈wo as
the open congruences.

4.2

Laws of the Full Calculus

The laws of the full π-calculus can be divided into three groups: The first group consists of basic laws that
hold for all the eight congruences. In addition to the laws given in Section 3 and Section 4, this group
has laws about the mismatch operator. The second group contains those laws that are valid for somestrong congruence but not all the strong congruences. These laws are particularly interesting. The thirdgroup collects all the tau laws used in this paper. Some of the tau laws are good for all the congruences.
Others only hold for some of the congruences. The relationship among the laws is complex. This section
tries to unveil part of the picture.
4.2.1

Basic Laws

In Figure 13 some basic laws for the full π-calculus are listed, together with all the equivalence andcongruence rules, all of them can be found in [32] or [37]. The laws M4 and M5 deal with the mismatch
operator. The law S5 also involves the mismatch operator. The rest of the laws have already been
seen in Section 3.2. This set of rules and axioms will be referred to as AS. They are sound for all
the observational equalities, for the full π-calculus, that we are aware of. Their intended meanings are
obvious.
The axioms about the mismatch operator in Figure 13 enables us to derive some interesting equalitiesfor π-processes. In Figure 14 some important derived laws are given. The proofs that these laws follow
from AS can be found in [37]. To establish D5 for example, one shows that both (x)[y6=z]P and [y6=z](x)P
are provably equal to [y6=z](x)[y6=z]P , using L6 and S5. Notice that D6 is derived from L7.
In [42] completeness theorem is proved for strong open bisimilarity on π-processes without the mismatch operator. A more streamlined approach is used in previous sections to establish complete result
for weak open congruence of the same language. In the presence of mismatch operator, the methodof [42] and previous sections should be modified. First of all the normal forms of the processes in the full
π-calculus need be redefined.
Definition 59. 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 bn(λi ) ∩ V = ∅, ψi is complete on V and Pi is a complete normal form on V ∪ bn(λi ) for eachi ∈ I.
Let d(P ) be the maximal number of nested prefix operators in P . The definition of d(P ) extends thedef

one given previously by requiring that d([x6=y]P ) = d(P ).
Lemma 60. For a process P and a finite set V of names such that f n(P ) ⊆ V there is a complete
normal form Q on V such that d(Q) ≤ d(P ) and AS ` Q = P .
The proof of the above lemma is by simple induction. Use S5 if necessary to transfer outermost
sequences of match and mismatch operators to complete ones on V .
We now derive some more equalities in AS.
Lemma 61. Suppose that y1 , . . . , yn are pairwise distinct names and Y is the set {y1 , . . . , yn }. ThenAS ` P = [x=y1 ]P + . . . +[x=yn ]P +[x6∈Y ]P .
29

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

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
φ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

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

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
ψP[x=y]P [y/x][x=y]P +[x=y]Q[x6=y]P +[x6=y]Q
0P
Q+P(P +Q)+RPP

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= yif φ ⇔ ψ

Figure 13: AS: Basic Rules and Axioms for the Full Pi Calculus
D1
D2
D3
D4
D5
D6
D7

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

=
=
=
=
=
=
=

P
P
0
0
[y6=z](x)P(x)PP

if x 6∈ {y, z}
if x 6= y
if x 6∈ f n(P )Figure 14: Some Laws Derivable from AS
Proof. First of all notice that the following equality is valid by D1 and S5:
AS ` [x=y]P +[x6=y][x=z]P = [x=y]P +[x=z]P
which can be derived as follows:[x=y]P +[x6=y][x=z]P

D1

=

S5

=

[x=y]P +[x=y][x=z]P +[x6=y][x=z]P[x=y]P +[x=z]P

30

(6)

L8
M6
S6

(x)C[[x=y]P ][x6=y]π.P
a(x).P +a(x).Q===(x)C[0][x6=y]π.[x6=y]P
a(x).P +a(x).Q+a(x).([x=y]P +[x6=y]Q)x, y 6∈ bn(C[]) and x6=y{x, y} ∩ bn(π) = ∅Figure 15: Additional Laws
L8a
L8b
M6a

(x)C[[x6=y]P ](x)P [x6=y]P [x6=y]===(x)C[P ](x)P[x6=y]Px, y 6∈ bn(C[]) and x6=yx 6∈ bn(P ) and x6=yFigure 16: Laws Equivalent to L8 or M6
When n = 1 the lemma is just S5. Suppose the lemma holds for n > 1. ThenAS ` PS5=[x=yn+1 ]P +[x6=yn+1 ]P

I.H.

=

[x=yn+1 ]P +[x6=yn+1 ]([x=y1 ]P + . . . [x=yn ]P +[x6∈Y ]P )M4=

[x=yn+1 ]P +[x6=yn+1 ][x=y1 ]P + . . . +[x6=yn+1 ][x=yn ]P +[x6∈Y 0 ]P

(6)

=
..
.

[x=yn+1 ]P +[x=y1 ]P + . . . +[x6=yn+1 ][x=yn ]P +[x6∈Y 0 ]P

(6)

[x=yn+1 ]P +[x=y1 ]P + . . . +[x=yn ]P +[x6∈Y 0 ]P
[x=y1 ]P + . . . +[x=yn ]P +[x=yn+1 ]P +[x6∈Y 0 ]P==

where Y 0 = {y1 , . . . , yn , yn+1 }.
The following generalization of Lemma 61 is also useful. For a proof of it, see Appendix A.2.
W
P
Lemma 62. If i∈I ψi is a tautology then AS ` i∈I ψi P = P .
The next lemma explains why M5 is necessary.
Lemma 63. If ψ ⇔ ⊥ then AS ` ψP = 0.
Proof. Obviously ψ ⇔ ⊥ if and only if ψ ⇔ x6=x. We are done by using M5.
4.2.2

Additional Laws

All complete systems studied in the rest of the paper extend AS. Each of these systems contains someof the axioms listed in Figure 15. The law S6 was first proposed in [37] and the law M6 was introducedin [32]. Notice that L8 and L1 imply L7.
In Figure 16 some equivalent formulations of L8 and M6 are given. The next lemma establishes theequivalence of L8, L8a and L8b on top of the system AS.
Lemma 64. AS ∪ {L8} ` L8a, AS ∪ {L8a} ` L8b and AS ∪ {L8b} ` L8.
Proof. The following inference shows that AS ∪ {L8} ` L8a:(x)C[P ]

=
L8

=
=

(x)C[[x=y]P +[x6=y]P ](x)C[0+[x6=y]P ](x)C[[x6=y]P ]The fact AS ∪ {L8a} ` L8b is clear. And AS ∪ {L8b} ` L8 is established easily as follows:(x)C[[x=y]P ]

L8b

=
=

L8b

=

where the second equality holds by Lemma 63.
31(x)C[[x=y]P ][x6=y](x)C[0][x6=y](x)C[0]L8 and L8a are formulated in terms of contexts while L8b has the virtue that it does not explicitly
refer to the notion of contexts. On the other hand L8 has the advantage of not using mismatch operator
and therefore is applicable to a wider range of calculi.
The next lemma relates M6 and M6a.
Lemma 65. AS ∪ {M 6} ` M 6a and AS ∪ {M 6a} ` M 6.
Proof. Assume that {x, y} ∩ bn(π) = ∅. Then M6a implies M6 because[x6=y]π.P

M 6a=(π.P )[x6=y]M1(π.[x6=y]P )[x6=y]

=

M 6a

=

[x6=y]π.[x6=y]PThe converse is proved by structural induction.
In view of the above two lemmas, we will use L8 to stand for any of the three laws L8, L8a, L8b andM6 for either of the two laws M6, M6a.
L8 is valid for the strong open bisimilarity whereas M6 holds for the strong early/late bisimilarity. Itshould come as no surprise that the latter implies the former in AS.
Lemma 66. AS ∪ {M 6} ` L8.
M6

D6

Proof. AS ` (x)P [x6=y] = (x)[x6=y]P = (x)P .
The law S6 can not be deduced from the law S5. The latter is valid for all the congruences whereas
the former is invalid for the open congruences.
4.2.3

Tau Laws

In order to extend AS to complete systems for the weak observational congruences of the full π-calculus,
we need the tau laws in Figure 17. There are altogether six tau laws. The first two are familiar. The rest
four need some explanation:• The T3 in Figure 17 is a generalization of the T3 in Figure 7, taking into account of the mismatch
operator. The general T3 is equivalent to the restricted T3 in the presence of M6. But in general theformer strictly subsumes the latter because the equality π.(P +[x6=y]τ.Q) = π.(P +[x6=y]τ.Q) + π.Q,
where bn(π) ∩ {x, y} = ∅, is not implied by the restricted T3.
• The T4 in Figure 17 is a generalization of the T4 in Figure 8, again taking into account of themismatch operator. This law is subsumed by M6.
• T5 is a law valid for the early open congruence. The following is a simple instance of the law:a(x).(P0 +[x=y]τ.Q) + a(x).(P1 +[x6=y]τ.Q) = a(x).(P0 +[x=y]τ.Q) + a(x).(P1 +[x6=y]τ.Q) + a(x).Q
More generally we have the following binary version, as it were, of T5:
a(x).(P0 + ψ0 τ.Q) + a(x).(P1 + ψ1 τ.Q) = a(x).(P0 + ψ0 τ.Q) + a(x).(P1 + ψ1 τ.Q) + ψa(x).Q
where ψ0 ∨ ψ1 ⇔ ψ and x 6∈ n(ψ). This binary law does not seem to imply T5. All our attempts
to simplify the law have failed.
• T6 holds for the weak open congruence. It implies T5. Notice that this law makes sense only in alate operational semantics. It has far less significance than the other five tau laws.
The overloading of the name T3, respectively T4, is not a problem since a same law takes different forms
in different subcalculi.
In Figure 18 some derived laws of T3, T4 and T5 are presented. The joint effect of T3a and T3b isthe same as that of T3. Similarly T4a and T4b together have the same power as T4. T5a is a moremanageable version of T5, which is more useful in practice. It is simpler yet equivalent to T5.
We now formalize some of the above claims in the rest of this section.
32

T1
T2
T3
T4
T5
T6

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

=
=
=
=
=
=

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

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

x 6∈ n(ψ)

Figure 17: Tau Laws for the Full Pi Calculus
T3aax.(P + δτ.Q) = ax.(P + δτ.Q) + δax.Q
T3b a(x).(P + δτ.Q) = a(x).(P + δτ.Q) + δa(x).Q
x 6∈ n(δ)
T4a
τ.P = τ.(P + [x=y]τ.P )T4b
τ.P = τ.(PP
P + δτ.P )
T5a
(a,
P,
Q,
δ)
=
(a, P, Q, δ) + δa(x).Q
x 6∈ n(δ)
PP
In T5a, (a, P, Q, δ) is y∈Y a(x).(Py +δ[x=y]τ.Q)+a(x).(P +δ[x6∈Y ]τ.Q)
Figure 18: Derived Tau Laws
Lemma 67. The following properties hold:(i) AS ∪ {π.(P +τ.Q) = π.(P +τ.Q) + π.Q} ∪ {M 6} ` T 3a.
(ii) AS ∪ {π.(P +τ.Q) = π.(P +τ.Q) + π.Q} ∪ {M 6} ` T 3b.
(iii) AS ∪ {T 1, T 2} ∪ {T 3a, T 3b} ` T 3.
Proof. The proof of (i) can be given as follows:
π.(P +δτ.Q)

=
M6

=
=
=

π.(P +δτ.Q) + δπ.(P +δτ.Q)
π.(P +δτ.Q) + δπ.(P +τ.Q)
π.(P +δτ.Q) + δπ.(P +τ.Q) + δπ.Q
π.(P +δτ.Q) + δπ.Q

The proof of (ii) is similar. For (iii) notice that τ.(P +τ.Q) = τ.(P +τ.Q) + τ.Q follows from T1 and T2.
Hence π.(P +δτ.Q) = π.(P +δτ.Q) + δπ.Q when bn(π) ∩ n(δ) = ∅. Suppose n(ψ) ∩ bn(π) = ∅. By M1 one
may assume that ψ = µδ, where µ is the match part of ψ and δ is the mismatch part of ψ. When µ = []the lemma is just T3a, T3b and T3c. When µ = [x=y]µ0 , thenπ.(P +[x=y]µ0 δτ.Q)

D1=

M 1,M 2[x=y]π.(P +[x=y]µ0 δτ.Q)+π.(P +[x=y]µ0 δτ.Q)=[x=y]π.(P +µ0 δτ.Q)+π.(P +[x=y]µ0 δτ.Q)

I.H.

=

[x=y](π.(P +µ0 δτ.Q)+µ0 δπ.Q)+π.(P +[x=y]µ0 δτ.Q)

M3=[x=y]π.(P +µ0 δτ.Q)+[x=y]µ0 δπ.Q+π.(P +[x=y]µ0 δτ.Q)

D1

π.(P +[x=y]µ0 δτ.Q)+[x=y]µ0 δπ.Q=

This completes the proof.
Lemma 68. The following properties hold:(i) AS ∪ {T 1, T 2} ∪ {M 6} ` T 4.
(ii) AS ∪ {T 4a, T 4b} ` T 4.
Proof. (i) The proof is by induction. The base case is taken care of by T1 and T2. For the inductive step33

observe that
S5

τ.(P +[x=y]ψτ.P )=

M 1,M 2=

M 6,M 4

=
=

M6

=

I.H.

=

S5

=

[x=y]τ.(P +[x=y]ψτ.P )+[x6=y]τ.(P +[x=y]ψτ.P )[x=y]τ.(P +ψτ.P )+[x6=y]τ.(P +[x=y]ψτ.P )[x=y]τ.(P +ψτ.P )+[x6=y]τ.([x6=y]P +[x6=y][x=y]ψτ.P )[x=y]τ.(P +ψτ.P )+[x6=y]τ.[x6=y]P[x=y]τ.(P +ψτ.P )+[x6=y]τ.P[x=y]τ.P +[x6=y]τ.P
τ.Plwhere the fourth equality is by Lemma 63. Similarly one can prove that ASw` τ.P = τ.(P + [x6=y]ψτ.P )lwhenever ASw ` τ.P = τ.(P + ψτ.P ).
(ii) The proof is by induction. By M1 one can suppose that ψ = µδ, where µ is the match part of ψand δ is the mismatch part of ψ. When µ = [] the lemma is simply T4b. When µ = [x=y]µ0 , one has
T 4a

τ.P

=

τ.(P +[x=y]τ.P )

D1=

τ.(P +[x=y]µ0 δτ.P +[x=y]τ.P )

I.H.

=

τ.(P +[x=y]µ0 δτ.P +[x=y]τ.(P +µ0 δτ.P ))M1=

τ.(P +[x=y]µ0 δτ.P +[x=y]τ.(P +[x=y]µ0 δτ.P ))T 4a

τ.(P +[x=y]µ0 δτ.P )=This completes the proof.
The Lemma 66, Lemma 67 and Lemma 68 explain why one hasn’t seen L8, the general T3 andthe general T4 in literature: They are all subsumed by M6. It is when one investigate bisimulation
congruences which fail M6 that one discovers these laws. The next lemma is another example of using
the power of M6, whose proof is placed in Appendix A.3.
Lemma 69. AS ∪ {M 6} ∪ {T 1, T 2, T 3} ` τ.(P +φτ.Q) = τ.(P +τ.(φτ.Q+¬φτ.P )).
Next we discuss properties concerned with T5 and T6. The proof of the next lemma can be found in
Appendix A.4.
Lemma 70. In AS ∪ {T 1, T 2, T 3} the law T5X
Xa(x).(Pi +ψi τ.Q) =a(x).(Pi +ψi τ.Q) + ψa(x).Q
i∈I

i∈I

is equivalent to the law T5akXa(x).(Pi +δ[x=yi ]τ.Q)+a(x).(P +δ[x6∈Y ]τ.Q)

i=1

=

k
X

a(x).(Pi +δ[x=yi ]τ.Q)+a(x).(P +δ[x6∈Y ]τ.Q)+δa(x).Q

i=1

In the above two equalities,

Wi∈I ψi ⇔ ψ, x 6∈ n(ψ), k ≥ 1, Y

= {y1 , y2 , . . . , yk } and x 6∈ n(δ).

The next lemma says that T6 is stronger than T5.
Lemma 71. AS ∪ {T 1, T 2, T 3} ∪ {T 6} ` T 5.
Proof. It is easily seen that T6 implies T5a. We are done by using Lemma 70.
Lemma 72. Let ψ be a set of mismatch and match operators none of which contains x, δ is a set ofmismatch operators each of which contains x. Then AS ∪ {T 1, T 2, T 3} ∪ {T 6} ` a(x).(P + ψδτ.Q) =a(x).(P + ψδτ.Q) + ψa(x).Q.
34

System
ASsl
ASse
l
ASw
e
ASw
ASos
ASol
ASoe
ASow

Axioms in Addition to AS
M6
M6,S6
M6
T1,T2,T3
M6,S6 T1,T2,T3
L8
L8
T1,T2,T3,T4
L8
T1,T2,T3,T4,T5
L8
T1,T2,T3,T4,T6

Congruencestrong late equivalencestrong early equivalence
weak late congruence
weak early congruencestrong open bisimilarity
late open congruence
early open congruence
weak open congruence

Figure 19: Systems for the Full Pi Calculus
Proof. Using induction on the numbers of match/mismatch operators in ψ, the proof is similar to thatof Lemma 67.
We have seen that S6 is the only law that separates the early congruence and the late congruence. We
will see that T5 is the only law that distinguishes the early open congruence and the late open congruence.
One would be interested to know the relationship between the two if there is any. The next lemma seems
to be the best one can expect in view of the fact that S6 is not valid for the early open congruence.
Lemma 73. AS ∪ {T 1, T 2, T 3} ∪ {S6} ` T 5.
The proof of the above lemma is in Appendix A.5.

4.3

Completeness Results for the Full Calculus

Finally we come to the point where we can prove the completeness results for the full calculus. In Figure 19
eight systems are defined, where each system on the left column is obtained from the system AS by adding
the axioms in the corresponding middle columns, with the corresponding congruence relation indicatedeon the right column. For instance ASw, the system for the weak early congruence, is defined to be thesystem AS ∪ {M 6, S6} ∪ {T 1, T 2, T 3}.
By simply looking at Figure 19, one gets two obvious yet important messages:• When moving from the systems for the ground congruences to the systems for the open congruences,
M6 must be weakened to L8.
• When moving from the systems for the weak ground congruences to the systems for the weak open
congruences, T4 must be added.
The thing we do not understand very well at the moment is what happens when moving from the systems
for the late congruences to the systems for the early congruences. We will come back to it later.
In the next three subsections we will follow the standard approach to establish the completenessresults of the eight systems.
4.3.1

Saturation Property

Saturation properties are about the relationship between operational semantics and axiomatic systems.
λA general statement goes like this: If Qσ =⇒ Q0 then AS 0 ` Q = Q+ψλ.Q0 for the system AS 0 ofinterest. In the π-calculus without the mismatch operator, ψ must satisfy the condition that σ(x) = σ(y)whenever ψ ⇒ x=y. In the presence of the mismatch operator a stronger relationship between σ and ψ
is called for.
The first lemma deals with the saturation properties enjoyed by all the systems of the full π-calculus.
Lemma 74. Suppose Q is a complete normal form on some V ⊇ f n(Q), ψ is complete on V , and σ isa substitution that is induced by ψ. Then the following properties hold:τ(i) If Qσ =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + ψτ.Q0 .
ax(ii) If Qσ =⇒ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + ψax.Q0 .

35

a(x)

(iii) If Qσ =⇒−→ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + ψa(x).Q0 .
a(x)(iv) If Qσ =⇒−→ Q0 then AS ∪ {T 1, T 2, T 3} ` Q = Q + ψa(x).Q0 .
τ

τ

a(x)

Proof. To give a flavor of the proof, we take a look at a special instance of (iii). Suppose Qσ −→−→−→ Q0 .
τ

τ

a(x)

By Lemma 34, we may assume that Qσ −→ Q1 σ −→ Q2 σ −→ Q0 ≡ Q3 σ. As Q is a complete normal
form, there must be some summand φτ.Q1 of Q such that ψ ⇒ φ. By definition φ is complete on V . Soφ ⇔ ψ by Lemma 38. It follows that
M1

M2

AS ∪ {T 1, T 2, T 3} ` Q = Q + ψτ.Q1 = Q + ψτ.Q1 στSimilarly it follows from Q1 σ −→ Q2 σ thatAS ∪ {T 1, T 2, T 3} ` Q1 = Q1 + ψτ.Q2 = Q1 + ψτ.Q2 σa(x)For the same reason, Q2 σ −→ Q0 implies thatAS ∪ {T 1, T 2, T 3} ` Q2 = Q2 + ψa(x).Q0
Putting all these together one has
AS ∪ {T 1, T 2, T 3} ` Q

=
=
T2

=

M 3,M 4

=

M1

=
=
=

Q + ψτ.Q1
Q + ψτ.(Q1 + ψτ.Q2 )Q + ψ(τ.(Q1 + ψτ.Q2 ) + (Q1 + ψτ.Q2 ))Q + ψψτ.Q2
Q + ψτ.Q2
Q + ψτ.(Q2 + ψa(x).Q0 )Q + ψa(x).Q0

This treatment of a special case should be enough to convey the general idea of the proof.
The ψ appeared in the above lemma must be complete on V. Otherwise the lemma would be false.
Here is a counter example: One hasτ([x=y][x6=z]τ.P )[y/x] −→ P
but notAS ∪ {T 1, T 2, T 3} ` [x=y][x6=z]τ.P = [x=y][x6=z]τ.P +[x=y]τ.PτThe action ([x=y][x6=z]τ.P +[x=y]τ.P )[y/x, y/z] −→ P [y/x, y/z] can not be matched up by any tau
action from ([x=y][x6=z]τ.P )[y/x, y/z].
Lemma 75. Suppose Q is a complete normal form on some V ⊇ f n(Q), ψ is complete on V , and σ is aa(x)lsubstitution induced by ψ. If Q =⇒ Q0 then the equality Q = Q + ψa(x).Q0 is provable in ASw
and ASol .
a(x)τProof. Suppose Qσ =⇒−→ Q00 σ =⇒ Q0 . By Lemma 74, AS ∪ {T 1, T 2, T 3} ` Q = Q + ψa(x).Q00 . It isclear 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 3a} ` Q00 = Q00 + [x6∈V ]ψτ.Q036

ThereforeQ==

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

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

Q + ψa(x).(Q00 + ψτ.Q0 )[x6∈V ]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==

The use L8 is justified by Lemma 66.
Corollary 76. Suppose Q is a complete normal form on some V ⊇ f n(Q), ψ is complete on V , and σa(x)eis a substitution induced by ψ. If Q =⇒ Q0 then the equality Q = Q + ψa(x).Q0 is provable in ASw, ASoew
and ASo .

It remains to show the saturation property for input actions. This will be stated in the next fourlemmas, three of which are proved in Appendix A.6, Appendix A.7 and Appendix A.8 respectively.
Lemma 77. Suppose Q is a complete normal form on some V = {y1 , . . . , yk } ⊇ f n(Q), ψ is completeon V , and σ is a substitution that is induced by ψ. Then the following saturation properties hold: Ifa(x)Qσ=⇒ −→ Q0 σ,
Q0 σ[y1 /x] =⇒ Q1 ,Q0 σ[y2 /x] =⇒ Q2 ,..
.
Q0 σ[yk /x] =⇒ Qk ,Q0 σ =⇒ Qk+1
then Q = Q + ψa(x).(τ.Q0 + ψPk

j=1 [x=yj ]τ.Qj + ψ[x6∈V ]τ.Qk+1 )) is provable in AS ∪ {T 1, T 2, T 3}.

Lemma 78. Suppose Q is a complete normal form on some V = {y1 , . . . , yk } ⊇ f n(Q), ψ is completeon V , and σ is a substitution that is induced by ψ. Ifa(x)Qσ=⇒ −→ Q01 σ, Q01 σ[y1 /x] =⇒ Q1 ,a(x)Qσ=⇒ −→ Q02 σ, Q02 σ[y2 /x] =⇒ Q2 ,
..
.
a(x)

Qσ=⇒ −→ Q0k σ, Q0k σ[yk /x] =⇒ Qk ,a(x)Qσ =⇒−→ Q0k+1 σ =⇒ Qk+1
Pkthen Q + ψ j=1 a(x).(τ.Q0j +ψ[x=yj ]τ.Qj )+ψa(x).(τ.Q0k+1 +ψ[x6∈V ]τ.Qk+1 )) is provably equal to Q in
AS ∪ {T 1, T 2, T 3}.
Proof. The proof is almost the same as that of Lemma 77.
Lemma 79. Suppose Q is a complete normal form on some V = {y1 , . . . , yk } ⊇ f n(Q), ψ is completeon V , and σ is a substitution that is induced by ψ. Ifa(x)Qσ=⇒ −→ Q01 σ, Q01 σ[y1 /x] =⇒ Q1 ,a(x)Qσ=⇒ −→ Q02 σ, Q02 σ[y2 /x] =⇒ Q2 ,
..
.
a(x)

Qσ=⇒ −→ Q0k σ, Q0k σ[yk /x] =⇒ Qk ,a(x)Qσ =⇒−→ Q0k+1 σ =⇒ Qk+1
37ethen ASw` Q = Q + ψa(x).([x=y1 ]τ.Q1 + . . . + [x6=y1 ] . . . [x6=yk−1 ][x=yk ]τ.Qk + [x6∈V ]τ.Qk+1 ).

Lemma 80. Suppose Q is a complete normal form on some V = {y1 , . . . , yk } ⊇ f n(Q), ψ is completea(x)on V , and σ is a substitution that is induced by ψ. If Qσ =⇒ Q0 then ASow ` Q = Q + ψa(x).Q0 .
4.3.2

Promotion Lemma

As has been said before, the basic idea of promotion lemmas is to lift two bisimulation congruent processes
P and Q to the equality τ.P = τ.Q in sufficiently rich systems. In this section we establish promotion
properties for the five weak congruences in the full π-calculus. These properties are stated in a single
lemma since their proofs have a great deal of overlap.
Lemma 81 (promotion). The following properties hold:l(i) If P ≈lw Q then ASw` τ.P = τ.Q.
ee(ii) If P ≈w Q then ASw` τ.P = τ.Q.
(iii) If P ≈lo Q then ASol ` τ.P = τ.Q.
(iv) If P ≈eo Q then ASoe ` τ.P = τ.Q.
w(v) If P ≈w
o Q then ASo ` τ.P = τ.Q.
The proof of the above lemma is placed in Appendix A.9.
4.3.3

Completeness Theorem

We now arrive at the most important theorem of this paper. For the benefit of the readers, we also state
below the completeness results for the strong early congruence and the strong late congruence.
Theorem 82 (completeness). The following properties hold:(i) ASsl is sound and complete for ∼l .
(ii) ASse is sound and complete for ∼e .
l(iii) ASw
is sound and complete for 'lw .
e(iv) ASw is sound and complete for 'ew .
(v) ASos is sound and complete for ∼o .
(vi) ASol is sound and complete for 'lo .
(vii) ASoe is sound and complete for 'eo .
(viii) ASow is sound and complete for 'wo.
Proof. The soundness can be easily established. For the completeness part the proofs for all the weakcases are similar to each other. Here we only prove (vii). By Lemma 60 we may assume that both P anddef

Q are complete normal forms on V = f n(P +Q)={y1 , . . . , yk }. Let P beX
φi λi .Pii∈I

and Q beX

ψj λj .Qj

j∈J
λ σ

i
Suppose σ is induced by φi and P σ −→Pi σ. There are several cases:

λ σi• λi is an output prefix or a tau prefix. From P 'eo Q one obtains some Q0 such that Qσ =⇒Q0 ande0e0
Pi σ ≈o Q . By Lemma 81, ASo ` τ.Pi σ = τ.Q . By Lemma 74,

ASoe ` Q =
=
=
=
=

38

Q + φi λi σ.Q0
Q + φi λi σ.τ.Q0
Q + φi λi σ.τ.Pi σ
Q + φi λi .τ.Pi
Q + φi λi .Pi

aσ(x)• λi is a restricted output action a(x). Now P 'eo Q implies that some Q0 exists such that Qσ =⇒ Q0
and Pi σ [x6∈D] ≈eo Q0[x6∈D] , where D is (f n(Pi σ + Q0 ) \ {x}). By Lemma 81
00ASoe ` τ.Pi σ [x6∈(f n(Pi σ+Q )\{x})] = τ.Q0[x6∈(f n(Pi σ+Q )\{x})]By Lemma 75
ASoe ` Q=

Q + φi aσ(x).Q0

L8=

Q + φi aσ(x).τ.Q0[x6∈(f n(Pi σ+Q )\{x})]=Q + φi aσ(x).τ.Pi σ [x6∈(f n(Pi σ+Q )\{x})]

L8

=
=

0

0

Q + φi aσ(x).τ.Pi σ
Q + φi a(x).Pi• λi is an input action a(x). It follows from P 'eo Q that some y, Q00 and Q0 exist such thataσ(x)Qσ =⇒ −→ Q00 and Q00 [y/x] =⇒ Q0 ≈eo Pi σ[y/x]. Using a similar proof to that of Lemma 81 one
can show that ASoe ` Q = Q + φi a(x).Pi .
In summary ASoe ` P +Q = Q. Symmetrically ASoe ` P +Q = P . It follows that ASoe ` P = Q.

4.4

An Alternative to the Law S6

We have indicated in Section 4.3 that the law S6 is a bit mysterious. It is used in the ground scenario
to move from the late congruences to the early congruences. Yet it does not appear in any of the open
congruences. In the studies of symbolic systems Lin has used the following alternative to S6:PP
C . i∈I τ.Pi = j∈J τ.Qj
P
P
E-Input
C . i∈I a(x).Pi = j∈J a(x).Qj
He proved that the E-Input rule is enough to transfer the late systems to the early systems. Parrow
has discussed the complete issue for the weak early congruence and the weak late congruence ([36]). His
system for the weak late congruence is virtually the same as ours. On the other hand his system for the
weak early congruence uses the non-symbolic version of the above rule:P
P
τ.Pi = j∈J τ.Qj
i∈I
P
P
E-Input’i∈I a(x).Pi =j∈J a(x).Qj
In this paper we use a slightly stronger version of E-Input’, the rule E-Input”:
PP
ψi τ.Pi = j∈J ψj τ.Qj
i∈I
P
P
E-Input”i∈I ψi a(x).Pi =j∈J ψj a(x).Qj
in which x 6∈ n(ψi ) for each i ∈ I and x 6∈ n(ψj ) for each j ∈ J.
E-Input” clearly subsumes E-Input’. It is not clear under what condition the reverse implication
holds. For the relationship between the E-Input rules and S6, Parrow has pointed out the following fact:
Lemma 83. AS ∪ {M 6} ∪ {E-Input0 } ` S6.
Consequently AS ∪ {M 6} ∪ {E-Input00 } ` S6. The following lemma reveals another interesting fact.
Lemma 84. AS ∪ {E-Input00 } ` T 5.
Proof. We prove that AS ∪ {E-Input00 } ` T 5a. Suppose Y is {y1 , . . . , yn } and x 6∈ n(δ). Then
n
X

T2

=
=

=

i=1
n
X
i=1
n
X
i=1
n
X

τ.(Pi +δ[x=yi ]τ.Q) + τ.(P +δ[x6∈Y ]τ.Q)
τ.(Pi +δ[x=yi ]τ.Q) + τ.(P +δ[x6∈Y ]τ.Q) +τ.(Pi +δ[x=yi ]τ.Q) + τ.(P +δ[x6∈Y ]τ.Q) +

n
X
i=1
n
X

(Pi +δ[x=yi ]τ.Q) + (P +δ[x6∈Y ]τ.Q)
δ[x=yi ]τ.Q + δ[x6∈Y ]τ.Q

i=1

τ.(Pi +δ[x=yi ]τ.Q) + τ.(P +δ[x6∈Y ]τ.Q) + δτ.Q

i=1

39

where the third equality holds by Lemma 61. That isnX

τ.(Pi +δ[x=yi ]τ.Q) + τ.(P +δ[x6∈Y ]τ.Q) =

i=1

n
X

τ.(Pi +δ[x=yi ]τ.Q) + τ.(P +δ[x6∈Y ]τ.Q) + δτ.Q

(7)

i=1

By applying E-Input” to (7) we obtain T5a.
The relationship between a rule and an axiomatic system is less simple than that between a law andan axiomatic system. To explain that we introduce two related notions.
Definition 85. Suppose R is a binary relation on the set of finite π-processes and R is the following rule
A1 = B1. . . An = Bn
A=B

R is derivable in R if ARB holds under the assumption that A1 RB1 , . . . , An RBn hold. R is admissible
in R if it is true that A1 RB1 , . . . , An RBn hold then ARB holds.
Derivability is clearly stronger than admissibility. In terms of axiomatic systems for π-processes, thetwo properties can be defined as follows:• R is derivable in AS if AS ` A = B can be derived under the assumption that AS ` A1 = B1 , . . . ,AS ` An = Bn are derivable.
• R is admissible in AS if whenever AS ` A1 = B1 , . . . , AS ` An = Bn are derivable thenAS ` A = B is derivable.
According to the definition, if R is derivable in AS then AS ` A = B is provable as long as we assume thatAS ` A1 = B1 , . . . , AS ` An = Bn are all provable. It doesn’t matter whether any of AS ` A1 = B1 ,. . . , AS ` An = Bn is actually provable or not. On the other hand, to show that R is admissible, wehave to verify the cases in which all of AS ` A1 = B1 , . . . , AS ` An = Bn are all provable. A good way
to distinguish the two properties is that derivability is about proof systems while admissibility is aboutmodels.
Lemma 86. The following properties hold:(i) E-Input” is not admissible in ∼ls .
(ii) E-Input” is derivable in ∼es .
(iii) E-Input” is not admissible in 'lw .
(iv) E-Input” is derivable in 'ew .
(v) E-Input” is derivable in ∼so .
(vi) E-Input” is not admissible in 'lo .
(vii) E-Input” is derivable in 'eo .
(viii) E-Input” is derivable in 'wo.
Proof. (i) through (iv) are well known. The proof of (v) is simpler than that of (vii) given below.
(vi) It is clear that τ.[x=y]τ.P +τ.[x6=y]τ.P ≈lo τ.[x=y]τ.P +τ.[x6=y]τ.P +τ.P . It is also clear thatla(x).[x=y]τ.P +a(x).[x6a(x).[x=y]τ.P +a(x).[x6=y]τ.P +a(x).P .
P =y]τ.P 6≈eo P(vii) Suppose i∈I ψi τ.Pi 'o j∈J ψj τ.Qj and x 6∈ n(ψi ψj ) for each i ∈ I and each j ∈ J. Let σ bea substitution that validates ψi . Then
X
aσ(x)
(
ψi a(x).Pi )σ −→ Pi σi∈IFor each name y one hasXτ(ψi τ.Pi )σ[y/x] −→ Pi σ[y/x]i∈I0It follows that some Q and j ∈ J exist such that σ[y/x] validates ψj , which is the same as saying that
σ validates ψj since x 6∈ n(ψj ), and thatXτ(
ψj τ.Qj )σ[y/x] −→ Qj σ[y/x] =⇒ Q0 ≈eo Pi σ[y/x]j∈J40System
Ases
Asew
Aseo

Axioms in Addition to AS
M6,E-Input”
M6,E-Input” T1,T2,T3
L8,E-Input” T1,T2,T3,T4

Congruencestrong early equivalence
weak early congruence
early open congruence

Figure 20: Alternative Systems Using E-Input”
ThereforeXτ(ψj τ.Qj )σ −→ Qj σ
j∈JandQj σ[y/x] =⇒ Q0 ≈eo Pi σ[y/x]PPWhat we have verified is that i∈I ψi a(x).Pi 'eo j∈J ψj a(x).Qj .
(viii) The proof is simpler than that of (vii).
Using Lemma 83 and Lemma 7, one can define systems slightly different from those in Figure 19. In
Figure 20 three systems for the early congruences are defined using E-Input”.
Theorem 87. The following completeness results hold:(i) Ases is sound and complete for ∼e .
(ii) Asew is sound and complete for 'ew .
(iii) Aseo is sound and complete for 'eo .
Proof. The completeness is given by Lemma 83, Lemma 84 and Theorem 82. The soundness is supported
by Lemma 86.
So adding E-Input” transfers systems for late congruences to systems for early congruences.
Corollary 88. The following properties hold:(i) E-Input” is not admissible in ASsl .
(ii) E-Input” is derivable in ASse .
l(iii) E-Input” is not admissible in ASw.
e(iv) E-Input” is derivable in ASw .
(v) E-Input” is not derivable in ASos but is admissible in ASos .
(vi) E-Input” is not derivable in ASol but is admissible in ASol .
(vii) E-Input” is derivable in ASoe .
(viii) E-Input” is derivable in ASow .
The fundamental difference between S6 and E-Input” is that the former is an equational law whereas
the latter is an equational rule. The two enjoy different properties: Suppose AS0 and AS1 are two systems
on finite π-processes. Suppose further that AS1 ` P = Q whenever AS0 ` P = Q.
• Then A = B is a derived law of AS1 if it is a (derived) law of AS0 . So an equational law persists
through system extension.
• If R is derivable in AS0 then R is not necessarily admissible in AS1 . So an equational rule is not
persistent through system extension.
We have seen the strict inclusions ASos ⊆ ASol ⊆ ASoe . The rule E-Input” is derivable in ASos . It is notadmissible in ASsl . It is however derivable in ASse .
Persistence property is a good thing to have. This is one of the reasons that a law is preferred toa rule. But there is something that E-Input” can offer: Its restriction to the π-calculus without themismatch operator is straightforward.

41

6
=
strongweak

early congruence
Parrow, Sangiorgi
Parrow, Fu, Yanglate congruence
Parrow, Sangiorgi
Parrow, Fu, Yang

open congruence
Fu, YangFu, Yang

Figure 21: Axiomatization with Mismatch, Revisited=strongweak

early congruence?
?

late congruence?
?

open congruence
Sangiorgi
Fu

Figure 22: Axiomatization without Mismatch, Revisited5

Comment and Related Issue

We have not been able to say anything about the axiomatizations of the four congruences of the πcalculus without the mismatch operator. But we have come up with some results on open congruences.
Figure 21 and Figure 22 summarize the achievements of this paper. We have proposed several new tau
laws and constructed complete systems for the three open congruence relations using these tau laws. We
believe that we have found out the correct definitions of weak open congruence for mobile processes.
The overlook of this issue in previous work is probably due to the fact that the three open bisimilarities
coincide for the π-calculus without the mismatch operator. In our view the results of this paper areimportant because we believe that the mismatch operator has a very important role in the algebraic
theory of mobile processes. This does not necessary mean that the operator is indispensable. But thetradeoff against it is probably not worthwhile in most cases. Take the case of testing equivalence for
instance. In [3] the authors argued that, in their view, testing equivalence would be rather unfamiliar in
the absence of the mismatch operator.
It came as a little surprise that the open semantics gives rise to two different bisimulation congruences.
The discrepancy between the early semantics and the late semantics, in both the open case and the groundcase, is due to the timing of instantiation. An early instantiation replaces the abstract name by anothername at the time the input action happens while a late instantiation does the same after the input action
has committed itself. In the absence of the mismatch operator, an early instantiation by a fresh nameachieve the same effect as a late instantiation. Therefore the mismatch operator is the reason of there
being more than one open bisimilarities. Having realized this one is tempted to think that the early andlate equivalences might be the same had one removed the match operator. This is actually false. The
following is a counter example: Let A be a(x).(x(z).yy+yy.x(z)) + a(x).(x(z).yy+yy.x(z) + τ ). Then
A + a(x).(x(z)|yy) ∼e A
but
A + a(x).(x(z)|yy) 6∼l A
a(x)

a(x)

since the action A + a(x).(x(z)|yy) −→ x(z)|yy is matched up by neither A −→ x(z).yy+yy.x(z) nora(x)A −→ x(z).yy+yy.x(z) + τ . More generallyXa(x).P +a(x).Py ∼ey∈f n(P )X

a(x).Pyy∈f n(P )buta(x).P +X

a(x).Py 6∼ly∈f n(P )X

a(x).Pyy∈f n(P )where, for each y ∈ f n(P ), Py ∼˙ e P [y/x] but not Py ∼˙ l P [y/x]. So for ∼l and ∼e to coincide at all one also
has to get rid of the choice operator.
One might ask the question of why should we need two more bisimulation congruences, the early open
congruence and the late open congruence, given that we already have several bisimulation congruences.
This is of course not a good question. The result of this paper brings out a fuller picture of the open
42

semantics than the previous work has done. Sangiorgi’s definition of open bisimilarity turns out to be a
special case of our definitions. Two better questions are: Why should we need the open semantics? Or
is the mismatch operator good? We are not going to reinforce our argument for the mismatch operator
apart from pointing out that the theoretical investigation of the weak early and late congruences use
the mismatch operator in an essential way. We will answer the question about the open semantics byreaffirming our view about it: The early (late) open congruence has a better claim to be the bisimulation
congruence than the early (late) congruence. As we have mentioned in the paper, two processes arebisimilar if they can not be told apart when putting in dynamic contexts. A dynamic context may wellreplace a free name in the processes by another name. For calculi of mobile processes, closure undersubstitution is a defining property rather than a derived property for bisimulation based equivalences.
This view is supported by some theoretical results. In [2] it is shown that the CCS-like bisimilarity, as wellas the barbed bisimilarity, for the asynchronous π-calculus are closed under substitution! One of the open
problems raised in the introduction is also about this phenomenon. These can be interpreted as sayingthat the defining property of closure under substitution can be dropped in some special cases. In [9, 10,
12, 13, 14, 18, 19] a simplified yet equally powerful calculus of mobile processes, the χ-calculus, is proposed
and investigated. The language has two motivations. One is to give a proof theoretical interpretation ofprocess ([11]) and the other is to simplify the π-calculus. Many bisimilarities for the χ-processes havebeen studied. These include the barbed bisimilarity, the open bisimilarity, and more generally the Lbisimilarities. These equivalences are all required to be closed under substitution. Otherwise the resulting
bisimilarities would not be even closed under composition, which definitely rule out any of these relations
as observational equivalence. In other words, the observationality of the bisimilarities on χ-processes
automatically imposes the condition of closure of substitution. The χ-calculus also makes it clear how
dynamic environments can change the free names of the processes involved.
The symbolic approach to the open bisimilarities for the π-calculus without the mismatch operator
has been studied by Li ([25]). But a correct treatment of the open bisimilarities on π-processes with themismatch operator is not yet available. However this should be a formality in view of the results of thispaper.
The paper would have looked a lot better had we removed the two major regrets of this paper:• One regret is about the question marks in Figure 22. All our attempts to remove any of them haveso far been unsuccessful. The failure makes one wonder if there exists a complete system for anyof the four equivalences. However the message one gets from Lin’s work using symbolic approachhas to be that such systems do exist. The priority at the moment is to get one complete system forany of the four congruences, whatever the system may look like. Improvement of the system maycome afterwards. A result like this might help to reveal some interesting relationship between thesymbolic approach and the non-symbolic approach.
• The other is about the generalization of Lemma 11 to the full π-calculus. The main obstacle isposed by the restriction operator. We have not be able to find a solution to overcome the problem.
From the point of view of axiomatization, some important issues have not been discussed in thispaper, which include the following:• Axiomatization of infinite π-processes is theoretically possible for those processes with finite states.
Milner initiated research in this direction for both the strong and the weak observational equivalences of CCS ([29, 30]). Lin has constructed complete systems for the strong and the weak
congruences on finite control π-processes using a symbolic approach ([27, 28]). One might discover something new by investigating the axiomatization of finite control mobile processes in a
non-symbolic setting.
• In practice equivalence relations are used just as often as congruence relations. Since weak earlyand late equivalences are not necessarily closed under substitution, their axiomatic systems trades
off the ruleP =Q
a(x).P = a(x).Q
for the following rule
P [y/x] = Q[y/x] for every y ∈ f n(P |Q)a(x).P = a(x).Q

43

The treatment of the match and the mismatch operator is a lot more easier. There are only twolaws:[x=y]P[x6=y]P

= P
= 0

(8)
(9)

The details of the systems are not difficult to work out. See [32] for more on the subject.
• The testing equivalence for the π-calculus is quite different from the bisimulation equivalences.
Boreale and De Nicola have defined in [3] the testing equivalence for the π-calculus. This equivalence
is not a congruence. The testing congruence can be defined by the following: P and Q are testing
congruent if and only if P σ and Qσ are testing equivalent for every substitution σ. In [16] a complete
system for the testing congruence is given based upon Boreale and De Nicola’s system. The πcalculus used in [3, 16] comes with the mismatch operator. In our opinion this is largely technicalsince we know nothing about how to axiomatize the testing equivalence/congruence without themismatch. Although removing the mismatch operator introduces an equivalence relation that looks
strange, testing without this operator is definitely interesting. But it appears that one should firstsolve the problems in Figure 22.
• Axiomatization of the barbed equivalence has never been an issue. Since in the π-calculus thestrong barbed equivalence coincides with the strong early equivalence and their weak versions
are most likely to be the same, there seems little point in studying barbed equivalence for the
purpose of axiomatization. Recently Sangiorgi and Walker proposed what they call open barbed
bisimilarity([43]). They showed that it is strictly between the barbed equivalence and the open
bisimilarity. We haven’t looket at the issue of axiomatization for the open barbed congruence.
There are many problems about the other aspects of π-calculus. Most of these problems are subtle.
For the purpose of illustration let’s take a closer look at one of the problems mentioned in the introduction.
The strong ground bisimilarity is obviously too weak to be useful for the whole of π-calculus. The question
is for which subcalculus of the π-calculus the strong ground bisimilarity ∼g is good. The first observationis that the subcalculus should contain neither the match operator nor the mismatch operator because
in general [x=y]P ∼g 0 does not imply ([x=y]P )[y/x] ∼g 0[y/x]. The subcalculus can not contain thereplication operator either. An example that supports this claim can be given in CCS. Let P and Q be
the processes defined below:
P
Q

def

=

def

=

(a)(!(u)(b.c.u|c.b.u.a)|!a.R)(a)(!(u)b.(c.u|c.b.u.a)|!(u)c.(b.u.a|b.c.u)|!a.R)

where R is w.0. Then one can easily verifies that P |Q ∼g Q. But not (P |Q)[c/b] ∼g Q[c/b]. This isbecause the action sequence
τ
τ
τ
τ
w
(P |Q)[c/b] −→−→−→−→−→ A,
for suitable A, can not be matched up by any action sequence from Q[c/b]. For Q[c/b] to perform aw-action it must perform at least five consecutive τ -actions first. So to be precise there are two questions
to be asked:• When confined to the subcalculus with none of the choice, match, mismatch and replication operators, is the strong ground bisimilarity closed under substitution?
• When confined to the subcalculus with none of the choice, match and mismatch operators, is the
weak ground bisimilarity closed under substitution?
These questions are related to the question of when the early bisimilarity and the late bisimilarity coincide.
But we are not going into that issue in this paper. For more about the usefulness of the ground bisimilarity
we refer to [41].
Acknowledgement The authors are grateful to the two anonymous referees for their criticism andsuggestions. The care they have given to the previous drafts of this paper and the extent they have gone
into these drafts are truly remarkable. They have helped tremendously in improving both the content
and the shape of the paper.
44

References[1] R. Amadio and S. Prasad, Modelling IP Mobility, CONCUR ’98, Lecture Notes in Computer Science
1466 (Springer, 1998) 301–316.
[2] R. Amadio, I. Castellani and D. Sangiorgi, On Bisimulations for the Asynchronous π-Calculus,
CONCUR ’96, Lecture Notes in Computer Science 1119 (Springer, 1996) 146–162.
[3] M. Boreale and R. De Nicola, Testing Equivalence for Mobile Processes. Information and Computation, 120 (1995) 279–303.
[4] M. Boreale and R. De Nicola. A Symbolic Semantics for the π-Calculus. Information and Computation, 126 (1996) 34–52.
[5] M. Boreale, On the Expressiveness of Internal Mobility in Name-Passing Calculi, CONCUR ’96,
Lecture Notes in Computer Science 1119 (Springer, 1996) 161–178.
[6] G. Boudol, Asynchrony and π-Calculus, Research Report 1702 (INRIA, Sophia-Antipolis, 1991).
[7] L. Cardelli and A. Gordon, Mobile Ambients, To Appear in Theoretical Computer Science.
[8] R. De Nicola and M. Hennessy, Testing Equivalence for Processes, Theoretical Computer Science 34(1984) 83-133.
[9] Y. Fu, The χ-Calculus, Proceedings of the International Conference on Advances in Parallel andDistributed Computing (IEEE Computer Society Press, 1997) 74–81.
[10] Y. Fu, A Proof Theoretical Approach to Communications, ICALP’97 , Lecture Notes in Computer
Science 1256 (Springer, 1997) 325–335.
[11] Y. Fu, Reaction Graphs, Journal of Computer Science and Technology, 13 (1998) 510–530.
[12] Y. Fu, Bisimulation Lattice of Chi Processes, ASIAN’98 , Lecture Notes in Computer Science 1538
(Springer, 1998) 245–262.
[13] Y. Fu, Variations on Mobile Processes, Theoretical Computer Science, 221 (1999) 327–368.
[14] Y. Fu, Open Bisimulations of Chi Processes, CONCUR’99 , Lecture Notes in Computer Science 1664
(Springer, 1999) 304–319.
[15] Y. Fu, An Open Problem of Mobile Processes, Unpublished Paper, 1999.
[16] Y. Fu, Testing Congruence for Mobile Processes, Journal of Computer Science and Technology, 17(2002).
[17] Y. Fu, A Schematic Axiom for Open Congruence, submitted.
[18] Y. Fu and Z. Yang, Chi Calculus with mismatch, CONCUR 2000 , Lecture Notes in Computer
Science 1877 (Springer, 2000) 596–610.
[19] Y. Fu and Z. Yang, The Ground Congruence for Chi Calculus, FST&TCS 2000 , Lecture Notes in
Computer Science 1974 (Springer, 2000).
[20] M. Hennessy and H. Lin, Symbolic Bisimulations, Theoretical Computer Science, 138 (1995) 353–
369.
[21] M. Hennessy and R. Milner, Algebraic Laws for Nondeterminism and Concurrency, Journal of ACM,
67 (1985) 137–161.
[22] K. Honda and M. Tokoro, An Object Calculus for Asynchronous Communication, ECOOP ’91,
Lecture Notes in Computer Science 512 (Springer, 1991) 133–147.
[23] K. Honda and M. Tokoro, On Asynchronous Communication Semantics, Object-Based Concurrent
Computing, Lecture Notes in Computer Science 612 (Springer, 1991) 21–51.

45

[24] K. Honda and N. Yoshida, On Reduction Based Process Semantics, Theoretical Computer Science,
152 (1995) 437–486.
[25] Z. Li, Theories and Algorithms for the Verification of Bisimulation Equivalences in Value-Passing
CCS and the π-Calculus, PhD Thesis (Changsha Institute of Technology, Changsha, 1999).
[26] H. Lin, Complete Inference Systems for Weak Bisimulation Equivalences in the π-Calculus, Proceedings of Sixth International Joint Conference on the Theory and Practice of Software Development,
Lecture Notes in Computer Science 915 (Springer, 1995) 187–201.
[27] H. Lin, Unique Fixpoint Induction for Mobile Processes, CONCUR ’95, Lecture Notes in Computer
Science 962 (Springer, 1995) 88–102.
[28] H. Lin, Complete Proof Systems for Observation Congruences in Finite-Control π-Calculus,
ICALP ’98, Lecture Notes in Computer Science 1443 (Springer, 1998) 443–454.
[29] R. Milner, A Complete Inference System for a Class of Regular Behaviours, Journal of Computerand System Science, 28 (1984) 439–466.
[30] R. Milner, A Complete Axiomatization System for Observational Congruence of Finite State Behaviours, Information and Computation, 81 (1989) 227-247.
[31] R. Milner, Communication and Concurrency (Prentice Hall, 1989).
[32] 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).
[33] R. Milner and D. Sangiorgi, Barbed Bisimulation, ICALP ’92, Lecture Notes in Computer Science
623 (Springer, 1992) 685–695.
[34] M. Merro and D. Sangiorgi, On Asynchrony in Name-Passing Calculi, ICALP’98 , Lecture Notes in
Computer Science 1443 (Springer, 1998) 856–867.
[35] D. Park, Concurrency and Automata on Infinite Sequences, Lecture Notes in Computer Science 154(Springer, 1981) 561–572.
[36] J. Parrow, On the Relationship Between Two Proof Systems for the Pi-Calculus, Note, 1999.
[37] J. Parrow and D. Sangiorgi, Algebraic Theories for Name-Passing Calculi, Information and Computation, 120 (1995) 174–197.
[38] J. Parrow and B. Victor, The Update Calculus, AMAST ’97, Lecture Notes in Computer Science
1119 (Springer, 1997) 389–405.
[39] J. Parrow and B. Victor, The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes,
LICS ’98 (IEEE Computer Society, 1998) 176–185.
[40] D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms,
PhD thesis (Department of Computer Science, University of Edinburgh, 1993).
[41] D. Sangiorgi, π-Calculus, Internal Mobility and Agent-Passing Calculi, Theoretical Computer Science, 167 (1996) 235–274.
[42] D. Sangiorgi, A Theory of Bisimulation for π-Calculus, Acta Informatica, 3 (1996) 69–97.
[43] D. Sangiorgi and D. Walker, On Barbed Equivalence in π-Calculus, CONCUR ’01, 2001.
[44] B. Thomsen, A Calculus of Higher Order Communicating Systems, POPL’89 (ACM, 1989) 143–154.
[45] B. Thomsen, Plain CHOCS—A Second Generation Calculus for Higher Order Processes, Acta Informatica, 30 (1993) 1–59.
[46] B. Thomsen, A Theory of Higher Order Communicating Systems, Information and Computation,
116 (1995) 38–57.

46

A

ProofsA.1

The Proof of Lemma 55

Proof. We prove the lemma for the late open bisimilarity. The proofs for the other two are almost thesame.
(i) Let R be {(P δ , Qδ )|P ≈lo Q}∪ ≈lo . We prove that R is a late open bisimulation. Suppose P δ RQδ .
If σ does not respect δ then P δ σ ≈lo 0 ≈lo Qδ σ, otherwise consider actions performed by P δ σ. There areseveral cases:λλ• If P δ σ −→ P 0 and λ is an output action or a tau action then, by (ii) of Lemma 39, P σ −→ P 00 forsome P 00 such that P 0 ≡ (P 00 )(δσ) , bearing in mind that P δ σ ≡ (P σ)δσ . It follows from P ≈lo Q
b
λ

b
λ

that Qσ =⇒ Q0 ≈lo P 00 for some Q0 . Therefore Qδ σ =⇒ (Q0 )(δσ) RP 0 .
a(x)• If P δ σ −→ P 0 then the proof is similar to the one in previous case.
a(x)

a(x)

• If P δ σ −→ P 0 then, by (ii) of Lemma 39, P σ −→ P 00 for some P 00 such that (P 00 )δσ ≡ P 0 .
a(x)

00

0

It follows from P ≈lo Q that Qσ =⇒ Q0 for some Q0 such that (P 00 )[x6∈(f n(P +Q )\{x})] ≈lo
00

a(x)

0

(Q0 )[x6∈(f n(P +Q )\{x})] . Thus Qδ σ =⇒ (Q0 )δσ and
00

0

00

0

P 00(δσ)[x6∈(f n(P +Q )\{x})][x6∈n(δσ)] RQ0(δσ)[x6∈(f n(P +Q )\{x})][x6∈n(δσ)]
This completes the proof of (i).
(ii) Let R be {(P, Q) | P δ ≈lo Qδ and ∀x, y.(δ⇒x6=y) ⇒ ({x, y}6⊆f n(P +Q))}. We show that R is alate open bisimulation. Consider the process P σ. If σ substitutes a name z in f n(P +Q) for some namenot in f n(P +Q) Then P σ ≈lo Qσ if and only if P σ 0 ≈lo Qσ 0 , where σ 0 differs from σ only in that theformer maps z onto itself. So without loss of generality we may assume that σ maps names in f n(P +Q)
onto names in f n(P +Q).
λλ

• P σ −→ P 0 and λ is an output action or a tau action. Then P δ σ −→ (P 0 )δσ by Lemma 34 andλb0

Lemma 39. So Qδ σ =⇒ Q00 ≈lo (P 0 )δσ for some Q00 . By Lemma 39 some Q0 exists such that
λb0

Qσ =⇒ Q0 and (Q0 )δσ ≡ Q00 . So P 0 RQ0 .
a(x)• P σ −→ P 0 . The proof is similar to the one in previous case.
a(x)

a(x)

a(x)

• If P σ −→ P 0 then P δ σ ≡ (P σ)δσ −→ P 00 ≡ (P 0 )δσ for some P 0 and P 00 . Therefore Qδ σ =⇒ Q00 ≈loa(x)(P 0 )δσ for some Q00 . Then by Lemma 39, Qσ =⇒ Q0 for some Q0 such that (Q0 )δσ ≡ Q00 . Now
00

00

00

00

(Q00 )[x6∈(f n(P +Q )\{x})] ≈lo (P 00 )[x6∈(f n(P +Q )\{x})]implies by (i) that
0

0

0

0

(Q0 )(δσ)[x6∈(f n(P +Q )\{x})][x6∈n(δσ)] ≈lo (P 0 )(δσ)[x6∈(f n(P +Q )\{x})][x6∈n(δσ)]
It is easy to see that (δσ)[x 6∈ n(δσ) \ f n(P 0 + Q0 )] satisfies the condition of R. Hence
0

0

0

0

(Q0 )[x6∈(f n(P +Q )\{x})] R(P 0 )[x6∈(f n(P +Q )\{x})]We have proved that R is a late open bisimulation.

A.2

The Proof of Lemma 62

W
Proof. Suppose i∈I ψi is a tautology. We may assume
that it contains at least two distinct names.
W
Otherwise the result can be easily proved. Let f n( i∈I ψi ) be {x, y1 , . . . , yn }. We may assume that ψi
is complete on {x, y1 , . . . , yn }, for each i ∈ I, because otherwise we could use the equivalence
x=y ∨ x6=y ⇔ >47

to expand it. Now consider
x=yj ∧ (_ψi ) ⇔ x=yj

(10)

i∈I

W
where j ∈ {1, . . . , n}. For each i ∈ I, either ψi ⇒ x6=yj or ψi ⇒ x=yj by completeness. Because i∈I ψi
is a tautology, there must exist some i ∈ I such that ψi ⇒ x6=yj . Consequently (10) is equivalent to_x=yj ∧ (ψi ) ⇔ x=yj
(11)
i∈I 0

for some strict subset I 0 of I such that for each i ∈ I 0 one has ψi ⇒ x=yj . By substituting yj for x in(11), one obtains_
ψi [yj /x] ⇔ >
(12)
i∈I 0

W

W
Since i∈I 0 ψi [yj /x] contains strictly less free names than i∈I ψi , we could use the induction hypothesis
to conclude thatX
ψi [yj /x]P = Pi∈I 0and therefore[x=yj ]

X

ψi P = [x=yj ]P

(13)

_

(14)

i∈I

Let Y be {y1 , . . . , yn }. Next we consider
x6∈Y ∧ (ψi ) ⇔ x6∈Yi∈I

It follows easily from (14) thatx6∈Y ∧ (_ψi0 ) ⇔ x6∈Yi∈I 00for some I 00 and ψi0 , where i ∈ I 00 , such that the following conditions are satisfied:• I 00 is a strict subset of I;• x6∈Y ∧ ψi0 ⇔ ψi for each i ∈ I 00 ;W
• x 6∈ n( i∈I 00 ψi0 ).
It follows that_x6∈Y ⇒

ψi00

i∈I 00from which it follows thatW0i∈I 00 ψi is a tautology. So by induction hypothesisXψi0 [x6∈Y ]P = [x6∈Y ]P(15)i∈I 00

It follows easily from (15) that[x6∈Y ]

X

ψi P = [x6∈Y ]P

(16)

i∈I

Uisng Lemma 61, (13) and (16), one getsP==

[x=y1 ]P + . . . +[x=yn ]P +[x6∈Y ]PX
XX[x=y1 ](
ψi P )+ . . . +[x=yn ](ψi P )+[x6∈Y ](ψi P )
i∈I

=

X

i∈I

ψi P

i∈I

This completes the proof.
48

i∈I

A.3

The Proof of Lemma 69

W
Proof. By Lemma 62 one has that P = φP +¬φP . Intuitively let ¬φ be Pi∈I ψi , where each ψi , fori ∈ I, is either a match operator or a mismatch operator. Formally ¬φP is i∈I ψi P . It is clear thatM6

M6

ψi φ ⇔ ⊥ for each i ∈ I. It is also clear that ¬φπ.(P +φQ) = ¬φπ.P and φπ.(P +¬φQ) = φπ.P .
Another important equality is¬φπ.¬φP = ¬φπ.P(17)which can be justified as follows:¬φπ.¬φP

=

=

X

ψi π.

X

ψj P

i∈I

j∈I

X

ψi π.(ψi P +

i∈I
M6

=

X

=

X

ψj P )j∈I

ψi π.(P +

i∈I
D1

j6=i
X

j6=i
X

ψj P )j∈I

ψi π.P

i∈I

=

¬φπ.P

Therefore
τ.(P + φτ.Q)= φτ.(P +φτ.Q)+¬φτ.(P +φτ.Q)= φτ.(P +τ.Q) + ¬φτ.P

On the other hand
τ.(P +τ.(φτ.Q+¬φτ.P ))

=
(17)

=
=

(17)

=

(17)

=
=

φτ.(P +τ.(φτ.Q+¬φτ.P ))+¬φτ.(P +τ.(φτ.Q+¬φτ.P ))φτ.(φP +φτ.(φτ.Q+¬φτ.P ))+¬φτ.(¬φP +¬φτ.(φτ.Q+¬φτ.P ))φτ.(φP +φτ.φτ.Q)+¬φτ.(¬φP +¬φτ.¬φτ.P )φτ.(P +τ.Q)+¬φτ.(¬φP +¬φτ.τ.P )φτ.(P +τ.Q)+¬φτ.(P +τ.τ.P )φτ.(P +τ.Q)+¬φτ.PThis completes the proof.

A.4

The Proof of Lemma 70

Proof. Using T 5a one can prove by induction on the number of the match operators in φ thatkXa(x).(Pi +φ[x=yi ]τ.Q)+a(x).(P +φ[x6∈Y ]τ.Q)

i=1

=

k
X

a(x).(Pi +φ[x=yi ]τ.Q)+a(x).(P +φ[x6∈Y ]τ.Q)+φa(x).Q

(18)

i=1

is provable in AS ∪ {T 1, T 2, T 3}, where x 6∈ n(φ).
Suppose V = n(∪i∈V ψi )\{x} = {y1 , . . . , yn }. Let {Rl } be the set of all equivalence relations on V and{φl } the set of corresponding conditions that are complete on V . For each φl , either φl ψ ⇔ φl or φl ψ ⇔ ⊥.
Suppose k ∈ {1, . . . , n}. If φl ψ ⇔ ⊥ then φl ψ[x=yk ]τ.Q
W = 0. If φl ψ ⇔ φl then φl ψ[x=yk ] is completeon V ∪ {x}. It follows from φl [x=yk ] ⇔ φl ψ[x=yk ] ⇔ i∈I φl ψi [x=yk ] that φl [x=yk ] ⇔ φl ψjk [x=yk ] forsome jk ∈ I. By using D1 and M 1 one gets thatAS ∪ {T 1, T 2, T 3} ` a(x).(Pjk + ψjk τ.Q)

D1

=

M1

=
=

49

a(x).(Pjk + ψjk τ.Q + φl ψjk [x=yk ]τ.Q)
a(x).(Pjk + ψjk τ.Q + φl ψ[x=yk ]τ.Q)
a(x).(Pj0k + φl ψ[x=yk ]τ.Q)

where Pj0k is Pjk + ψjk τ.Q. Similarly some j ∈ I exists such thatAS ∪ {T 1, T 2, T 3} ∪ {T 5a} ` a(x).(Pj + ψj τ.Q) = a(x).(Pj0 + φl ψ[x 6∈ V ]τ.Q)
where Pj0 is Pj + ψj τ.Q. So
AS ∪ {T 1, T 2, T 3} ∪ {T 5a} `X

a(x).(Pi + ψi τ.Q)

i∈I

=

X

(18)

X

a(x).(Pi + ψi τ.Q) +

i∈I

=

n
X

a(x).(Pj0k + φl ψ[x=yk ]τ.Q) + a(x).(Pj0 + φl ψ[x6∈V ]τ.Q)

k=1

a(x).(Pi + ψi τ.Q) + φl ψa(x).Qi∈I

from which one gets
AS ∪ {T 1, T 2, T 3} ∪ {T 5a} `X

a(x).(Pi + ψi τ.Q) =i∈I

Xa(x).(Pi + ψi τ.Q) +

i∈I

=

X

X

φl ψa(x).Qla(x).(Pi + ψi τ.Q) + ψa(x).Qi∈I

By Lemma 62.

A.5

The Proof of Lemma 73

Proof. We show that AS ∪ {T 1, T 2, T 3} ∪ {S6} ` T 5a. Now suppose k ≥ 1, Y = {y1 , y2 , . . . , yk } andx 6∈ n(δ). Thenk
Xa(x).(Pi +δ[x=yi ]τ.Q) + a(x).(P +δ[x6∈Y ]τ.Q)

i=1
S6

=

k−1
X

a(x).(Pi +δ[x=yi ]τ.Q) + a(x).([x=yk ](Pk +δ[x=yk ]τ.Q)+[x6=yk ](P +δ[x6∈Y ]τ.Q))

i=1

=

k−1
X

a(x).(Pi +δ[x=yi ]τ.Q) + a(x).(. . . +δ[x=yk ]τ.Q+δ[x6∈Y ]τ.Q)

i=1
S6

=

k−2
X

a(x).(Pi +δ[x=yi ]τ.Q)

i=1+a(x).([x=yk−1 ](Pk−1 +δ[x=yk−1 ]τ.Q)+[x6=yk−1 ](. . . +δ[x=yk ]τ.Q+δ[x6∈Y ]τ.Q))
=

k−2
X

a(x).(Pi +δ[x=yi ]τ.Q) + a(x).(. . . +δ[x=yk−1 ]τ.Q+δ[x6=yk−1 ][x=yk ]τ.Q+δ[x6∈Y ]τ.Q)

i=1
(6)

=

k−2
X

a(x).(Pi +δ[x=yi ]τ.Q) + a(x).(. . . +δ[x=yk−1 ]τ.Q+δ[x=yk ]τ.Q+δ[x6∈Y ]τ.Q)

i=1

where (6) is the equality used in the proof of Lemma 61. Continuing in this way one getskXa(x).(Pi +δ[x=yi ]τ.Q) + a(x).(P +δ[x6∈Y ]τ.Q)

i=1

=
=
T3

=

=

a(x).(. . . +δ[x=y1 ]τ.Q+ . . . +δ[x=yk−1 ]τ.Q+δ[x=yk ]τ.Q+δ[x6∈Y ]τ.Q)
a(x).(. . . +δτ.Q)
a(x).(. . . +δτ.Q) + δa(x).QkX

a(x).(Pi +δ[x=yi ]τ.Q) + a(x).(P +δ[x6∈Y ]τ.Q) + δa(x).Q

i=1

50

This completes the proof.

A.6

The Proof of Lemma 77

Proof. By the assumption of the lemma and Lemma 74
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 )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 that
Q = Q + ψa(x).(τ.Q0 +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.

A.7

The Proof of Lemma 79

Proof. By assumption, for each j ∈ {1, . . . , k}, the following conditions hold:a(x)τ• Qσ=⇒ −→ Q0j σ and either Q0j σ[yj /x] =⇒ Qj or Q0j σ[yj /x] ≡ Qj .
a(x)τ• Qσ=⇒ −→ Q0k+1 σ and either Q0k+1 σ =⇒ Qk+1 or Q0k+1 σ ≡ Qk+1 .
By Lemma 74 one gets thateASw
` Q = Q + ψa(x).Q01 + . . . + ψa(x).Q0k + ψa(x).Q0k+1

Now f n(Q0j ) ⊆ {x} ∪ f n(Q) ⊆ {x} ∪ V ; σ[yj /x] is complete on {x} ∪ V and is induced by ψ[x=yj ]. There
are two cases:51τ• If Q0j σ[yj /x] =⇒ Qj then Q0j = Q0j + ψ[x=yj ]τ.Qj follows by Lemma 74. Now by Lemma 69, one
has
τ.(P +[x=y]τ.Q) = τ.(P +τ.([x=y]τ..Q+τ.[x6=y]τ.P ))Using the above equality, one hasψa(x).Q0j====

ψa(x).(Q0j +ψ[x=yj ]τ.Qj )ψa(x).(Q0j +[x=yj ]τ.Qj )ψa(x).(Q0j +τ.([x=yj ]τ.Qj +[x6=yj ]τ.Q0j ))ψa(x).Q0j + ψa(x).([x=yj ]τ.Qj +[x6=yj ]τ.Q0j )• If Q0j σ[yj /x] ≡ Qj thenψa(x).Q0j= ψa(x).Q0j + ψa(x).([x=yj ]τ.Q0j +[x6=yj ]τ.Q0j )= ψa(x).Q0j + ψa(x).([x=yj ]τ.Q0j σ[yj /x]+[x6=yj ]τ.Q0j )= ψa(x).Q0j +ψa(x).([x=yj ]τ.Qj +[x6=yj ]τ.Q0j )τ

Now if Q0k+1 σ =⇒ Qk+1 then by Lemma 69 one gets
τ.(P +[x6∈V ]τ.Q) = τ.(P +τ.([x6∈V ]τ.Q+[x∈V ]τ.P ))By Lemma 74 and the above equality one hasψa(x).Q0k+1

=
=
=
=

ψa(x).(Q0k+1 +ψ[x6∈V ]τ.Qk+1 )ψa(x).(Q0k+1 +[x6∈V ]τ.Qk+1 )ψa(x).(Q0k+1 +τ.([x6∈V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 ))ψa(x).Q0k+1 +ψa(x).([x6∈V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 )If Q0k+1 σ ≡ Qk+1 thenψa(x).Q0k+1

M2

=
=
=

ψa(x).Q0k+1 σψa(x).Qk+1
ψa(x).τ.Qk+1

S5

ψa(x).([x6∈V ]τ.Qk+1 +[x∈V ]τ.Qk+1 )=In either case we may assume that
ψa(x).Q0k+1 = ψa(x).Q0k+1 +ψa(x).([x6∈V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 )It follows that
Q = Q + ψa(x).([x=y1 ]τ.Q1 +[x6=y1 ]τ.Q01 )..
.
+ψa(x).([x=yk ]τ.Qk +[x6=yk ]τ.Q0k )+ψa(x).([x6∈V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 )Using S6 one hasψa(x).([x=yk ]τ.Qk +[x6=yk ]τ.Q0k ) + ψa(x).([x6∈V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 )= ψa(x).([x=yk ]τ.Qk +[x6=yk ]τ.Q0k ) + ψa(x).([x6∈V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 )+ψa(x).([x=yk ]([x=yk ]τ.Qk +[x6=yk ]τ.Q0k ) + [x6=yk ]([x 6∈ V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 ))= ψa(x).([x=yk ]τ.Qk +[x6=yk ]τ.Q0k ) + ψa(x).([x6∈V ]τ.Qk+1 +[x∈V ]τ.Q0k+1 )+ψa(x).([x=yk ]τ.Qk +[x6∈V ]τ.Qk+1 )52

To continue consider the following process
ψa(x).([x=yk−1 ]τ.Qk−1 +[x6=yk−1 ]τ.Q0k−1 ) + ψa(x).([x=yk ]τ.Qk +[x6∈V ]τ.Qk+1 )Using similar argument we getψa(x).([x=yk−1 ]τ.Qk−1 +[x6=yk−1 ][x=yk ]τ.Qk +[x6∈V ]τ.Qk+1 )By repeating this construction we finally getψa(x).([x=y1 ]τ.Q1 + . . . +[x6=y1 ] . . . [x6=yk−1 ][x=yk ]τ.Qk +[x6∈V ]τ.Qk+1 )Therefore
Q = Q + ψa(x).([x=y1 ]τ.Q1 + . . . +[x6=y1 ] . . . [x6=yk−1 ][x=yk ]τ.Qk +[x6∈V ]τ.Qk+1 )This complete the proof.

A.8

The Proof of Lemma 80
a(x)

a(x)

τ

Proof. If Qσ=⇒Q1 −→ Q0 then ASog ` Q = Q+ψa(x).Q0 follows by Lemma 74. If Qσ=⇒ −→ Q1 =⇒ Q0
then [x6∈V ]ψ is complete on f n(Q1 ) since f n(Q1 ) ⊆ f n(Q) ∪ {x}. Thus σ is induced by [x6∈V ]ψ.
Consequently by Lemma 74
ASog ` Q1 = Q1 +[x6∈V ]ψτ.Q0
It follows that
ASog ` Q ====Q+ψa(x).Q1
Q+ψa(x).(Q1 +[x6∈V ]ψτ.Q0 )Q+ψ(a(x).(Q1 +[x6∈V ]ψτ.Q0 )+ψa(x).Q0 )Q+ψa(x).Q0

where the third equation is valid by Lemma 72.

A.9

The Proof of Lemma 81

Proof. The proofs of all the five clauses are similar to each other. The only difference is in the treatment
of input actions and, to a lesser degree, restricted output actions. Now suppose P ≈ Q, where ≈ is anyof the five bisimilarities. By Lemma 60 we may assume that both P and Q are complete normal forms
def
on V = f n(P +Q)={y1 , . . . , yk }. Let P beX
φi λi .Pii∈I

and Q beX

ψj λj .Qj

j∈J
λ σ

i
Suppose σ is induced by φi and P σ −→Pi σ.
The proof of this lemma is carried out by induction on the sum of depths of P and Q.
τIf λi is a τ prefix and the τ action is simulated by Qσ =⇒ Qj σ for some j ∈ J, then by induction
hypothesis AS ∪ {T 1, T 2, T 3} ` τ.Pi σ = τ.Qj σ. The simulation can happen only if φi ⇒ ψj . But
then φi ⇔ ψj since both φi and ψj are complete on V and agree with σ. By (i) of Lemma 74, AS ∪
τ{T 1, T 2, T 3} ` Q+φi τ.Pi = Q+φi τ.Pi σ = Q+ψj τ.Qj σ = Q+ψj τ.Qj = Q. If P σ −→ Pi σ is simulated byvacuous action then AS ∪ {T 1, T 2, T 3} ` Q+φi τ.Pi = Q+φi τ.Pi σ = Q+φi τ.Qσ = Q+φi τ.Q.
If λi is an output prefix ax then, by (ii) of Lemma 74 and similar approach, it is easy to see thatAS ∪ {T 1, T 2, T 3} ` Q+φi ax.Pi = Q.

53

aσ(x)

Suppose λi is a restricted output action a(x). If P ≈lw Q then some Q0 exists such that Qσ =⇒˙ lw Pi σ. Therefore ([x6∈V ]φi Q0 )σ ≈lw ([x6∈V ]φi Pi )σ. Since [x6∈V ]φi is complete on V ∪ {x} ⊇Q0 σ ≈f n(Q0 +Pi σ) we may deduce from Lemma 45 that [x6∈V ]φi Q0 ≈lw [x6∈V ]φi Pi . By induction hypothel
sis ASw` τ.[x6∈V ]φi Q0 = τ.[x6∈V ]φi Pi . ConsequentlylASw` Q+φi a(x).Pi

=
=
=
=

Q+φi aσ(x).[x6∈V ]φi Pi
Q+φi aσ(x).τ.[x6∈V ]φi Pi
Q+φi a(x).τ.[x6∈V ]φi Q0
Q+φi a(x).[x6∈V ]φi Q0L8Q+φi a(x).φi Q0
Q+φi a(x).Q0
Q

=
=
=

aσ(x)

The proof for weak early bisimilarity is similar. If P ≈lo Q then some Q0 exists such that Qσ =⇒ Q000
and (Pi σ)[x6∈(f n(Pi σ+Q )\{x})] ≈lo (Q0 )[x6∈(f n(Pi σ+Q )\{x})] . By induction hypothesis one has
00ASol ` τ.(Pi σ)[x6∈(f n(Pi σ+Q )\{x})] = τ.(Q0 )[x6∈(f n(Pi σ+Q )\{x})]Using L8 one obtains that a(x).P = a(x).P [x6∈Y ] for any set Y whose elements are names free in P .
Therefore by Lemma 75 one gets
ASol ` Q+φi a(x).Pi= Q+φi aσ(x).Pi σ
0= Q+φi aσ(x).(Pi σ)[x6∈(f n(Pi σ+Q )\{x})]0= Q+φi aσ(x).τ.(Pi σ)[x6∈(f n(Pi σ+Q )\{x})]0= Q+φi aσ(x).τ.(Q0 )[x6∈(f n(Pi σ+Q )\{x})]0= Q+φi aσ(x).(Q0 )[x6∈(f n(Pi σ+Q )\{x})]= Q+φi aσ(x).Q0= Q
The proofs for the cases of the weak early bisimilarity and the weak open bisimilarity are similar.
Next we examine input actions in each of the five cases. Suppose λi is aσ(x).
aσ(x)(i) P ≈lw Q. λi is an input prefix. Let σ be a substitution that is induced by φi . Now P σ −→ Pi σ.
It follows from P ≈lw Q that Q0 exists such that the following properties hold:aσ(x)1. Qσ =⇒ −→ Q0 σ.
˙ lw Pi σ[yl /x] for l ∈ {1, . . . , k}.
2. Qil exists such that Q0 σ[yl /x] =⇒ Qil σ[yl /x]≈
˙ lw Pi σ.
3. Qik+1 exists such that Q0 σ =⇒ Qik+1 σ ≈It follows that, for l ∈ {1, . . . , k},˙ lw(φi [x=yl ]Qil )σ[yl /x] ≈(φi [x6∈V ]Qik+1 )σ(φi [x=yl ]Pi )σ[yl /x]

˙ lw≈(φi [x6∈V ]Pi )σ

≈lw
≈lw

φi [x=yl ]Piφi [x6∈V ]Pi

Consequently, for l ∈ {1, . . . , k},φi [x=yl ]Qilφi [x6∈V ]Qik+1

by Lemma 45. Then by induction one has, for l ∈ {1, . . . , k},lASw` τ.φi [x=yl ]Qill
ASw ` τ.φi [x6∈V ]Qik+1

54= τ.φi [x=yl ]Pi= τ.φi [x6∈V ]PiBy Lemma 77, one can get
Q=

Q+φi aσ(x).(τ.Q0 +φikX[x=yl ]τ.Qil +φi [x6∈V ]τ.Qik+1 )

l=1
M6

=

Q+φi a(x).(τ.Q0 +φikX[x=yl ]τ.φi [x=yl ]Qil +φi [x6∈V ]τ.φi [x6∈V ]Qik+1 )l=1=

Q+φi a(x).(τ.Q0 +φikX[x=yl ]τ.φi [x=yl ]Pi + φi [x6∈V ]τ.φi [x6∈V ]Pi )l=1=

Q+φi a(x).(τ.Q0 +φikX[x=yl ]τ.Pi + φi [x6∈V ]τ.Pi )

l=1

=
=
=

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

This completes the proof of (i).
aσ(x)(ii) P ≈ew Q and P σ −→ Pi σ. It follows from P ≈ew Q thataσ(x)˙ ew Pi σ[y1 /x],Qσ =⇒ Q0i1 σ, Q0i1 σ[y1 /x] =⇒ Qi1 σ[y1 /x]≈
..
.
aσ(x)
˙ ew Pi σ[yk /x],Qσ =⇒ Q0ik σ, Q0ik σ[yk /x] =⇒ Qik σ[yk /x]≈aσ(x)˙ ew Pi σ
Qσ =⇒ Qik+1 σ ≈for Q0i1 , . . . , Q0ik , Qi1 , . . . , Qik , Qik+1 . So for each l ∈ {1, . . . , k},˙ ew(φi [x=yl ]Qil )σ[yl /x] ≈˙ ew(φi [x6∈V ]Qik+1 )σ ≈(φi [x=yl ]Pi )σ[yl /x](φi [x6∈V ]Pi )σBy Lemma 45 one gets, for l ∈ {1, . . . , k}, thatφi [x=yl ]Qilφi [x6∈V ]Qik+1

≈ew
≈ew

φi [x=yl ]Piφi [x6∈V ]Pi

Using induction hypothesis one infers, for l ∈ {1, . . . , k}, that
e
ASw
e
ASw

`
`

τ.(φi [x=yl ]Qil ) = τ.(φi [x=yl ]Pi )τ.(φi [x6∈V ]Qik+1 ) = τ.(φi [x6∈V ]Pi )By Lemma 79, one derives that
Q = Q+φi aσ(x).([x=y1 ]τ.Qi1 +[x6=y1 ][x=y2 ]τ.Qi2 + . . . +[x6∈V ]τ.Qik+1 )= Q+φi a(x).(φi [x=y1 ]τ.φi [x=y1 ]Qi1 +φi [x6=y1 ][x=y2 ]τ.φi [x=y2 ]Qi2
+ . . . +φi [x6∈V ]τ.φi [x6∈V ]Qik+1 )= Q+φi a(x).(φi [x=y1 ]τ.φi [x=y1 ]Pi +φi [x6=y1 ][x=y2 ]τ.φi [x=y2 ]Pi+ . . . +φi [x6∈V ]τ.φi [x6∈V ]Pi )= Q+φi a(x).([x=y1 ]τ.Pi +[x6=y1 ][x=y2 ]τ.Pi + . . . +[x6∈V ]τ.Pi )= Q+φi a(x).Pi
which completes the proof of (ii).
aσ(x)

aσ(x)

(iii) P ≈lo Q and P σ −→ Pi σ. It follows from P ≈lo Q that Q0 exists such that Qσ =⇒ −→ Q0 σ andthe following conditions hold:• For each l ∈ {1, . . . , k}, Qil exists such that Q0 σ[yl /x] =⇒ Qil ≈lo Pi σ[yl /x].
55

• Qik+1 exists such that Q0 σ =⇒ Qik+1 ≈lo Pi σ.
Now by Lemma 77 one can get
ASol ` Q = Q+φi a(x).(τ.Q0 +kX

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

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

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

l=10= Q+φi a(x).(τ.Q +k
X

φi [x=yl ]τ.Pi +φi [x6∈V ]τ.Pi )l=1= Q+φi a(x).(τ.Q0 +φi τ.Pi )= Q+φi a(x).(τ.Q0 +τ.Pi )= Q+φi a(x).Pi
where the fourth equality is justified by Lemma 61.
aσ(x)(iv) P ≈eo Q andP σ −→ Pi σ. Then both of the following conditions hold:aσ(x)• For each l ∈ {1, . . . , k}, Q0il and Qil exist such that Qσ=⇒ −→ Q0il σ and Q0il σ[yl /x] =⇒ Qil ≈eo
Pi σ[yl /x].
aσ(x)• Some Q0ik+1 and Qik+1 exist such that Qσ=⇒ −→ Q0ik+1 σ =⇒ Qik+1 ≈eo Pi σ.
By Lemma 78 one can get
ASoe ` Q

=

Q+

k
X

φi a(x).(τ.Q0il +φi [x=yl ]τ.Qil )+φi a(x).(τ.Q0ik+1 +φi [x6∈V ]τ.Qik+1 )

l=1

=

Q+

k
X

φi a(x).(τ.Q0il +φi [x=yl ]τ.Pi σ[yl /x])+φi a(x).(τ.Q0ik+1 +φi [x6∈V ]τ.Pi σ)

l=1

=

Q+

k
X

φi a(x).(τ.Q0il +φi [x=yl ]τ.Pi )+φi a(x).(τ.Q0ik+1 +φi [x6∈V ]τ.Pi )

l=1
T5

k
X

φi a(x).(τ.Q0il +φi [x=yl ]τ.Pi )+φi a(x).(τ.Q0ik+1 +φi [x6∈V ]τ.Pi )+φi a(x).Pi

=

Q+

=

Q+φi a(x).Pi

l=1

This completes the proof of (iv).
aσ(x)

aσ(x)

0
w
(v) P ≈wo Q and P σ −→ Pi σ. It follows that Qσ =⇒ Q ≈o Pi σ. By induction one has thatASow ` τ.Q0 = τ.Pi σ
By Lemma 80
ASow ` Q =====Q+φi aσ(x).Q0
Q+φi aσ(x).τ.Q0
Q+φi aσ(x).τ.Pi σ
Q+φi a(x).τ.Pi
Q+φi a(x).Pi

This completes the proofs of all the input cases.
In summary in each of the five axiomatic systems AS 0 , one has thatX
AS 0 `
φi τ.Q+Q=P +Q
i∈I 0

56

for some subset I 0 of I. It follows from T 4 that
AS 0 `τ.(P + Q) = τ.(X

φi τ.Q + Q) = τ.Qi∈I 0Symmetrically AS 0 `τ.(P +Q)=τ.P . Hence AS 0 ` τ.P =τ.Q.

57