Decidability of Behavioral Equivalences inProcess Calculi with Name Scoping?
Chaodong He, Yuxi Fu, Hongfei FuBASICS, Department of Computer Science
Shanghai Jiao Tong University, Shanghai 200240, China
MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems

Abstract. Local channels and their name scoping rules play a significant role in the study of the expressiveness of process calculi. The paper
contributes to the understanding of the expressiveness in the context
of CCS by studying the decidability issues of the bisimilarity/similarity
checking problems. The strong bisimilarity for a pair of processes in
the calculi with only static local channels is shown Π10 -complete. The
strong bisimilarity between those processes and the finite state processes
is proved decidable. The strong similarity between the finite state processes and the processes without name-passing capability is also shown
decidable.

1

Introduction

Process calculi are usually Turing complete. The known proofs of Turing completeness share the same guideline that counting is represented as the nestingof suitable components [4, 6, 20]. In the name-passing calculi [24, 26], the encodings of counter [4, 6] depend on the existence of local channels and some degrees
of name-passing capabilities. In the setting of CCS-like calculi, there are several
Turing complete variants in which local channels are provided by the localization
operation while name-passing capabilities are partly obtained by an explicit operation such as parametric definition [23, 11] or relabeling [22], or by an implicit
dynamic-scoping recursion [28, 4].
A fundamental problem in the area of system verification is that of equivalence (or preorder) checking [3]. In concurrency theory these are the problemsof deciding whether two given processes are behaviorally equal, or whether one
process is behavioral close to the other. Among these equivalences (or preorders),
bisimilarity (or similarity) plays a prominent role.
This paper explores the decidability issues of bisimilarity/similarity checking
problems for various subcalculi of CCS classified by different name scoping rules,in which the capability of producing and manipulating local channels becomes
weaker and weaker. These decidability results contribute to the understandingof the way productions and mobilities of local channels affect the expressiveness.
?

The work is supported by NSFC (60873034, 61033002).

µ
CCS
O ◦

/ CCSµ•O/ CCSµO

CCS!◦/ CCS!•/ CCS!

/ CCSPdef

Fig. 1. CCS Hierarchy

The seven subcalculi of CCS studied in this paper are given in Fig. 1. In the/ ’ indicates the sub-language relationship. These seven
diagram an arrow ‘
subcalculi are further divided into four classes in which the scoping rules of local
channel names are weakened gradually.
The first class contains CCSPdef , the full CCS with parametric definition(but without relabeling), which is known to be Turing complete [11]. In CCSPdef
process copies can be nested at arbitrary depth by the name-passing capability
offered by parametric definition. Turing completeness implies that all behavioral
equivalences and preorders for CCSPdef are undecidable.
The second class contains CCSµ and CCS! . These two subcalculi have thepower of producing new local channels but do not have the power of passing
names around. In both models the infinite behaviors are specified by (static
scoping) recursion and replication respectively. They are not Turing complete
because they are not expressive enough to define the process Counter in thesense of Section 2.5 of [10]. For the readers unfamiliar with the static scoping
recursion, we give the following illustration. Static scoping and dynamic scoping
are different ways of manipulating local names when unfolding recursions [11,def10]. When a process is defined as P = µX.(a | (a)(a | X)), the static scoping
requires that the local a and the global a must be distinguished before unfolding. That is, µX.(a | (a)(a | X)) is understood the same as µX.(a | (a0 )(a0 | X)).
The recursion used in [4, 6] admits dynamic scoping, meaning that P should
be understood as a | (a)(a | a | (a)(a | P )), which induces the infinite computationττP −→ a | (a)(0 | 0 | (a)(a | P )) −→ . . .. It is pointed out in [11] that the dynamic
scoping recursion can be encoded via parametric definition. For this reason weshall only consider the parametric definition in this paper.
The third class contains CCSµ• and CCS!• . They are the subcalculi of CCSµand CCS! which have only static local names. Here ‘static’ means that no local
channels can be produced during the evolution of a process. In these situations, localizations can only act as the outermost constructors, and processesa)P where the inner process
in CCSµ• and CCS!• can be assumed in the form (eP is localization-free. In this paper the word ‘static’ is only used in the context of ‘static local names’ in order to avoid confusion with the ‘static scoping
recursion’.
The fourth class contains CCSµ◦ and CCS!◦ , where the localization operator
are removed completely. For those subcalculi, strong bisimilarity is decidable [7].
We will use notation L1 ∼ L2 (or L1 - L2 ) to indicate the problem of checking strong bisimilarity (or strong similarity) between an L1 process and an L2
2

L

L∼L

L ∼ FS FS - L L - FS

CCS!◦
CCSµ
◦
CCS!•
CCSµ
•
!

X [7]
X [7]
?
?
X [7]
X [7]
?
?
?
?
?
?
?
?
?
?
CCS
?
?
?
?
CCSµ
?
?
?
?
CCSPdef × [4, 11] × [4, 11] × [4, 11] × [4, 11]“∼”: strong bisimilarity“-”: strong similarity“X”: known decidable“×”: known undecidable“?”: unknown

Fig. 2. Problems to Explore

process. These problems are indicated by the question marks in the table ofFig. 2. The notation FS stands for the class of the finite state processes. The
contributions of this paper are summarized as follows.
– We show the undecidability (Π10 -hardness) of CCSµ• ∼ CCSµ• by a reduction
from the halting problem of Minsky Machine. The relevant technique is called‘Defender’s Forcing’ [14, 18], which is widely used in undecidability proofs
for bisimilarity checking. Typical examples of this technique can also befound in [17, 18]. The reduction is then modified to show the undecidability(Π10 -hardness) of CCS!• ∼ CCS!• . This resolves the four problems in the firstcolumn of the table.
– Busi, Gabbrielli and Zavattaro establish in [5] the undecidability (Σ10 hardness) of the weak bisimilarity of CCS! . By modifying the proof of Busi etal., CCS! ∼ FS is shown undecidable (Π10 -hard), which immediately implies
the undecidability (Π10 -hardness) of CCSµ ∼ FS.
– By constructing a translation from CCS!• to the Labeled Petri Net, wedemonstrate the decidability of CCS!• ∼ FS, CCS!• - FS and FS - CCS!• ,making use of Jančar and Moller’s decidability result [16] on the Labeled
Petri Nets. The same approach applies to CCSµ• .
– We show that FS - CCS! is decidable. The technique used in the proof issimulation base, originated from the technique of bisimulation base pioneeredby Caucal and widely used in decidability proofs of bisimilarity. Our proof
also makes use of expansion tree presented in [17] and the well-structured
transition system [8] for CCS! [4, 10]. In literature there are examples offormalisms [19] in which bisimilarity is decidable while similarity is not. We
are not aware of any examples showing that the opposite situation happens.
This result is more or less surprising.
The finite branching property guarantees that the bisimilarity can be approximated in the sense that P 6∼ Q if and only if P 6∼n Q for some n. The
approximation can also be applied to the similarity relation. It necessarily implies that all the problems in Fig. 2 are actually in Π10 . So we only need to show
Π10 -hardness to get Π10 -completeness. We remark that a relation R(x) is in Σ10(resp. Π10 ) in arithmetic hierarchy if it can be expressed by ∃y.S(x, y) (resp.
3

λ

λi
n
i=1 λi .Ei −→ EilE −→ E 0

a not appear in λλl

E −→ E 0

F −→ F 0τλE | F −→ E 0 | F 0

E | F −→ E 0 | F

λLocalization

E −→ E 0

Composition

Choice P

λFixpoint

E{µX.E/X} −→ E 0(a)E −→ (a)E 0

λµX.E −→ E 0

Fig. 3. Semantics of CCSµ∀y.S(x, y)) for some decidable relation S(x, y). Clearly R(x) is in Σ10 if and only
if its complement is in Π10 .
The rest of the paper is organized as follows. Section 2 lays down the preliminaries. Section 3 investigates the problems of deciding the strong bisimilarity on
the CCSµ processes and the CCS! processes. Section 4 considers the problem ofdeciding the strong bisimilarity/similarity between a CCS! /CCSµ process and afinite state process. Section 5 gives concluding remarks.
Most proofs and technical details are omitted. See [13] for complete coverage.

2

Basic Definition and Notation

To describe the interactions between systems, we need channel names. The setof the names N is ranged over by a, b, c, . . . , and the set of the names andthe conames N ∪ N is ranged over by l, . . .. The set of the action labels A =N ∪ N ∪ {τ } is ranged over by λ. To define the fixpoint operator and we need aset of process variables V ranged over by X, Y, Z.
The set ECCSµ of CCSµ terms is generated by the following grammar.
E ::= 0

| X

|

n
X

| E | E0

λi .Ei| (a)E| µX.E.

i=1

A name a appeared in a localization term (a)E is local. A name is global if it is
not local. The variable X in the fixpoint term µX.E is bound. A variable is free
if it is not bound. A CCSµ term containing no free variables is a CCSµ process.
In µX.E it is not required that X be guarded in E because unguarded recursion can be encoded P
by guarded recursion in CCSµ [10]. With guarded recursionnand guarded choice i=1 λi .Ei , finite branching property is guaranteed. Once
unguarded recursion is admitted, replication !P can be defined by the recursionµX.(X | P ).
The standard semantics of CCSµ is given by the labeled transition system(ECCSµ , A, −→), where the elements of ECCSµ are often referred to as states. The
relation −→ ⊆ ECCSµ × A × ECCSµ is the transition relation. The membershipλ(E, λ, E 0 ) ∈ −→ is always indicated by E −→ E 0 . The relation −→ is generated
inductively by the rules defined in Fig. 3. The symmetric rules are omitted.
4

Standard notations and conventions in process calculi will be used throughout the paper. The inactive process 0 is omitted in most occasions. For instancea.b.0 is abbreviated to a.b. A finite sequence (or Pset) of names a1 , . . . , an isnoften abbreviated to ea. The guarded choice termi=1 λi .Ei is usually written as λ1 .E1 + · · · + λn .En . Processes are not distinguished syntacticallyQn up tothe commutative monoid generated by ‘+’ and ‘ | ’. We shall write i=1 Pi for
P1 | . . . | Pn . The notation ‘≡’ is used to indicate syntactic congruence. We shallwrite PL for the set of the processes definable in L. The set of the derivativesof a process P , denoted by Drv(P ), is the set of the processes P 0 such that
λ

λ

n
1
P 0 for some n ≥ 0 and λ1 , . . . , λn ∈ A.
· · · −→P −→!
CCS is obtained from CCSµ by using the replication instead of the fixpoint
operation. The grammar is defined as follows:nX

P ::= 0 |λi .Pi| P |P0| (a)P| !P.

i=1

The operational semantics of the replication stated below is from [4, 5], whichenjoys the finite branching property.
lλP −→ P 0

P −→ P 0

Replication

λ!P −→ P 0 | !Pl

P −→ P 00

τ!P −→ P 0 | P 00 | !P

The advantage of the replication is that one could give a first order presentationof CCS. There is no need for process variables. This is why the above grammar
and rules are defined on the set of the processes, not on the set of the terms.
A binary relation R on PL is a strong simulation if, for each pair (P, Q) ∈ R,
P can be simulated by Q in the following sense:λλ

If P −→ P 0 , then Q −→ Q0 for some Q0 such that (P 0 , Q0 ) ∈ R.
A binary relation R is a strong bisimulation if both R and its inverse R−1
are strong simulations. The strong similarity - is the largest strong simulation,and the strong bisimilarity ∼ is the largest strong bisimulation. The former is apreorder and the latter is an equivalence.
Strong bisimilarity has a game theoretic characterization known as the bisimulation game. It is a complete-information dynamic game played by two players
named ‘attacker’ and ‘defender’. The labeled transition system (PL , A, −→) isperceived as a game-board. During the play the current position is described bya pair of states (P1 , P−1 ) ∈ PL × PL . The game is played in rounds. In eachround the players change the position according to the following rules:
1. The attacker chooses a state i ∈ {1, −1}, an action λ ∈ A, and some Pi0 ∈ PL
λsuch that Pi −→ Pi0 .
λ
00
2. The defender responds by choosing some P−i∈ PL such that P−i −→ P−i;00and then (P1 , P−1 ) becomes the current position of the next round.
If the defender never gets stuck, it wins. Otherwise the attacker wins. It is easy
to see that the defender has a winning strategy in the bisimulation game startingfrom the position (P, Q) if and only if P ∼ Q.
5

3

Undecidability of Strong Bisimilarity

This section aims at the undecidability of CCSµ ∼ CCSµ and CCS! ∼ CCS! . In
fact, by many-one reductions from the halting problem of Minsky Machines, it
can be shown that both CCSµ• ∼ CCSµ• and CCS!• ∼ CCS!• are Π10 -complete.
Two-register Minsky Machine is a well-known Turing complete computational model [25]. A Minsky Machine R has two registers r1 and r2 that canhold arbitrary large natural numbers. The behavior of R is specified by a sequence of instructions {(1 : I1 ), (2 : I2 ), . . . , (n − 1 : In−1 ), (n : halt)}. For eachi ∈ {1, . . . , n − 1}, the i-th instruction may be in one of two forms:- (i : Succ(rj )): The instruction adds 1 to the content of the register rj andi + 1 becomes the value of the program counter.
- (i : Decjump(rj , s)): If the content of the register rj is not zero, the instruction decreases it by 1 and i + 1 becomes the value of the program counter;otherwise s becomes the value of the program counter.
The configuration of R is given by the tuple (i; c1, c2) where i is the program
counter indicating the instruction to be executed, and c1,c2 are the current
contents of the registers. The computation of R is defined in a natural way via
a (finite or infinite) sequence of configurations starting from a certain initialconfiguration. Whenever the n-th instruction (known as the halting state) isreached, the computation terminates.
The halting problem of Two-register Minsky Machines, whose undecidability
is well-known, is formally stated as follows:
Problem: HaltingMinskyMachine
Instance: A Two-register Minsky Machine R.
Question: Does the computation of R terminate when R starts from the initialconfiguration (1; 0, 0)?

Lemma 1. HaltingMinskyMachine is undecidable. It is Σ10 -complete in thearithmetic hierarchy.
If a process calculus L is able to encode the computation of a Minsky Machinefaithfully, undecidability of L ∼ L can be obtained by a straightforward reduction
from HaltingMinskyMachine, which confirms that the i-th Minsky Machine
Ri does not halt if and only if the interpretation PRi of Ri is strongly bisimilar
to !τ . Recall that there is no such reduction for any calculi in Fig. 1 except for
CCSPdef .
In the rest of this section, we outline the reductions that demonstrate theundecidability of CCSµ• ∼ CCSµ• and CCS!• ∼ CCS!• .
3.1µ
Undecidability of CCSµ• ∼ CCS•

The idea is to construct a CCSµ• process which models a given Minsky Machine
R in a nondeterministic fashion. The encoding is nondeterministic because it introduces unfaithful computations which do not follow the expected behavior of6

R. Two slightly modified copies of the constructed process are taken for bisimilarity checking. The modifications guarantee that in the bisimulation game,whenever the attacker takes the ‘unfaithful’ move at some round, the defender
have the ability to punish the attacker by moving to a pair of trivially bisimilarstates. Thus the attacker are ‘forced’ to take the ‘faithful’ move at each roundand the defender will lose the game if R ever halts. This technique is known as‘Defender’s Forcing’ [14, 18].
The construction is motivated by a construction in [17]. For convenience
constant definitions are used instead of µ-operations. Since localization operator
must not appear underneath any µ-operations, no confusion will arise. Twoslightly modified copies are given directly instead of describing the encoding in
advance.
Let R be an instance of HaltingMinskyMachine whose instruction set is{(1 : I1 ), (2 : I2 ), . . . , (n − 1 : In−1 ), (n : halt)}. Without using the localization
operator the processes {Pi }ni=1 and {Qi }ni=1 are defined as follows:
def

def

– Pi = incj .Pi+1 and Qi = incj .Qi+1 if the i-th instruction is (i : Succ(rj )).
– If the i-th instruction is (i : Decjump(rj , s)), then let
def

Pi = decj .d.Pi+1 + zeroj .(tt.z.Ps + ff.z.Qs ),def

Qi = decj .d.Qi+1 + zeroj .(tt.z.Qs + ff.z.Ps ).
def

def

– Pn = halt.0 and Qn = 0 for the n-th instruction (n : halt).
The processes {Pi }ni=1 and {Qi }ni=1 are two families of slightly different processes
that interpret the instructions of R. Special attention should be paid to thegadget ff.z.Qs (or ff.z.Ps ) in the defining equation of Pi (or Qi ) for instruction(i : Decjump(rj , s)). This gadget is designed to ‘force’ the attacker to stick to
the faithful moves. Also notice that the only asymmetry between Pi ’s and Qi ’s
is that Pn can perform a special action halt whereas Qn cannot.
The processes P seudoCounterj (k), for j ∈ {1, 2}, introduced below are used
to partially model the registers of R.
def

P seudoCounterj (k) = Cj | Cj | . . . | Cj | Oj ,
|
{z
}
k

where Oj and Cj are defined as follows without using the localization operation:def

Oj = incj .(Cj | Oj ) + zeroj .tt.Oj ,def

Cj = decj .0 + zeroj .ff.Cj .
The process P seudoCounterj ’s are the weak forms of the counter, for they lackthe ability to zero-test — they can make a ‘zero’ move while the actual value ofthe counters are positive. However P seudoCounterj ’s are good enough for the
purpose of deriving the undecidability results we want.
7

Finally every configuration of R is modeled by the following two slightly
different processes.
def f
f zero)(tt)(ff)g
Conf igP (i; c1 , c2 ) = (inc)(dec)((Pi | P seudoCounter1 (c1 ) | P seudoCounter2 (c2 )),def f
f zero)(tt)(ff)g
Conf igQ (i; c1 , c2 ) = (inc)(dec)((Qi | P seudoCounter1 (c1 ) | P seudoCounter2 (c2 )).
The correctness of the above encoding is guaranteed by Lemma 2, Lemma 3,
and Lemma 4, which eventually lead to Theorem 1.
Lemma 2. Let (i; c1, c2) be a configuration of R and (i : Succ(rj )) be the i-th
instruction. Then there is a unique continuation of the bisimulation game fromthe pair of processes Conf igP (i; c1 , c2 ) and Conf igQ (i; c1 , c2 ) such that, after
one round, the players reach the pair Conf igP (i; c01 , c02 ) and Conf igQ (i; c01 , c02 )where c0j = cj + 1 and c03−j = c3−j .
Lemma 3. Let (i; c1, c2) be a configuration of R and (i : Decjump(rj , s)) be
the i-th instruction. Assume that a bisimulation game is played from the pair
Conf igP (i; c1 , c2 ) and Conf igQ (i; c1 , c2 ). The followings hold:(a) If cj = 0, then there is a unique continuation of the game such that after threerounds, the players reach the pair Conf igP (s; c1 , c2 ) and Conf igQ (s; c1 , c2 ).
(b) If cj > 0 and the attacker chooses the τ action induced by the synchronization
via channel decj , then the defender has a way to continue the game suchthat, after two rounds, Conf igP (i; c01 , c02 ) and Conf igQ (i; c01 , c02 ) are reached,
where c0j = cj − 1 and c03−j = c3−j . If the defender does not play in this way,
there is a way for the attacker to win the game.
(c) If cj > 0 and the attacker chooses the τ action induced by the synchronization
via channel zeroj , then there is a way for the defender to win the game.
Lemma 4. The execution of R from the configuration (1; 0, 0) terminates if andonly if Conf igP (1; 0, 0) 6∼ Conf igQ (1; 0, 0).
Theorem 1. Both CCSµ• ∼ CCSµ• and CCSµ ∼ CCSµ are Π10 -complete.
3.2

Undecidability of CCS!• ∼ CCS!•

The result established in Section 3.1 does not immediately imply the same result
for CCS! /CCS!• . A well known fact is that recursion can be turned into replication [26, 11] by the encoding J K whose nontrivial part is given by JXi K = ai .0 andJµXi .EK = (ai )(ai | !ai .JEK), where names ai ’s are fresh. However this encoding
does not give rise to a strong bisimulation. Another problem is that an encoding
from CCSµ to CCS! would not always produce an encoding from CCSµ• to CCS!•
automatically since they introduce additional local names.
Undecidability of CCS!• ∼ CCS!• does not rely on the existence of such an
encoding. The basic idea and the construction in Section 3.1 can be repeated8with subtle modifications. The intuition of the next encoding is to interpret every
instruction of a Minsky Machine R by a process of the form !addr.opr, where addr
should be understood as the address of the instruction and opr the operation of
the instruction. The difficulty is to guarantee that only a finite number of local
channels are necessary. In the following definition 2n extra static local channels{instiP , instiQ }ni=1 are used.
– If the i-th instruction is (i : Succ(rj )), let
def

def

Pi = !instiP .incj .insti+1
P ,Qi = !instiQ .incj .insti+1
Q .

– If the i-th instruction is (i : Decjump(rj , s)), letdef

Pi = !instiP .(decj .d.insti+1+ zeroj .(tt.τ.τ.z.instsP + ff.ack.z.instsQ )),
P
def

s
s
Qi = !instiQ .(decj .d.insti+1
Q + zeroj .(tt.τ.τ.z.instQ + ff.ack.z.instP )).

– For the n-th instruction (n : halt), let
def

def

Qn = !instnQ .0.

Pn = !instnP .halt.0,

In the following modification of P seudoCounterj (k), {mj }2j=1 and ack are theonly extra local channels introduced.
def

P seudoCounterj (k) = Cj | Cj | . . . | Cj | Oj | !mj .ack.Cj ,
{z
}
|
k

def

def

where Oj = !(incj .Cj + zeroj .tt), and Cj = decj + zeroj .ff.mj . When zeroj is
triggered on some Cj , channel mj is used to require a new copy of Cj fromthe resource !mj .ack.Cj , and after that, the channel ack ais used to inform theprocess that triggers the action zeroj . Such treatment will make the whole systemsequential. As a side-effect it will take two more computation steps when the zerotesting is unfaithfully chosen by the attacker, and for the defender, two extra
τ ’s are introduced into the definition of Pi and Qi . The configuration (i; c1 , c2 )of R is interpreted by the following two processes:
def g ff zero)(g m)(tt)(ff)(ack)eConf igP! (i; c1 , c2 ) = (inst)(inc)(dec)(


n
n
2
Y
Y
Y
instiP |Pi |Qi |P seudoCounterj (cj ) ,
i=1

i=1

j=1

def g f!
f zero)(g m)(tt)(ff)(ack)eConf igQ(i; c1 , c2 ) = (inst)(inc)(dec)(


n
n
2
Y
Y
Y
instiQ |Pi |Qi |P seudoCounterj (cj ) .
i=1

i=1

j=1

Using the same argument as in Section 3.1 we can prove the following.
Theorem 2. Both CCS!• ∼ CCS!• and CCS! ∼ CCS! are Π10 -complete.
94Strong (Bi)similarity on Finite State Processes

We investigate in this section the decidability of strong bisimilarity/similarity
between a CCS! /CCSµ process and a finite state process.
4.1

Undecidability of CCS! ∼ FS

The general problem CCS! ∼ FS is undecidable. This result depends on the construction of Busi et al in Section 3 of [5], where Minsky Machines are encoded
by CCS! processes in a nondeterministic fashion. Using this encoding, one canshow that if a Minsky Machine R does not halt, the encoding of R is a CCS!
process strongly bisimilar to !τ , which cannot perform any visible actions and isdivergent in every computation branch. If R does halt, the encoding of R has atleast one divergent computation branch. This fact leads to Theorem 3.
Theorem 3. The strong bisimilarity between a process P ∈ PCCS! (or P ∈PCCSµ ) and a fixed finite state process F ∈ PFS is Π10 -complete.
It is worth noting that Theorem 1 of [5] confirms that the Minsky Machine R
halts if and only if R is interpreted as a CCS! process P satisfying P ≈ τ.P +halt,
which establishes the Σ10 -hardness of the weak bisimilarity checking problem of
CCS! . An interesting question is how to establish the Π10 -hardness of CCS! ≈ FS.
It is widely believed that checking weak bisimilarity is harder than checking thestrong bisimilarity. However the above construction does not immediately offer
an answer to the latter problem.
4.2

Decidability of CCS!• ∼ FS

Although both CCS! ∼ FS and CCSµ ∼ FS are undecidable in the general case,their restricted versions, CCS!• ∼ FS and CCSµ• ∼ FS, turn out to be decidable.
These results are motivated by the following observations.
Q Suppose P ∈ PCCS!•
or P ∈ PCCSµ• . We may assume that P is of the form (ã) i∈I Pi in which e
a are
all the local Q
names of P and every Pi is localization free and is not a composition.
We call (ã) i∈I Pi a concurrent normal form of P , and every Pi a concurrent
component of P . The key opoint is that no local names can be produced during
the evolution of P , and the number of the possible concurrent components of allderivatives of P must be finite.
Based on the above observations, a strongly bisimilar encoding from CCS!•(or CCSµ• ) to the Labeled Petri Net is constructed. With the help of the resultsof Jančar et al. [16], we know that the same problem for the Labeled Petri Net
is decidable. Hence the decidability of CCS!• ∼ FS and CCSµ• ∼ FS.
Definition 1. A Petri Net is a tuple N = (Q, T, F, M0 ) and a Labeled Petri
Net is a tuple N = (Q, T, F, L, M0 ), where Q and T are finite disjoint sets ofplaces and transitions respectively, F : (Q × T ) ∪ (T × Q) → N is a flow function
and L : T → A is a labeling. M0 is the initial marking, where a marking M isa function Q → N assigning the number of tokens to each place.
10

t

A transition t ∈ T is enabled at a marking M , denoted by M −→, if M (p) ≥F (p, t) for every p ∈ Q. A transition t enabled at M may fire yielding thetmarking M 0 , denoted by M −→ M 0 , where M 0 (p) = M (p) − F (p, t) + F (t, p) forλλall p ∈ Q. For each λ ∈ A, we write M −→, respectively M −→ M 0 to meanttthat M −→, respectively M −→ M 0 for some t with L(t) = λ.
In the above definition A is the set of the action labels. A Labeled PetriNet N can be viewed as a labeled transition system (M, A, −→) with M being the markings of N . Strong bisimilarity is defined accordingly. Suppose Q ={S1 , S2 , . . . , Sn } is the finite set of places. Labeled transition rules of the form
λ

m0

m0

m0

S1m1 S2m2 . . . Snmn −→ S1 1 S2 2 . . . Sn n are used to indicate that there is a transition t whose label is λ and the flow function for t is defined by F (Si , t) =mi and F (t, Si ) = m0i for every i = 1, . . . , n. A marking M is denoted by
M (S ) M (S )M (S )
S1 1 S2 2 . . . Sn n , which can be viewed as a multiset over Q. Thus N
is specified by (Q, A, Tr, M0 ), where Tr is the set of the labeled transition rules.
The next lemma is due to Jančar and Moller [16].
Lemma 5. The strong bisimilarity between a marking M0 of a Labeled PetriNet N and a finite state process F ∈ PFS is decidable.
To describe the encoding from CCS!• to the Labeled Petri Net, we need thefollowing definitions and lemma, borrowed from [10].
Definition 2. Suppose the PCCS! process P does not contain any local names.
The concurrent subprocesses of P , notation Csub(P ), is defined inductively bydefCsub(0) = ∅,def

Csub(P 0 | P 00 ) = Csub(P 0 ) ∪ Csub(P 00 ),
n
n
X
X
[
def
Csub(
λi .Pi ) = {λi .Pi } ∪CSub(Pi ),
i=1

i=1
0

def

i∈I

0

Csub(!P ) = {!P } ∪ Csub(P 0 ).
def

Clearly if P ≡ (a)P 0 is in concurrent normal form, then Csub(P ) = Csub(P 0 ).
Lemma 6. For every process P of CCS!• in concurrent normal form, Csub(P )is finite, and for every P 0 ∈ Drv(P ), Csub(P 0 ) ⊆ Csub(P ).
def

By letting Csub(µX.E) = {µX.E} ∪ Csub(E{µX.E/X}), the counterpartof Lemma 6 for CCSµ• can be established. Now an encoding from the concurrent
normal forms of CCS!• or CCSµ• to the Labeled Petri Net is given in the proof of
Lemma 7.
Lemma 7. There is an algorithm such that, given process P ∈ PCCS!• (or P ∈PCCSµ• ) in concurrent normal form, it outputs a Labeled Petri Net NP with thesame set of the action labels and P ∼ NP .
11

Q
Proof. Let Csub(P ) = {Ci | i ∈ I} and P = (ã)( i∈I Cini ). The Labeled
Petri Net NP = (Q, A, −→, M0 ) is defined as follows. The set of the places is
def
def Q
Q = {[Ci ] | i ∈ I} and the initial marking is M0 = i∈I [Ci ]ni . The transition
rules are defined inductively:
λ Q
λ Q
n
– If Ci −→ j∈I Cj j , then [Ci ] −→ j∈I [Cj ]nj is a rule provided that λ 6∈ m̃.
Q
Q
l
l
τ
mj
nj
– If Ci1 −→and Ci2 −→j∈I Cjj∈I Cj , then [Ci1 ][Ci2 ] −→Q
mj +njis a rule.
j∈I [Cj ]The remaining work is to confirm thatYY{((ã)( Cini ), [Ci ]ni ) | ni ≥ 0 for i ∈ I)}
i∈I

i∈I

t
u

is a bisimulation.
The combination of Lemma 7 and Lemma 5 produces the following.

Theorem 4. The strong bisimilarity between a process P ∈ PCCS!• (or P ∈PCCSµ• ) and a finite state process F ∈ PFS is decidable.
4.3

Decidability Results of Simulation PreorderThis part focuses on the problems L - FS and FS - L. In the case that L is
CCS!• or CCSµ• , the decidability result can be obtained via the same encoding
provided in Section 4.2 with the help of the results already known for the Labeled
Petri Net stated in Theorem 3.2 and Theorem 3.5 of [16].
Theorem 5. FS - CCS!• , FS - CCSµ• , CCS!• - FS, CCSµ• - FS are decidable.
Now let’s turn to CCS! or CCSµ . It has been suggested that the similarity
checking is computational harder than the bisimilarity checking. This point is
supported by two general proof methods applied to many process classes in apaper by Kučera and Mayr [19]. These two proof methods however cannot be
used to show similar results for CCS! or CCSµ . As a matter of fact we will provethat FS - CCS! is decidable, despite of the fact that FS ∼ CCS! is undecidable
by Theorem 3.
Our proof makes use of simulation bases. A simulation base is a finite subsetof - consisting only of ‘crucial’ similar pairs from which a possibly infinite simulation relation can be produced algorithmically. Similarity will be decidable if
simulation bases can be effectively constructed. For more on this technique, thereader is referred to [3, 17, 18].
In order to get a simulation base, we shall make good use of the wellstructured transition system [8] of PCCS! , which was first pointed out by Busi etal in [4]. Here we follow the definition from [10] with slight amendment.
Definition 3. A well quasi order (X, ≤) is a preorder such that, for every infinite sequence x0 , x1 , x2 , . . . in X, there exist indexes i < j such that xi ≤ xj .
12Definition 4. The structural expansion 4 on the CCS! processes is definedinductively as follows:– P 4 Q whenever Q ≡ P | R for some R;– (a)P 4 (a)Q whenever P 4 Q;
– P 4 Q whenever P ≡ P1 | P2 , Q ≡ Q1 | Q2 , P1 4 Q1 and P2 4 Q2 .
Notice that Definition 4 works up to structural congruence. Intuitively P 4 Q
means that Q contains at least as many possible individual processes runningconcurrently as P . The relation 4 is transitive. Due to the syntactical natureof the definition, 4 is decidable. The next two technical lemmas, due to Busiet al, are crucial to the effective production of the simulation bases. The proof
of Lemma 8 is straightforward. For a detailed proof of Lemma 9, one may consult [10].
Lemma 8 (Compatibility Lemma). Suppose that P ,Q are CCS! processes.
λλ

If P 4 Q and P −→ P 0 , then Q0 exists such that Q −→ Q0 and P 0 4 Q0 .
Lemma 9 (Expansion Lemma). Let P ∈ PCCS! , then (Drv(P ), 4) is a wellquasi order.
Using the techniques and lemmas discussed above, one can infer the following
main result of the section.
Theorem 6. FS - CCS! is decidable.

5

Concluding Remark

Summary. We have studied several decidability and undecidability issues on
the bisimilarity and similarity checking problems of some subcalculi of CCS.
We have concentrated on the question of how the solutions are affected when
the capability of producing and manipulating local channels becomes weaker.
An instance is identified that similarity checking is decidable while bisimilarity
checking is not. Fig. 4 summarizes the status quo of our understanding of thedecidability property. These results offer a different angle to look at the relative
expressiveness of the subcalculi of CCS.
Related Work. The relative expressiveness of CCS is studied in [4, 5, 11, 6, 10,2]. It is proved in [5, 11] that CCS! and CCSµ are less expressive than CCSPdef .
Two problems are left open in [11, 2]. Both are answered in [10]. One answer
is given by an encoding from CCSµ to CCS! that is codivergent and branchingbisimilar. The other is by an encoding from CCSµ to itself with only guarded
recursion. A more formal approach to the expressiveness study is proposed in [9].
In [15] the bisimilarity checking problem between the infinite-state processes andthe finite-state ones is reduced to the model checking problem of reachability ofHennessy-Milner property. A recent survey on the decidability and complexity
results of bisimilarity checking for the processes defined in Process Rewrite Systems [21] is given in [27]. A surprising result is pointed out in [20] that strong
13

L

L∼L

L ∼ FSFS - LL - FS

CCS!◦
X [7]
X [7]
X
X
CCSµ
X [7]
X [7]
X
X
◦
CCS!•
× (Th.2) X (Th.4) X (Th.5) X (Th.5)
CCSµ× (Th.1) X (Th.4) X (Th.5) X (Th.5)•
CCS!
×× (Th.3) X (Th.6)?
CCSµ×× (Th.3)?
?
CCSPdef × [4, 11] × [4, 11] × [4, 11] × [4, 11]“∼”: strong bisimilarity“-”: strong similarity“X”: known decidable“×”: known undecidable“?”: unknown

Fig. 4. Summary of the Results

bisimilarity is decidable for a higher-order calculus. The Petri Net semantics is
proposed in [12] for CCSµ◦ with guarded recursion. In [2] a similar encoding of
CCS!◦ into the Petri Nets is presented. Our results assert the nonexistence of
reasonable encodings from CCS! /CCSµ to the Labeled Petri Net. The interplay
between CCS! and the Chomsky Hierarchy are studied in [1].
Future Work. Recently we have attempted to set up an expansion order for
CCSµ , which we hope would help us prove the decidability of FS - CCSµ . The
problem CCS! - FS is interesting. It appears undecidable, but nothing seems
to indicate that a positive answer is unlikely. Finally notice that the number ofthe static local channels used to show Theorem 1 is bounded, whereas we havenot got such a bound for Theorem 2. This may suggest that CCSµ• cannot be
encoded into CCS!• .
Acknowledgements The authors are indebted to all the anonymous referees
for their detailed reviews on the previous version of the paper. Their criticisms,
questions and suggestions have led to a significant improvement of the paper.

References
1. Jesús Aranda, Cinzia Di Giusto, Mogens Nielsen, and Frank D. Valencia. Ccs
with replication in the chomsky hierarchy: The expressive power of divergence. In
APLAS, pages 383–398, 2007.
2. Jesús Aranda, Frank D. Valencia, and Cristian Versari. On the expressive powerof restriction and priorities in ccs with replication. In FOSSACS, pages 242–256,
2009.
3. Olaf Burkart, Didier Caucal, Faron Moller, and Bernhard Steffen. Verification on
infinite structures. In Handbook of Process Algebra, pages 545–623, 2001.
4. Nadia Busi, Maurizio Gabbrielli, and Gianluigi Zavattaro. Replication vs. recursive
definitions in channel based calculi. In ICALP, pages 133–144, 2003.
5. Nadia Busi, Maurizio Gabbrielli, and Gianluigi Zavattaro. Comparing recursion,
replication, and iteration in process calculi. In ICALP, pages 307–319, 2004.
6. Nadia Busi, Maurizio Gabbrielli, and Gianluigi Zavattaro. On the expressive powerof recursion, replication and iteration in process calculi. Mathematical Structuresin Computer Science, 19(6):1191–1222, 2009.

14

7. Søren Christensen, Yoram Hirshfeld, and Faron Moller. Decidable subsets of CCS.
Comput. J., 37(4):233–242, 1994.
8. Alain Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere!
Theor. Comput. Sci., 256(1-2):63–92, 2001.
9. Yuxi Fu. Theory of interaction. 2010. http://basics.sjtu.edu.cn/~yuxi/.
10. Yuxi Fu and Hao Lu. On the expressiveness of interaction. Theor. Comput. Sci.,
411(11-13):1387–1451, 2010.
11. Pablo Giambiagi, Gerardo Schneider, and Frank D. Valencia. On the expressivenessof infinite behavior and name scoping in process calculi. In FoSSaCS, pages 226–
240, 2004.
12. Ursula Goltz. CCS and petri nets. In Semantics of Systems of Concurrent Processes, pages 334–357, 1990.
13. Chaodong He, Yuxi Fu, and Hongfei Fu.
Decidability of behavioural equivalences in process calculi with name scoping.
2010.
http://basics.sjtu.edu.cn/~chaodong/.
14. Petr Jancar and Jirı́ Srba. Undecidability of bisimilarity by defender’s forcing. J.
ACM, 55(1), 2008.
15. Petr Jančar, Antonı́n Kučera, and Richard Mayr. Deciding bisimulation-like equivalences with finite-state processes. Theor. Comput. Sci., 258(1-2):409–433, 2001.
16. Petr Jančar and Faron Moller. Checking regular properties of petri nets. In CONCUR, pages 348–362, 1995.
17. Petr Jančar and Faron Moller. Techniques for decidability and undecidability ofbisimilarity. In CONCUR, pages 30–45, 1999.
18. Antonı́n Kučera and Petr Jancar. Equivalence-checking on infinite-state systems:
Techniques and results. TPLP, 6(3):227–264, 2006.
19. Antonı́n Kučera and Richard Mayr. Why is simulation harder than bisimulation?
In CONCUR, pages 594–610, 2002.
20. Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, and Alan Schmitt. On the expressiveness and decidability of higher-order process calculi. In LICS, pages 145–155,
2008.
21. Richard Mayr. Process rewrite systems. Inf. Comput., 156(1-2):264–286, 2000.
22. Robin Milner. Communication and concurrency. Prentice-Hall, 1989.
23. Robin Milner. Communicating and Mobile Systems: the π-calculus. Cambridge
University Press, 1999.
24. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes.
Inf. Comput., 100(1):1–77, 1992.
25. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, 1967.
26. Davide Sangiorgi and David Walker. PI-Calculus: A Theory of Mobile Processes.
Cambridge University Press, 2001.
27. Jiřı́ Srba. Roadmap of Infinite results, volume Vol 2: Formal Models and Semantics.
World Scientific Publishing Co., 2004.
28. Dirk Taubner. Finite Representations of CCS and TCSP Programs by Automata
and Petri Nets, volume 369 of Lecture Notes in Computer Science. Springer, 1989.

15