Topology in Process Calculus (I): Limit Behaviour of Agents

計算機科學(xué)技術(shù)990406計算機科學(xué)技術(shù)R資源系統JOURNAL OF COMPUTER SCIENCE數字化期刊WANFANG DATA ( CHINAINFO)AND TECHNOLGYDIGITIZED PE RIODICAL1999年第14卷第4期V ol.14 No.41999T opology in Process C alculus(I):Limit Behaviour of AgentsYING Mingsheng(應明生)Department of C omputer Science and T echnology, TsinghuaUniversityBejing 100084, P.R. ChinaAbstract This paper introduces the modifications onactions of a topology on names ofactions and thesimplest topology onagents induced by a topology on names of actions andshows that the limitbehaviour of some agents is compatible with transitional semantics.Key words process calculus, transitional semantics,topology, limit behaviour1 IntroductionC ommunication and concurency are essential in understandingcomplex dynamic systems,and there have been many theories to deal with,such as Petri nets[1], CSP [23] and ACP[4].CCSproposed by R. Milnerin [ 5, 6] or process calculus as calledin[ 6] isoneof themost important and mathematially developed models ofcommunication and concurrency. Inprocess calculus, a central notion isobservation equivalencewhich expresses the equivalenceofprocesseswhose external communications follow the same pattern but whose internalbehaviourmay differ widely. W e know that both external and internalbehaviours in a process consist ofsome basic actions, and these basicactions are supposed to be distinct and irrelativewith eachother. Insome realistic situations, however, we may find that some actions arequite similar butothers are not. To be more explicit, let us consideran example. Suppose that three vendingmachinesC, F and S forselling C oCa-C ola, Fanta and soap, respectively, are defined as follows:C“e 1.cacaCalacoletC,F ≌l(shuí)danacollet.F. andS ae 1d.ap.olletsThis means, for example, that to buy a cup of Fanta from the machine Fyou must put in onedollar, press the button marked Fanta' on themachine F, and collect your Fanta from the tray. Ifsome person isextremely thirsly and wants to buy a cup ofC 0caC ola, and there is notthemachine C but the machines F and S nearby, then it isreasonable to expect that this person willbuy a cup of Fanta from Fbut not a cake of soap fromS. As asecond example, wesupposeothertwo vending machinesC+ and C- areall for selling C oCaC olabut the prices are different.Furthermore, we suppose that C+ andC- are defined byC+ eg! 1.5d.Coca-Colacollect.C+, andC-“些 0.8d.Coca中國煤化工MHCNMHGrespectively. If some person just wants to buy a cup ofC 0ca-C olawnich COSTS aoout 80cents, and there is not the machineC- but themachinesC and C+ nearby, then it isfle:/// vqkj-/sig9/sik994/90406.htm(第1/ 15頁(yè)) 2010-3-23 1:12:03計算機科學(xué)技術(shù)990406alsoreasonable to expect that this person will buy acup of C oca C olacosting one dollar fromCbut not acup of C 0caC ola costing onedollar and 50 cents fromC+. Why? An intuitive answermay be thatF is moresimilar to C than S, and C is moresimilar to C -than C+. H owever, it isclearthat this cannot be explainedformally in the process calculusin [ 5, 6] . To this end, we shouldaddsome topological structure on agent expressions. For example, we definea metric ρ 1 withρ 1(Coca-Cola, Fanta)=1,ρ 1(Coca-Cola, soap)=ρ 1(Fanta, soap)=+∞and ametricp 2with ρ 2(0.8d, 1d)=0.2, ρ 2(0.8d, 1.5d)=0.7 andp 2(1d, 1.5d)=0.5.Ifρ 1 and ρ 2 can induce somemetricp on agent expressionssuchthat, say,ρ (C,F)=1,ρ (C,S)=ρ (F,S)=+∞,ρ (C,C)=0.2,ρ (C-,C+)=0.7andρ (C,C+)=0.5, thenρ (C,F)<ρ (C,S)andρ (C-,C)<ρ (C-,C+),and this will be a quitenatural mathematical answer to the above question.Asa formalization of the simple idea mentioned above, the main aim ofthis paper and itscontinuations is to construct some natural topologieson agent expressions from each giventopology on basic actions and showthat these topologies are compatiblewith some notions ofbehaviour ofagents and equality over the process calculus. In this paper, weintroduce theconcepts of modifications on actions of a topology onnames of actions and the simplest topologyon agents induced by atopology on names of actions and show that the limit behaviour ofsomeagents is compatiblewith transitional semantics.2 PreliminariesIn this paper, for simplicity and as the first step we onlyconsider the basic calculusofsynchronisationin [ 6] . H ere, we displaysome fundamental concepts in the way which can beusedconveniently forour purpose. For details, see [ 6] .2.1 Basic LanguageLetO beaset, whose elements aealled actionslet△= {征:a∈0}thessetof co- namesofactions, andletI = 0 U A, theset oflabels. In addition, Ietτ stand for thesilent action,andAct = ru {}, the set of actions. By defininga = a foranya∈△andF = T,- may beextended as a mapping from Act to itself. Afunction f:「→「is called a rlabellingiif() =兩foreveryI∈「. Wemay extenda relabelling fto bea mapping fromAct to itself by definingf(τ )=τ .Furthermore, letθ∈On (the limitordinals), and let究be aset, whose elements are calledagentconstants. Weset8= RU{a.:a∈Act}U {2n<8:δ < o}∪{|}u{\L: L≤r}u {[f]:f sarlabeling andE<0 =∪8 Odoes not hold. This meansthat E isnot closed.Example5.2. Let(A, 3) bethe same asin the aboveexample,犯= {An :n≥1}andAne(1- )0+ An+1 (n2 1).ThenAu中Oforanyn≥1, (3a)limn→∞(1-)= 1,andAs+odoes nothold, i.e, A1 is not closed.In the abovetwo examples, E and A1 are bisimilar and both of themare not closed. In the otherside; the fllowing example ilustrates thatsome agents are(strong) bisimilar but oneof them is closedand anotheris not.Example 5.3. Let(O,3)be the sameasin Example5.1,E= 2(1-)A'A and(n-1)a'sF= z(1-). .a .A,whereA '=a.A. Then it is easy to showthatE ~ F, F isclosed and E is not.Lemma5.2.(1) IfE∈Ppa,then 3E = 8a.中國煤化工(2) IfE andF havethe sameschema, thenE∈Po ifF∈Pa,.MHCNMH G∈Ppa. .(3) IfE isasubepresion ofF, thenF∈Pa impliesE∈Pa, andF∈Ppa impliesfle:/// vqkjr e/jk99/jk9904/990406.htm(第9/ 15頁(yè)) 2010-3-23 1:12:03計算機科學(xué)技術(shù)990406E∈Ppa.Proof. Straightforward.Definition5.3.LetE∈9. Then thecardinalS(E)=|U{δ∈On:En<8 occurs in E} |is called the summation index of E.LetD and D' be two directed sets. If there exists mappingh:D→D such that for everyn∈D, wehavesomen'∈D' with n≤h(n2), then D' is said to be cofinal with D. Thecardinalcf(D)= inf{| D' |: D' is cofinal with D}is called the character of cofinality ofD.The main result in this paper is the following.Theorem5.1. Le{E n:n∈D} beanetino,En牛E' for every .n∈p,(3p)limnεD En = E, (3p)limnεD En = E', and (3g)limn∈DQn=a. If(1) all constants in E are stable,[ C] 10.4cm= 11.4truemm=0mm(2) w+s(E)+≤cf(D), whereS(E)+ stands for thesuccessor ofS(E) (in particular, {En:n∈D}isasequence andE does not contain infinite summation), and(3) E∈Ppa, or E does not contain composition and(3.1) any L∈Res(E) is symmetric with respect to-, and(3.2) for anyf∈Rel(E),f~ (a) ≠中, and f1(a n) isasingle-ton(n∈D),thenE與E'中國煤化工MHCNM HGfle://E/ Vir e/jk99/jk9904/990406.htm(第10/ 15頁(yè)) 2010-3- 231:12:03計算機科學(xué)技術(shù)990406Exan+E'limE-_+E'Proof. AssumeG∈Qε andE=G(a n :η <δ ). Since .E∈PG∈S3p and (3p) limnεD En = E, threistsno∈D suchthatEn∈PG foranyn≥no. Thus without any loss of generality we can suppose thatEn = G(a):η < 0)forany n∈D. Now, we proceedby induction on thelength of G.(1)IfG∈犯，then En=E=G for every n∈D. Assume thedefining equationofG isG 2 Pc. ThenPc $ E' for everyn∈D.By noticing that terestriction and rlbelingassignments. are alregular, we knowthat Res( G)=Res(Pc), Re(G)=Re(Pc), SG = SPa, and(3c)imneDan = a implies (3p)imneDQn = a. SinceG istable P。ilosed andwehavePc 4 E'.With therule Conit holdsthatG 9 E'.(2)IfG = xo.G'{x1+n/xn : η < 6}andG?∈Qε , thenEn = a.G'(q{+n : η < 8) foranyn∈DandE = ax.G'{a1+n :η < b} Since(8p)imn∈D En = E, itholdsthat (3a)limneDa" = an foreeachη <1+8 fromProposition 2.3.34in [ 7] . In addition, we obtaina n=a on andE = G'(ar+n:η< 6)fromEn° E,for eachn∈D. Thus,a= ($g) limn∈DQn = ($g) limn∈D哈However,(3a)limn∈DQ = ao and 3a S 8g. Thisleadstoa =a 0. Furthermore, withProposition2.3.34in [ 7] and therule Act weassert thatE號G'(a1+n:η< 8) = (Sp) limnεDG'(a'+n:n< 6)= (3p)limneDE;= E'.(3) IfG = S<<|Dξ | provided D ? iscofinal withD, and | Dε|