Towards a Theory of Bisimulation for the Higher-Order Process Calculi

May 2004, Vol.19, No.3, pp.352- 363J. Comput. Sci. & Technol.Towards a Theory of Bisimulation for the Higher-Order ProcessCalculiYong-Jian Li and Xin-Xin LiuLaboratory of Computer Science, Institute of Software, The Chinese Academy of Sciences, Bcijing 100080P.R. China .E-mail: lyj238@ios.ac.cnReceived December 25, 2002; revised September 12, 2003.Abstract In this paper, a labelled transition semantics for higher-order process calculi is studied. The labelledtransition semantics is relatively clean and simple, and corresponding bisimulation equivalence can be easilyformulated based on it. And the congruence properties of the bisimulation equivalence can be proved easily.To show the correspondence between the proposed semantics and the well-established oncs, the bisimulation ischaracterized as a version of barbed equivalence and a version of context bisimulation.Keywords higher order process, labelled transition semantics, barbed bisimulation, context- bisimulation1 Introductioncated the definition of labelled transition relation.The second problem is the meaning of the label ofLabelled semantics achieved great success inhigher order output action in traditional LTS. Itearly studies of process calculi. Based on lblled only takes into account the object that the processsemantics, the idea of bisimulation was introduced emits, but not the context in which the emittedand formulated by Miner and Parkl,2 and has be- object is supposed to be used. For example, let uscome one of the most important notions in pro-consider an output action in HOπ's LTS[5].cess calculi. In mobility-free calculi such as cCsl3P v远(K), p'which has later become a blueprint for new processcalculi, a labeled transition system describes the where vca(K) represents the output object of P,operational behaviors of processes, and bisimula and P' represents the derivative of P. And thetion is defined on top of the labeled transition sys- whole transition rule does not contain any infor-tem (LTS) by imposing the following requirement: mation about the context in which emitted objecttwo processes are bisimilar if any action by one of is supposed to be used.ther can be matched by an equal action from theThis traditional higher order output transitionother in such a way that the resulting derivatives will cause the non naturalness problems in the def-are again bisimilar. Note that two matching actions inition of bisimulation. In more detail, when defin-must be syntactically identical. It is reasonable in ing some kind of bisimulation R of two examplefirst-order process calculus, because the effect of processes P, Q, we cannot use the traditional clausethe first-order object on the enviroument can be as below to define the matching of the higher-orderentirely represented by its syntax form.output actions of the two processes.When moving to more powerful process calculi●Whenever P与P', then Q' existss.t. Q牛Q'with mobility and higher order features, the tra- and P' RQ', where μ is a higher-order output ac-ditional labelled semantics become hard to work tion.(1with, and corresponding bisimulation formulationsUnlike first- order output action, the compari-are often much more elaborated, resulting in less son of labels of high order output action, for exam-satisfactory theories. It seems that two problems ple, processes, cannot be based on syntactic iden-have made traditional labelled semantics difficult tity in formulation of bisimulation, that would befor richer process calculi. The first is passing of too strong for any reasonable sernantic equivalence.local names out of the scope where they are deThomsen used bisimilarity instead of identity infined. The scope extrusion rule was introduced comparing labelslo), following earlier ideas of Aste-to cope with this4, but some delicate structure siano and Boudol[r别), but the resulting equivalencewas also introduced into the labels, which compli-is still too strong.*CorrespondenceThis work is Bupported by the National Natural Science Foundation of China under Grant No.60173020.中国煤化工MYHCNMHGYong-Jian Li et al: Towards a Theory of Bisimulation for the Higher Order Process Calculi353Sangiorgi had some very ilustrative examplesidea can be successfully applied to higher orderof the problems in his dissertationsl5. And heprocess calculi. In our labelled transition seman-pointed out that the separation between the ob-tics, there are three kinds of labels: T, a(U).q,ject part (i.e, the process emitted) and the con-a(K).0. As usual, P与P' represents internal com-text of a higher-order output prevents a satisfac-munication as traditional LTS. However p*OYp'tory treatment of the channels private to the two,and p4R2) P' represent that P can respond to theand then causes the problems of higher order bisim-ulation mentioned above. To avoid this separation tets a(V).Q and (K>.0 from context rspectivelyebetween object part and context of an output ac-and then becomes P'. We will show that our la-tion, he proposed a context bisimulation as belowbelled transition semantics are relatively clean andwhich explicitly takes into account the context inthe corresponding bisimulation equivalence can bewhich the emitted object is supposed to be used.easily obtained.To show the correctness and rationality of ourWhenever P IDOa\h14P', then Q' ex-semantics, we want to show the correspondenceists s.t.Q welakz+Q' and for all PG withbetween our labelled semantics and those well-fn(PG)n(6u2) = 0, (ub)(P'PG{K/U})R estabished. First, we want to relate our LTS with(ue)(Q'|PG{K2/U})-(2reduction semantics. And we will characterize ourBut this style of context bisimulation still seemsnew bisimulation in terms of a version of barbednon-natural and complex. First, the clauses of theequivalence. Second, we relate our LTS semanticsdefinition of bisimulation are not defined in a uni-to Sangorigi's LTS. And our new bisimulation willform style. The clause, which defines matching be-be characterized in terms of a version of contexttween higher-order output actions of two processes,bisimulation defined in his LTS.The rest of the paper is organized as follows.is different from other clauses. Especially, the prin-Section 2 reviews the syntax of the calculus thatciple that underlies the definition of matching ofwill be considered in this paper. Section 3 speci-higher-order output actions adopts the contextualfies the contextual labelled transition semantics forview, which is defined as the clause (2); on the otherthe calculus. Sections 4 and 5 will show the correhand, the definition of matching of first-order out-spondence between our labelled transition seman-put actions adopts the non-contextual view whichtics and reduction semantics and the traditional la-is defined as the clause (1). Second, this contextbelled transition semantics. Section 6 is the con-bisimulation is very complex. When he showed theclusion and related work.correspondence between his context bisimulationand a version of barbed equivalence, the proof istoo complex(5].2 SyntaxIn [9), Sewell introduced the contextual pointThe language we explored is similar to theof view of labelled semantics and opened up a newsecond-order fragment of reduced HOπ proposedalternative towards the solution to the above prob-in [5] by Sangiorgi, which satisfes the following relems. He pinpointed the connection between la-strictions: 1) all arities are uary, 2) each processbelled semantics and reduction semantics by mak-is finitely describable, 3) only guarded choices areing explicit the intuition that labelled transitionspermitted, 4) only processes are allowed to trans-capture the possible interactions between a termmit. In this calculus replication may be avoidedand a surrounding context. Roughly his idea isbecause recursion and replication can be simulatedthat labels of transitions from a process P will beusing restriction and parallel composition in ourcontexts that, when put together with P, createcalculus, as shown by Thomsenl6. We still thinkan occurrence of a reduction rule.As a test ofit is convenient for us to have replication explicitly,the idea, he it is shown that the new definition ofand its presence does not complicate our theory.labelled transition induces the same bisimulationAnd we use K, L,P, Q, R如range over processes;for a fragment of ccs. Notice that the key difera, b, ...., to range over names; U, V, X, Y toence between Sewell's contextual transition labelrange over variables. The syntax is as follows:and traditional transition label is in that the formercomes from the process that performs the action,P:= 2 f{a;:P|i∈}P|P}|vaP|X|!Pbut the latter comes from the process environmenta:: = a(P)|a(X)(or context).In this paper we want to show that the sameAs usual, we write P{Q/X} for the capture-中国煤化工MYHCNMHG354J. Comput. Sci. & Technol, May 2004, Vol.19, No.3avoiding higher-order substitution of Q for the P and Q are syntactically identical.free occurrences of X in P, fn(P)(fv(P)) forthe set of free names (variables) occurring in P,n(P)( Vars(P)) for the set of names (variables) ocSemanticscurring in P. We write Pr for the set of all theprocesses, Pre for the set of all closed processes, NThe labelled transition relation is given by thefor the set of all names. For convenience, we shall rules in Fig.1, together with the rules for the aux-treat processes that are a-equivalent as syntacti-iliary relation ↓used in the side condition for com-cally identical processes. And P= Q means that munication rule.nput: (l(a().R..}的(K2:P{K/U} Output: (.({...}.. PIQ{K/U}Coml:p(U)-9 R(P'↓a(U).Q)Comr:p*(W:8PP"+RP'|P与RParl:P9 p'Parr:Q SQ'PIQ 9 PIQPIQ 9 P|Q'Re:- pSP';(e史fn(a))Rep-Act:_P4P've.P 9 ve.P!PS Pl|IPp(U)8R(P↓a(V).Q)(x0.......↓a(U).P!P 5 R|!PP↓a(U).P'(c≠a)(U fo(Q))vcPta(U).nePlIgt a(U.(P"lQ)Q1a(U.Q'(U t fv(P))PIQ↓a(U).(PlQ)IP I a(U).(P"I!P)Fig.1. Rules for labelled transitions.In the labelled transition there are three P|!P9 P'we use the transition rules Rep-Actkinds of labels: r,a(U).Q, a(R).0. As expected!P$ P'P 4 p' represents internal communication. How- and Rep-Comm for replication operator. The rea-ever p(U)8p' and P可(R)0 pr represent that Pson is that the relations斗are image finite in ourcan respond to the tests a(U).Q, and a(R).0 respec-semantics if we adopt the latter approach. Thetively, and then becornes P'. If the first still hasinterested reader can see [10] for a discussion re-some trace of carly transition semantics for inputgarding image finiteness.actions, the second is quite diferent from the usualWith this labelled transition relation the notionunderstanding of the labels. From the rule for re-of bisimulation can be given in the usual way.striction we can see that one advantage of adoptingDefinition 1. A binary relationRS PrcX Prcthis point of view is that now we can avoid thesub is a simulation ifP R q implies that whenevertle notion of scope extrusion, since here the labels P 与P', then there existsQ' such thatQ与Q'are from the environment, not from within P.and P'R q'; where μ is of the form T, a(U).Q,The aziliary predicate P↓a(U).P' says that a(R).0.P can provide the test a(U).P'. In this case it is theA relation R is a bisimulation if both R andsame as the conmitment predicate in [10]. Mostof R-1 are simulations. We say that P, Q are bisim-the rules explain themselves. The communication ilar, written as P~ Q if thereis P R Q for somerulebisimulation积.Definition 2 (Bisimulation for Open Pro-p a(U).日RP|PrFR(P'↓a(U).Q) .cesses). For processes P1, P2 with free variablesfv(P)∪f0(P)∈{&}, we set P ~ Bz iffor .says that if P can react to the test a(U).Q andall closed processes q, it holds that P{Q/x} ~becomes R, and P' can provide the test, then by P2{Q/X}.putting them in parallel the system can do an in-Lemma 1. ~ is an equivalence relation.ternal communication and becomes R.The notion of bisimulation up to ~ is very use-Instead of using the single transition rule REP ful in many bisimulation proofs. We introduce it in中国煤化工MYHCNMHGYong-Jian Li et al: Towards a Theory of Bisimulation for the Higher-Order Process Calculi355the following lemma which is easy to prove.bn(vbC) = bn(C)U {b}Lemma2. LetR∈Prx Pr be such that PRbn(!C) = bn(C)Q implies:The following lemma says that if a program R1) whenever P号P', then there exists Q' suchcan react to the test a(U).S, and becomes R', thenthatQ °Q' andP'~ R~Q'2) whenever q9Q', then there exists P' suchR and R' should be of special kind of forms. Thelemma will be used in the proof of Lemma 5. .thatP°→P' andP'~R~Q'.a(U).SThen ~ R ~ is a bisimulation. We call such RLemma4. IfR°°R', then1) thene erist a static contert C, a non-replica-a bisimulation ψ to ~.tion context C' and two processes K, S' such thatNext we will explore somne property of ~Theorem 1 (Properties of ~) The follow-R= C[2 (a(K).S')], R' = C"[S'|S{K/U}];2) moreover, ifC is a non-replication context,ing equivalence holds:1) E{a;Pl|i∈I}~ E{aj.Pj|j∈J},ijJ is .thenC=C';3) ra(O)TC[$'T{K/U}] for any T sucha permutation of I;2) (PIQ)R ~ P(Q|R), P|Q~ Q|P,P|0~P;that bm(C)∩fn(T)= 0.3) vx0~ 0; vxvy P~vyvx P; (vx P)|q~ vx .Proof. By induction on the tree to derive(P|Q), i工在fn(Q); .Ra0S R', and by case analysis on the last rule4)! P~ P!IP.of the tree.Example 1. 1) Consider P = a(0)>.0, Q =Case 1. The last rule is the Output. Then R =(vx)a(3<0)>.0>.0, then we have P~ Q. Let .E(a(K).S') for somea, K, S'.Let C =C"=[.R= {(P,Q)}U {(R{0/X},(vx)R{元(0) .0/X})Obviously 1} and 2) hold.|R is a process such that $史fn(R)}, obviouslyCase 2. The last rule is the Parl, Parr, Res.RUR-1 is a bisimulation up to ~Simple.2) Consider P =. (x)(0)0)x(U)U， Case 3. The last rule is the Repl-Act. Then2 = (x)().x(U).U, then we have P必Q.R =!Ro for some Ro. Anda(U).S、Because pA4(vx)(x(U).U|@(0).0) and (ux)Ro“R%，R' = R{!Ro for some R'(x(U).U|(<().0)子vx(0|0),q()4(x)(x(U).By induction bypothesis, Ro = Co[S(a(K).s')],U}0), and (vx)(x(U).Uj0) cannot match the T ac-Ro 0.+ R = C%[S"|S{K/U}] for some contextstion.The following states the relationship betweenCo, C%, and Ro (04 C'[S'|T{K/U}] for any Tthe auxiliary predicate↓and the transition rela-such that bn(Co) ∩fn(T) = 0. Let C =!Co,C' = Cl!Ro, obviously, R = C[(K).5'), .tion 0(42) .!Ro， R%|!Ro = C'[S'|S{K/U}], and ifT isaLemma 3. Let P be a program, then1)ifP 114 P', then there exists some S suchprocess such that bm(C)Nfn(T) = 0, then bn(C)∩fn(T) = 0, so !Roa(U).T+ CI[S'T{K/UJ}]!Ro =that P↓a(U).S and P' = s{R/U};C'[$'T{K/U}].2) P↓a(U).s, then P (B):( s{R/U}.Exarmple2. 1) R= Z(a(K>.S'), and Ra(U);SProof. For 1), use induction on the tree to de-S'|${K/U};rive pA44P'. For 2), use induction on the tree2) R = vb(Z(K>.5')), and RS二vb(S"|to derive the predicate P↓a(U).S..The following definition will introduce one-holeS{K/U});context which will be used later.3) R= vb(E(a(K).S'))|T， and R， a(U).SDefinition 3. A stactic context C is defined byvb(S"\S{K/U})IT;the BNF grammar.C:= 0IC|P| PIC | vbC|!C.4) Rr=(vb(S().)T), and R=(U)5Moreover, ifC is just defined by the BNP grammar; (b(S"S{K}/T})P()(b[(()S.))IT).C :=0|C|P| PIC | vbC, then C will be calledLemma 5 says that ~ is preserved under non-non-replication context. And for a context C, we replication context. The result will be used in thedefine bn(C) by induction:proof of some congruence properties of ~ .Lemma 5 (Aux0). Let R = {(CIP],C[Q])bn([)=0P~ Q}, where C is a non-replication contert de-bn(C|P) = bm(C)fined in Lemma 4, then R is a bisimulation, andbm(P|C) = bm(C)for any pair (C[P],C[q])∈R, we have:中国煤化工MHCNMHG356J. Comput. Sci. & Technol, May 2004, Vol.19, No.31) whenever C[P]与P', then there exists Q'Lemma 6. 1) If!P与P', anda≠T, thensuch that C[Q]与Q' and P'RQ';P'=Q|!P andP 4Q for some Q.2) whenever C[Q]牛Q'，then there exists P'2)IfP与Q,then!P与Q|!P.such that C[P]与P' and P'RQ';3) If S|!IP→P'， then P' ~ Q|!P andwhere μ is of the form T, a(U)Q, a(K).0.S|(P|P)→Q for some Q.Proof. By induction on the structure of C.4) If S|(PIP)→Q, then S|!PAP', and P'~Base case: C = 0, trivial.Q|!P for some P'.For inductive cases, we do case analysis on theThe fllowing lemma says that ~ is preservedstructure of C.under the replication operator.Case 1. C = vaC", sinple.Lemma 7. Let P, q∈Pr, P~ Q impliesCase2. C = C|R, and C'"[P]|R与w, then do!P ~!Q.Proof. Let犯= {(R|!P, S|!Q)| P~Q,R~ s}.case analysis on the last rule applied to derive theFirst we show R is a bisimulation up to ~ .transition.Case2.1. C'[PI 与P{ and w = P[|R for someq|Q.Since P~Q, then by Lermma5, PIP~ Q|P ~P', by induction hypothesis, there exist a non-We show that s|!Q can match any action fromreplication context C" and two processes P',Q'R|!P, say RlIP与T. We just examine the case insuch that C"[P'= PI, and C"[Q] 4C"IQ'], andwhich μ is a silent action. By Lemma 6 3), T ~. P'~ Q' for some Q', then by transition rule Parl,TI!P and R(P|P)与T' for some T'. By congru-R.C'[Q]|R 与C"[Q']R, and (C"[P']lR,C"Q'|R)∈ence property of |, we know R(P|P) ~ S|(Q|Q),Case2.2. R气R' and W = C"[P]IR', simple.then S|(QlQ)-T" and T' ~ T" for some T". ByCase 2.3. C'[P] a(OSPI, R↓a(U).S, C[PI\Lemma 64), SI|!Q 4Q', and Q' ~ T"I!Q for someQ', then Q' ~ T"|!QRT'|!P ~ T. That is enough.RFP{，and W = Pl for some P', by induc-0tion bypothesis there exist a non-replication con-Next lemma shows that ~ is preserved overtext C" and two processes P',Q' such that P[ =higher- order substitution. This lemma is the mostC"[P'], C"[Q] 005C"[Q'], P' ~ Q' for some Q',important result in this paper, and helps us tothen by transition rule Coml, so C[Q]}R干CI"[Q'],prove congruence for object output constructors.C"[P']RC"[Q'].(Theorem 2 5)).Lemma 8_ (abs-Congruence). Let P, P2,Case 2.4.Rr(U).SR', C{P] ↓a(U).Sp,P∈Pr, Pr~ P: implies P{Pr/X}~ P{Pz/X}.C'[P|R子R', andW = R'.Proof. Interested readers please contact withBy Lemmna 4， there exist a context Cr,the authors for the detailed proof.a process K and a process S' such thatNext we will show the bisimulation equivalenceR = Cr[2(K).S')], R' =. Cr[S'|Sp{K/U}],~ is preserved by all the constructs.bn(CR)n(Fn(C"[P)Uf("[q))=0. By C[IP↑↓Theorem 2 (Congruence of ~). Let P, Q,a(U).Sp, we have C"[P]> Sp{K/U}.R, S be processes erpressions. IfP~ Q, then .By induction hypothesis and Lemma 31) va.P~ va.Q; .1)，there exists a process Sq such that2)a.P + R~a.Q+ R;C'"[Q] a7394Sq{K/U}, C'[Q] ↓a(U).Sq and3) P|R~ Q|R;4) !P ~!Q;Sp{K/U}R Sq{K/U}, i.e., there exist a con-5) a(P).S+ R~a(Q).S + R.text C" and two programs P" and Q" such thatSp{K/U}= C"[P"] and Sq{K/U} = C"IQ"] andProof. Clause 5) can easily be derived fromLemma 8. And the proof of Clause 2) is routine.P'"i~ Q".Then by the definition of the transitionClauses 1), 3) can be obtained immediately from口Lemma 5. Clause 4), is Lemma 7.rule, we also have R a(0.54 CR["C"[Q"].So C'lQI|R 5 Ce[$'"C"[Q"I] and (Cx['1C"[P"], .4 First CharacterizationCr[SI(C"Q'1]) E R.Case3. C= R[C', similar to Case 2.In this section, we will explore the correspon-The following lemmas are about the replication dence between our LTS semantics and the reduc-operator.tion semantics of the calculus. And we will derive中国煤化工MYHCNMHGYong-Jian Li et al: Towards a Theory of Bisimulation for the Higher-Order Process Calculi357a characterization of the bisimulation ~ in termsR|CIQ'],soP~Q. IfC= E{a(U).C"}∪S, thenof a version of barbed equivalence.we have C[P'= C'lQ'], and then for any processThe reduction semantics of the calculus usedK we have C"[P']{K/U} = C"[Q] {K/U}, by inhere is also the same as that in [5], which contains duction hypothesis C'[P']{K/U} ~ C"[Q'] {K/U}.a set of rewrite rules and a set of reduction contexts With these it is not hard to see 2 ){a(U).C'[P']}∪in which they may be applied, and a structural con- s ~ E{a(U).C"[Q']}US. Other cases can be provedgruence. The structural congruence is as follows:in a similar way.1) E{a;Pl|i∈I}= E{aj.Pjlj∈J},ifJ isaThe following lemma relates the two relationspermutation of I;→and→. The proof is an easy induction on the2) (PlQ)|R= (PlQ)|P; PIQ=Q|P; P|0= P;proof tree of -3) vx0= 0; vxvy P= vyvx P;(vx P)|Q =Lemma10. p→P' if there exist Po, P( such .vx(P|q), ifne fn(Q); .thatP= Po, P二P', P%{= P'.4) P= P|!P.Now we show that ~5 and ~ coincide for theAnd the reduction relation is the sct of the ruleshigher-order calculus. We need the following twoas follows.lemmas which are easy to prove.COM: (E({(U)..+({(.)...}Lemma 11. For any process P and name a,it holds that P ta ifP9P', where a = a(U).Q,→P{K/U}|Qa(K).0 for some U,K,Q.P→P'.P→P'Lemma 12. Letl be a nuame not occurring freePAR:PIQ→P'IQRES:vxt P→Nx Prin P, a(U).Q, a(K).0, thenSTRUCT:Q=P,P→P',P'=Q'1)ifP"(029 p' ther Pla(Y).(Ql(V).0)干P"Q→Q'l(V).0;As ual, P↓a represents thatU).Q, a(K).Q2)if p(4h)9P' then P|a(K).(U).0千occurs unguarded in P with a unrestricted, i.e,P'Il(U).0;the occurrence is not a subexpression of e(U").R,c(K'^).R, and not within the scope of va.3) if P'a(U).(Ql(V).0) →R and R↓thenHere we will present a notion of barbed equiva-there exists P' such that R三P'l(V).0,lence in the style of [12], which is a variation ofP' 4, andP 0(0),9 P';barbed bisimulation proposed in [5]. Interested4) if P|a(K).l(U).0→R and R↓then therereaders can see [13] for a discussion regarding the .exists P' such that R三P'IU(U).0, P'↓,two approaches.and P 0(K909 P'.Definition 4. A binary relation R∈Prx PrTheorem 3. For two processes P and Q,is a barbed bisimulation if PRP2 impliesP~°Q讲P~Q.1) for any processQ∈Pr, PI|Q R P2}Q;Proof. If: We show that ~ is a barbed bisimu-2) for each namea, R↓a ifPr↓a;3) whenever P→P[, then there exists PI suchlation. Suppose P ~ Q. By Theorem 2, ~ is pre-served by all the contexts, so it is also preserved inthat Px→P'2 and P'RP2.parallel operator. By Lemma 11 and P ~ Q, we4) whenever Pz→P2, then there erists PI suchhave that P↓a ifand onlyifQ↓a.IfP→P', thenthat P→P and P'RP2.by Lemma 10, there exists P such that P = Po,Two processes P and Q are barbed equivalent,P与P%, P三P'. Since =S~, then P~P~Q,written as P R Q for some bisimulation R.soQ→Q' for some Q' withQ' ~ P'= P'. ThusThe structural congruence is included in ~.we can find Q' such that Q - +Q' and P'~Q'Lemma 9. =≤~.Only if: We prove that ~b is a bisimulation upProof. Let P三Q, we prove by induction onto~. Consider P ~ Q. Suppose that P a(Q.4P'.the structure ofP, Q that P~Q. IfP=Q is byChoose somel生fn(P, a(U).R). By definition weone of axioms, then by P~Q. IfP=Q is not byhave Pla(U).(Rl(V).0) ~b Q{la(U).(Rl(V).0), andthe axioms directly, then there must exist a contextby Lemma 12 1), P|a(U).(Rl(V).0) 与P'|l(V).0,C≠] and processes P', Q' such that P= C[P'],thusQ{a(U).(Rl(V).0)→Q" for some Q" withQ= C[Q'], and P' = Q'. We do case analysis onthe sruturofC. IfC= RIC, thenwehave Q" ↓andQ"n”P"(),.0. By Lemma 12 3),C'[P"] = C[Q'], and by the induction hypothe-there exists Q' such that Q”= Q']l(V).0sis C'[Pl]~ C'[Q'], then by Lemma 5 R|C'[P]~ and Qa(U).RQ'. We will show that P' ~rb~中国煤化工MYHCNMHG358J. Cormput. Sci. & Technol, May 2004, Vol. 19, No.3Q'. Since_ (P'|l(V).0)i(K).0 ~b Q"|[(K).0 =will derive a characterization of the bisimulation ~(Q'I(V)0)|(k).0，and Q"|[(K).0 →Q'0, soin terms of a version of context bisimulation defined(P'Il(V)0)(K).0→P" for some P" and P" ~bon Sangiorgi's LTs.Q'|0. Since Q' h, so P"↓h, and it is easy to seeThe traditional LTS of the calculus is given bythat the only pssibility is that P"三P'(0. Thus the rules in Fig2. To distinguish the same namne ofP'~ P'|0~b Q'|0~Q'. The case for P可(6,4 P'transition rules in our LTS, we use the bold lettercan be proved in the same way. The case forfor the nare of the transition rules in his LTS[8]P 4 P' is simpler.口such as RES, INPUT, and so on.Here the transition relations P 64 P',5 Second CharacterizationP (b(6)p', P p' are the input, output andIn this section, we will explore the correspon-tau actions respectively in [5]. To distinguish thedence between our LTS semantics and the tradi-tau action in his LTS from that in our LTS, we usetional LTS semantics of Sangiorgi in [5]. And we P→ P' to represent a tau action in his LTS.Input: Ea{(U)...} <(3), P{K/V}Output: (E{.(...}世4pp (u)a()p/ q (5)q'p a(h) p' q (0)6(5), q'Coml:. enfn(Q)=0 Comr:-E∩fn(P)=0 .PIQ #岷(P'Q)PIQ一ve(P'|Q)bn(a)∩fn(Q)=0ParrQ二Q1bn(a)∩fn(P)=0PIQ二P"IQPIQ P|Q'Open:二, (0u0)a(K),c≠a,c∈fn(K)-ERES:p9p'(c t n(a))veP. (ue,)(K) prvcP年vcP1Rep-Act:p气pRep-Com:p. a(K)p1 p . (w2)8(2IP 9 PIPIP王(w([IP")PFig.2. Traditional ealy Lts.In the transition rules in Fig.2, we can find that(P'PG{K1/U})RvE(Q'}PG{K2/U});the label of an action of a program P is from P it-3) whenever P一P', there existsQ' s.t. Q物self, representing the ability of itself. Especially,q' and P'RQ'.the label of an output action of P only shows thatA relation R is a context bisimulation, brieflyP can emit some object, but does not consider thedenoted as Eat-bisimulation, if R and R-1 are con-context in which the emitted object is supposed totext simulations.be used. So the efct, which the emitted object willIn fact, the version of context bisimulation herehave in the context, cannot be expressed directly inis diferent from the version of context bisimulationthis LTS. Thus when defining higher. order bisimu-in [5] in the clauses for output action matching. Forlation in the traditional LTS framework, we musthigh order output action matching, Sangiorgi usedexplicity take into. account the context in whichthe late style which reversed the order of the quan-the emitted object is supposed to be used.tifiers in Clause 2). In fact, this version of contextThe notion of the context bisimulation used inbisimulation is corresponding to the early contextthis paper is defined as follows.bisimulation defined in [14].Definition 5 (Context Bisimulation). A bi-To facilitate the reasoning later, we introducenary relationRE Prcx Pre is a context simulationthe concept of concretion, w hich is originated fromif PRQ implies,Milnerl1o]. A concretion would be an expression of1) whenever PA4P', there exists Q' s.t.the form (ub)(K,Q). With the help of concretion,Q a(54Q' andP' R Q';we can rewrite the transition relation P rba(k+q2) whenever P baK1Pr and for all PGas P台(vb)(K, Q), where b represents the names towith fn(PG) ∩6 = 0， there erists Q' s.t.be extruded, K represents the process ermitted, andQ is the remaining process. And we define pseu-Q (we)l(k3)q' with fn(PG)∩ε= 0 and vbdoappliaction between a concretion (2b)(K, Q) and中国煤化工MYHCNMHGYong-Jian Li et al: Towards a Theory of Bisimulation for the Higher _Order Process Calculi359a process PG possibly with a free variable U as fol-Definition 6. Let S = {P|P is a programlows:of the forrn ve(P|P2)}. We define three functionswhose domain is S.PG●(z0)(K,Q) =af vb(Q|PG{K/U}}get. res. _names(ve(P|P2)) =djcpart(vE(P1|P2)) =df P1First, we give the correspondence between theparr(vE(P|P2))=df Pztransition relation P 17 P' in our LTS and theThen we will define a function trans, which willtransition P“A) P' in Sangiorgi's LTSl5. Inter-take such P, P', K, PG as parameters, and returnested readers please contact with the authors for a process which is just the form of a pseudoappli-the detailed proof.cation between some concretion ve(K, Po) and theLemma 13. F(2).:P" if Iprocess PG, and furthermore P is just a programSecond, we will explore the correspondence be- such that P_ Po. By Lemma 4, we will findtween the transition relation9p' inour that if P a(U).PCP', then P= C[(K).P")I,LTS semantics and the transition peAP' inP' = C'[P"PG{K/U}] for some P", C, and K.Sangiorgi's LTSI5I. First we see an example to So it is not surprising that the function trans isfind some intuitive correspondence between the tworecursively defned on the structure of C.kinds of transition relation.Defnition 7. Let P, P' be two prograrns, KExample 3. Let P = E{(a(K>.Q...}.be a process or a name, PG be a process. We re-cursively defirne a partial function trans: Pr x Prx1) p(k>q, and P).PC&q|PG{K/U}.Prx Pr→Pr as follows.2) Ifc∈fn(K), then vcPvea(K)Q, further-trans(P,P",K,PG) =dmore, ife史fn(a(U).PG), then vcP a().PCSif P= ({{a(>...} and P' = (q|PG{K/U})vc(Q|PG{K/U}).and Pa(OD.PCp' then P'3) Ifc史fn(K), vcP a(A vcQ, furthermore, ifelse ifP=vbQ and p' =w6Q' and P (U)PC P'c史fn(a(U).PG), veP a0 vc(Q|PG{K/U}).ifb'∈fn(K {b'/b}) thenNote that vc(Q|PG{K/U}) = (vcQ)PG{K/U}({b'}Uget-_ res - names(rans(Q{b/b},Q',K{6/6},because c申fn(K)∪fn(a(U).PG).par(trans(Q{6'/b},q', K{b'/b}, PG))4) P|R (5) Qir, and P|R a(U),PE(Q{PG{K/PG)) ( lr(rans(6/b)，Q, K{6/6},PG)U})IR, and note that (Q|PG{K/U})IR = (Q|R)|else v(get-res _names(trans(Q{b' /6}, Q' , K, PG)))PG{K/U}.( (vb' par(trans(Q{b'/B},Q' , K,PG)) )5) !(P|R) ()(Q(R)!(PIR), !(PIR) (U,PG( lr(rmr({6/6),0), K,PG))end if((Q|R)PG{K/U})|!(P|R), and note that ((Q|R)|else ifP= P|P2 and P a(U).PS P' thenPG{K/U })]!(P|R)三(Q|R)!(P|R)|PG{K/U}From the above example, we conjecture that:ifP“0P andP'= P'|P2if P has the ability to output something, i.e,then v(get res_.names( truns(P, P', K, PG)))P bea(4, P for somne P, e, K, then P can respond! (arl(trons(Pr, R,K, PG)P2)| )( par(trans(P, P', K,PG))to an output test a(U).PG from the context withe∩fn(a(U).PG) = 0, and be changed into a formelseifP a(U),PC% andP'=P |B'which is structure congruent to pseudoapplicationthen v(get. .re8. names(trans(P2; P%, K, PG))between the concretion ve(K, P) and the process( (Pipar(rans(P2, P%, K, P)))( pr(rns(PB,P,K,PG))” )PG, i.e., p"O.G P', and ve(Po|PG{K/U})三P' for some P'; and vice versa, if P can respond toelseifP=!Q andP'= Q'|Q and P a(U).PCP'a test a(U).PG from the context, and be changedthen U(get-res . names(trans(Q,Q', K, PG)))into P' for some P', then P has the ability to out-(parl(trans(q,Q' ,K, PG))|!Q)| )put something, i.e, P ea9 P for some Po,e, K,( parr(tran8(Q,Q,K,PG)) )and the pseudoapplication between the concretionve(K, P) and the process PG is structure congru-else no defnittionent to P'.Before detailed proof, we need two preliminaryExample 4. Consider the program P in Exam-definitions.ple 3 again.中国煤化工MYHCNMHGJ. Comnput. Sci. & Technol, May 2004, Vol.19, No.31) trans(P,qIPG{K/U},K,PG) = Q{|PGparl(trans(Q{b/b}, Q',K{b'/b}, PG)){K/U}.larr(trans(Q{b/)},Q' ,K{6/B}, PG) )2) Ifc∈fn(K), trans(vcP, vc(Q|PG{K/U}),= (vb,2)(Qo{b' /B}|PG{K{b' /6}/U})K, PG)= vc(Q|PG{K/U}).二(vb, 2)(Qo|PG{K/U})3) Ifc史fn(K), trans(vcP,vc(Q|PG{K/U}),= (vb,e)(PIPG{K/U}).K, PG) = (vcQ)PG{K/U}4) trans(P|R, (Q|PG{K/U})|R, K,PG)= (Q|At the same time,R)[PG{K/U}.5) tran8s(!(P|R), (Q|R)PG{K/U })!(P|R), K,(ub, e)(Qo|PG{K/U})PG) = (QR)!(P|R)|PG{K/U}.= vb(u@)(Qo|PG{K/U})) (by induction hypothesisAs the following lemmna says, if P has the abi-(u2)(Qo|PG{K/U})= Q')lity to output something, then P can respond toan =vbQ' = p'.output test from context.Lemma 14. IfP(002(5) P, then for all pro- Case 2.2. b史fn(K), then P = vbQo, notecesses PG such that e∩(fn(PG)U{a})= 0, thenthat b may be in fn(a(U).PG).Let P' = vb'Q'.there exists a programp' such that P a(U).PC,trans(P, P',K,PG)and trans(P,P',K,PG) = (ve)(Px|PG{K/U})== trans(vbQ,vb' Q', K, PG)P'.Proof. By induction on the tree to derive= v(get.res_names(tran8(Q{b'/b}, Q', K, PG))( (vb parl(trans(Q{b'/b},Q',K, PG)))p. (ue)a(l)Po, then by case analysis on the last( lr(rns({0/6},Q(,K,PG)) )rule of the tree.= (v2)(vb'Qo{b/b}|PG{K/U})Case 1. The last rule is Output. Then P is of= (v2)(vbQo|PG{K/U})the form Z{(a(K.Q...} for some ?, and Po= Q.= (w()(P|PG{K/U}).Let P' = Q|PG{K/U}.P aU).PC p/ = Q|PG{K/U}, and P 4(5Q.(v2)(vbQo|PG{K/U})Since P = ((.>...}, trans(P,P', K,PG)(6' f fn(PG{K/U}))= P'= (Q|PG{K/U}).Case 2. The last rule is Res，Then P is .= (vb'2)(Qo{b /b}|PG{K/U})vbQ, and Q ea.4+Qo for someb, Q,己Qo. On= bW((v)(Qo{b /}|PG{K/J})(by inductionthe other hand, P is a-convertable to vb'Q{b'/b},hypothesis (va)(Qo{b/b}[PG{K/U})= Q")= vb'Q" = P'whereb' is a name such that b'史n(a(U).PG)UCase 3. The last rule is Parl or Parr. Thenn(P). And Q{b/b}(12)a(K{6/6])、>Qo{6/b}. And P= P|B for some P, P.the trees to derive Q vea(A+Qo and Q{b'/b}Case 3.1. The last rule is Parl. Then(vE)a(K{b' /B})> Qo{V/b} have the same length.P-vea(K>P" for some P[", and e∩fn(P2) = 0and P = P"|P2, by induction hypothesis. IBy induction byotesis,s fQ{1BE(2H8(K{6/b2}p,. vea(K)4 P", then there exists a program P' suchQo{b' /b}, then there exists a program Q' such thatthat P Pl and trans(P,PI,K,PG) =Q{6/} a(U,PSq'，trans(Q{6/B},Q',K{6/b},Then there exist two subcases.Let P' = PIP2. Obriously PIPBgauU,rG PIPR2,Case 2.1. b∈fn(K)， then Po = QoandAnd b'∈fn(K{b/b}), obviously P = vbQtrans(P|P, P|Pz, K,PG)(B ,C)4(K{b' /0})、4Qo{b'/b}. Let P' = (vb')Q', by= v(get.res-names(trans(Pr, P1, K, PG)))par(trans(P, PI, K, PG))P2)\({b}U2)∩fn(a(U).PG) = 0, P= vbQ90:19|parr(trns(P1, PI, K, PG))(ub')q',= ve((P'"lP2)|PG{K/U}).trans(P, P', K, PG) = trans(ubQ, vb'Q', K, PG)At the same time, P = P|Pzvea P'IP.And .= v({} U get.res - names(trans(Q{b'/b},q',ve((P"|B)|PG{K/U})K{b/b}, PG)))= ve((P'"|PG{K/U})IP;)(E∩fn(P2)= )中国煤化工MYHCNMHGYong-Jian Li et al: Towards a Theory ol Bisnulation for the Higher-Order Procss Caleuli361= (ve(P"|PG{K/JU})IPz (by inductionLemma 15. If pa(O.PGp', then there erhypothesis, 顺(P'|PG{K/U})= PI)ist a process K and a name list e such that=P|P2= P'.Case 3.2. The last rule is Parr. Thenε∩fn(a(U).PG) = 0, a prognam B such that .R for. some P", ande∩fn(B)=θ Pp wR and trens(P,P",K,PG) = ()(P%|and P. = P|P", by induction hypothesis. IfPG{K/U})= Fvea(KProof. The proof is still by induction on the treeP2当P", then there exists a program P suchto derive P U).PG P". Intersted readers pleasethat BRO(U-PCB and trans(P,P%, K,PG) =contact with the authors for the detailed proof. 0v(P"|PG{K/U})= P%.The fllowing lemas will show the correspon-Let P' = P|P. Obviously PIP a(U).PC p",dence between the transition relation P→P' inDZDIandour LTS semantics and the transitiontrans(P|P,R|P',K,PG)Sangiorgi's LTS5. Interested readers please con-= u(getres_names(rans(P2, PI, K, PG)))tact with the authors for the detailed proof.(Plpr(trans(B,% K, P)))Lemma 16. IfP + P', then there erists a( |parr(trans(P2, P2, K, PG))program P" such that P与p" andP'= P".= ve(PI|P")IPG{K/U}).Lenma17. IJP子P", then there erists a pro .At the same time, P = P|B oe P|PB',gram P" such thatP→P" andP'= P".and e∩fn(P)= 0. AndNow we can prove the main result of this sec-e((PI|P")|PG{K/U})tion, ~ and二et coincide.= ve((Pl|(P'IPG{K/U})(e∩fn(P)= 0)Theorem4. P~QjP∞ot Q.= Pl|(ve(P"lPG{K/U})) (by inductionProof, Proof of→:hypothesis, v(P"|PG{K/U})= P2)Let犯={P,Q)P~ Q}, then we will= P|PI= P'.prove that咒is a context bisimulation. SupposeCase 4. The last rule is Rep-Act. Then P P-4 P', then there are 3 cases to be considered.is !Q for some q, and ? vetaA4Qo, P= Qo!Q,Case1. P“A p' (by Lemma 13)obviously E∩fn(Q)= 0.=→p1(R3Qpr (byP~Q)By induction hypothesis, if Q Deal24 Qo, then→3Q'●Q -a(K),0+Q' AP' ~ Q' (by Lemma 13)there exists a program Q' such that Q a(U)-PSq→3Q'●Q akQ'λP"~Q'.and trans(Q.Q',K,PG) = ve(Qo|PG{K/U}}三Case2. P (020(54 p'2’.Let P'= Q1I!Q. Obviously P =!Q a(U).PC, Q'|{a})= 0.Let PG be a process such that bn (fn(PG)U!Q= P'. And”trans(P,P',K, PG)Lemma 14)p (06)0(K1)P', b∩(n(PG)∪{a}) = 0 (by= trans(Q, Q'|!Q, K, PG) (by inductionhypothesis)→3PoP a(U).PC PAtrans(P,P, KI,PG) == u(get. res_names(trans(Q,q', K, PG))(u)(P'|PG{K1/U}) and trans(P,P,K1,PG) =(par(truns(Q, q',K, PG))l!Q)P(P~Q)( parr(tnans(Q, Q', K,PG)))→3Qu●Q .a(U).PG>Qo^ P ~ Qo (by Lermma= vl(lo[()PG{K/U})15)= v(P|PG{K/U}).At the same time,→3,Q',K2●Q(w2)a(K2)Q'八ε∩(fn(PG)((Qo}!Q)|PG{K/U})U{a}) =日人trans(Q,Qo,K2,PG) = (ve)(Q1三ve(Qo|PG{K/U}IQ)(E∩fn(Q) = 0)PG{K2/U})= Qo.= ve(Qo|PG{K/U})IQ (by inductionAnd (wb)(P'|PG{K/U}) = R ~ Qo =hypothesis ve(Qo|PG{K/U})= Q')(va)(Q'|PG{K2/U}).By =C~, then we have= q'IQ(ub)(P"|PG{K1/U}) ~ P ~ Qo ~ (v0){Q'IPG= P".。{K2/U}).And vice versa, if P can respond to an outputCase3. P一P' (Lemma 16).test from context, then P has the ability to output=→3P"●P→P"λP'= P"(P~Q)something.→3Q°●q→q"AP"~ Q" (Lemma 17)中国煤化工MHCNMH G362J Comput. Sci. & Technol, May 2001, Vol.19, No.3→3Q'●Q→Q'^Q' =Q".over traditional ones. Firstly, we use the test labelAnd P' = P"~Q"=Q', by =C~, thenit is a(U).Q to represent the meaning of an output ac-concluded that P' ~ Q'.tion, where the context Q can be encoded in theProof of年:label a(U).Q naturally. So we can easily avoid theLet貺= {(P,Q)IP 二ct Q}, then we will separation between object part and context of anprove that R' is a bisimulation up to ~. Suppose output action. Secondly, the labels of any action ofPa(K)，then there are also 3 cases to be con-a program are from its environment, not from theprogram itsclf, so we can avoid the complex notionsidered.of scope extrusion. Thirdly, based on the new la-Case1. P 81470 P' (by Lemma 13)belled transition semantics, we can propose bisim-冷pAA4P' (by Psot Q)ulation in the standard way following CCS without.→Q aAQ' AP'二at Q' (by Lemma 13)any dificulty. Besides these advantages, our se-mantics and bisimulation are natural and rational.+Q'八P'≌et Q'.The results of two characterisation theorems (The-Case2. palO.Pe P' (by Lemma 15)oremns 3 and 4) have shown the naturalness and→3e, Po,K1●pwe)aka, Po入en(fn (PG)urationality. And the results also relate our equiva-{a}) = 0 ^ trans(P,P',K1,PG) = (ve)(Po|lence with the well- established semantics. Here ourresult is only for the strong version. But in fact wePG{K1/U}) Atrans(P,P', K,PG)= P'.can find that our theory can apply to the weak case(PLa Q)without any dificulty.→3d,Qu,K2●Q(2)a(K)+ Qo ^d∩(fn(PG)In fact, the work in this paper is the continua-U{a)) = 0A (v0)(PB|PG{K1/U}) =et (vai(Qol tion and extension of that im [15]. In [15), we stud-PG{K2/U}) (by Lemma 14) .ied the contextual labelled semantics in the first-→3Q'●Q10.P Q'^ trans(Q, Q', K2, PG) = order T-calculus and a simple fragment of higher-Q' ^ trans(Q,q', K2, PG) = (vd)(Qo|PG{K2/U}). order -calculus separately. In fact, the syntax ofThen P' = (ve)(Po|PG{K1/U}) ≌et (ud) that fragment of higher-order π-calculus is very re-(Qo1PG{K2/U})=g', by =C~,S0 P'~ (we)(P| stricted, and much simnpler than that in this paper.PG{K1/U})二a (vJ(Qo[PG{K2/U}}~ Q'.So the result of the congruence of the bisimulationCase3. P千P' (Lemma 17)is much easier to obtain than that in this paper.And we need many new techniques to prove the.→3P"◆P→P"λP'= P"(P-ct Q)congruence theorem in this paper. For example,才3Q"●Q→Q" ^ P"二et Q" (Lemma16)we develop new techniques to prove that the new→3Q'●Q→Q'^Q'= Q".bisimulation is preserved under parallel and repli-AndsoP'=P"=otQ"= Q'.口cation operator. Besides the result of the congru-ence property, we also develop the theory to show6 Conclusion and Related Workthe precise correspondence between our LTS se-mantics and the traditional early LTS semanticsIn this paper, we studied a lblled transi- of Sangiorgi in [5].tion relation and the corresponding equivalence forSangiorgi did the most extensive study on simi-a higher-order process calculus. We proved con- lar topic for HOπ in his thesisl5,14l. There he pro-gruence properties of the new bisimulation, and posed a labelled semantics and a reduction seman-showed its two versions of characterization. The tics for HOπ and several bisimulation equivalencesmain purpose of this work is to apply the con- including context bisimulation, triggered bisimula-textual labelled semantics to higher-order process tion, and normal bisimulation. He contributed acalculi and to define a tractable notion of labelled novel approach to prove the congruence propertiesbisimilarity. In fact, the intuition behind the con- of context bisimulation. And his study acted astextual point view is very natural and simple. The a stimulus and basis for our work. Especially, welabels a(U).Q and (K).0 represent the test pro- refer to his semantics and early context bisimula-vided by a process's environment which will result tion to show the naturalness and rationality of ourin interaction between the process and its environ- semantics. But we can find our proof of congru-ment, and the predicate P↓a(U).P' says that Pence property is cleaner and more modular thancan provide the test a(U).P' for its environment. Sangiorgi's because our semantics and the style ofAnd this labelled semantics has several advantages new defined bisimulation are more natural than his.中国煤化工MYHCNMHGYong- Jian Li et al: Towards a Theory of Bisimulation for the Higher-Order Process Calculi363An interesting question for future exploration is toVerlag,Barcelona, Spain, March 13- 17, 1989, pp.149-define triggered bisinulation, normal bisimulation[9] Peter'eter Sewell. From rewrite rules to bisimulation con-and prove the coincidence between them in our se-gruences. In Proc. Concur'98, LNCS 1466, Springermantic framework.Verlag, Nice; France,1998, pp:269-284.Jeffery and Rathke adopt the sarme idea and [10] Milner R. The polyadie π-calculus: A tutorial. In Proc.give a labelled semantics for a fragment of CMLthe Intermnational Summer School on Logic and Algebmawith local names[16), and prove that the bisimu-[11] Sangiorgi D, Walker D. The π-Calculus; A Theory ofof Specification, 1991.lation equivalence thus obtained is the same as aMobile Processes. Cambridge University Press, 2001,version of barbed equivalence. And the proof ofthe first characterization theorem in our paper is[Kohei Honda, Nobuko Yoshida. On reductionbasedprocess semantis, Theoretical Computer Science, 1995,adapted from their work. But due to the functionnature of CML, they adopted a triggered semantics [13] Fournet C, Gonthier G. A hierarchy of equivalenceto prove the congruence properties of the bisimu-for asynchronous calculi In Proc. Interrlalional Col-lation equivalence in their work, so their proof isloquium on Algorithms, Language and Programming,much more difficult than ours.LNCS 1448,4 SrigngeVerloe, Aalborg, Denmark, JulyAs said previously, when mnoving to more pow- [14] Sangiorgi D. Bisimulation for higher-ordererful process calculi with mobility and higher or-culi. Information and Computation, 1996, 131(2): 141-der fcatures, the labelled semantics of traditional15] Liu Xinxin, Li Yongjian. Bisimulation forstyle become hard to work with, and correspond-Bisimulation for higher-orderπ-calculus. In Proc. the Third Asian Workshop on Pro-ing bisimulation formulations are often much moreelaborated, resulting in less satisfactory theories.Alan Jeffery; Julian Rathke. A theory of bisimulationWe hope that our results can open up a new alter-for afragment of concurrent CML with local names.native to the development of manageable theory forInPracLogenComputerscrencertseosrress,Santa Barbara, alifroria, Jume 26 28, 2000, Pp311-powerful process calculi with mobility and higher-321.order features. It would be very interesting to um- [17] Luca Cadeli, Andrew D Gordon. Mobile ambients.derstand whether our semantics and formulationfor higher-order calculi can be applied to processcalculi modeling distributed and mobile program-18] Cedric Fournet, Georeges Gonthier. The reflexiveming such as Ambient17] and join[18].Symposium on Principles of Prograrmming Languages,1996, pp.372- -385. .ReferencesYong-Jian Li received hisPh.D. degree in computer sci-[1] Milner R. Caculus of communicating systems. LNCSence from Shanghai JiaoTong92, Springer Verlag, 1980.2} Park D. Concurrency and automata on infinite se-university in 2001. He is an a-quences. LNOS 104, Springer Verlag, 1981.sistant researcher in the Labo-[3] Milner R. Communication and Concurrency. Prenticeratory of Computer Science, in-Hall, 1989.stitute of Software, the Chinese[4] Milner R, Parrow J, Walker D. A calculus of mobile pro-Academy of Sciences. His cur-cesscs, (Parts I and II). Informnation and Computation,rent research interests are con-1992, 100(1): 1-40.currency theory, semantics of5] Sangiorgi D. Expressing mobility in process algebras:First-order and higher-order paradigms [Dissertation].programming language, application of formal methods.University of Edinburgh, Edimburgh, UK, 1992[6] Thomsen B. Calculus for high order communicating sys-Xin-Xin Liu received his Ph.D. degree in com-tems [Dissertation]. Department of Computing, Impe-puter science from Aalborg university in Denmark inrial College, 1990.[7] Astesiano E, Giovini A. Generalized bisimulation in e1992. He is a researcher in the Laboratory of Computerlational specifcations. LNOS 294， Springer- Vcrlage,Science, Institute of Software, the Chinese Academy ofpp.207- -266Sciences. His current research interests are concurrency[8] Boudol G. Towards a lambda calculus for concurrent theory, function programming language, model check-and communicating systems. LNCS 351, Springer-中国煤化工MYHCNMHG