《π-演算的符号迁移图及其早互模拟验证算法.doc》由会员分享，可在线阅读，更多相关《π-演算的符号迁移图及其早互模拟验证算法.doc（13页珍藏版）》请在三一文库上搜索。
1、-演算的符号迁移图及其早互模拟验证算法*李舟军陈火旺王兵山摘要提出符号迁移图作为-演算进程直观而高效的表示模型，并给出了符号迁移图多种版本(强/弱，基/符号)的早操作语义，在此基础上定义了相应版本的早互模拟和观察同余.同时引入了符号观察图和符号同余图以及-循环和-边消去定理. 最后给出了关于强/弱早互模拟等价和早观察同余的符号验证算法，并证明了其正确性. 将关于传值进程的强互模拟验证算法和关于纯CCS的弱互模拟和观察同余的验证技术融合和推广至有穷控制-演算.关键词-演算符号迁移图互模拟观察同余谓词等式系-演算1是Milner在其代表作通信系统演算CCS2的基础上提出的移动通信演算，其不同之处在
2、于允许进程之间传送通道名.因此-演算具有很强的表达能力，可描述动态演变的系统.目前关于-演算的一个研究热点是互模拟验证算法.已有的验证算法可分为两类：一类基于传统的划分求精算法(partition refinement algorithm)35，划分求精算法本身是高效的.但待验证进程的有穷迁移图的生成过程既繁琐又低效，且生成的迁移图相对庞大，此类方法对弱互模拟的验证尤为困难.另一类采用“on the fly”方法验证开互模拟6，进程的状态空间是动态生成的，由于需要不断的回溯，该算法的时空效率均较差.因此能否将Hennessy和Lin7,8关于传值进程的强互模拟验证算法推广至-演算，是一个令人关
3、注的问题3,9.由于-演算允许传名和限名，以及通道名和值的混用，这一推广远非平凡.至于对实际应用中最为重要的弱互模拟等价和观察同余，是否存在相应的符号验证算法，更是一个尚未解决的难题3,7,8.本文提出了-演算的符号迁移图及其生成规则，并给出了符号迁移图多种版本(强/弱，基/符号)的早操作语义和早互模拟定义，同时提出了这些互模拟的符号验证算法，对于迟互模拟，我们也得到了类似的结果1)，限于篇幅不再赘述.1-演算和符号迁移图令是通道名的可数无穷集，其元素用a,x,y,z表示.-演算由如下BNF语法给出：关于这些算子的含义参见文献1,9,10. 在a(x).t和(x)t中，x为具有辖域t的约束名.
4、由此引出进程项t的约束名字集bn(t)和自由名字集fn(t). 为了描述-演算的符号语义和验证算法，下面首先引入关于Boole表达式的可判定理论.Boole表达式由如下BNF语法给出：我们用BExp表示Boole表达式的集合，其元素用,表示.其他逻辑联结词和均是作为缩写引入的.计值Ev是从BExp至true,false的函数，满足：Ev(x=x)=true; 若x不同于y，则Ev(x=y)=false. 用vx表示文献9中的Boole表达式Rx().等名式是上等名测试(形如x=y)的有穷合取式，条件式是上等名测试或不等名测试(形如xy)的有穷合取式.等名式和条件式也可看成名字测试的有穷集.显然
5、等名式和条件式均为Boole表达式之特例.令和*分别为在-演算中扩充了形如xyt和t的项所得到的语言.本文结果不仅对-演算成立，而且对和*均成立.我们总假定V为的有穷集，并用new(V)表示不属于V的最小名字x. 用n()表示出现在中的名字集.若n()V, 则称为V上的Boole表达式.对于-演算，我们只涉及形如的有穷替换.若则记故当xn(),y=x当且仅当y=x.表示空替换，表示替换与的复合，xz表示将在x处的值修改为z的替换.V表示在V上的限制.称替换满足, 记作如果Ev()=true. 表示对任意替换，只要就有,=表示且.设B为Boole表达式的有穷集，如果B=,则称B为一个-划分.称B
6、oole表达式为协调的，若不存在x,y，使得x=y且xy.称12m为V上的Boole表达式的析取范式，如果=12m且每个i均为V上的协调条件式.同样地，可定义合取范式.利用范式和文献11中的命题2.1，易证得定理1.1对于任意Boole表达式和，是可判定的.设为V上协调的条件式.称为V上极大协调的，如果对任意x,yV, 或者x=y或者xy.称条件式为在V上的极大协调扩张，如果且为V上极大协调的.用MCEV()表示协调条件式在V上极大协调扩张的集合.当12m为V上的Boole表达式的析取范式时，记MCDV()为并称MCDV()为在V上的极大协调析取子.利用析取范式和文献11中的引理2.2，可知下
7、列定理成立：定理1.2若为V上的Boole表达式，则MCDV()=.下面我们引入符号迁移图作为-演算进程的直观而紧凑的表示模型.令SAct=a(x),x,(x)|a,x,Act=ax,x,(x)|a,x,其中(x)为导出的约束输出动作，而ax为自由输入动作，是为刻画早基互模拟特意引入的.并引入记号：若, 则=.定义1.1符号迁移图(简称STG)是一具有根结点的有向图，其每个结点n标有一有穷自由名字集fn(n), 每条边标有由Boole表达式和符号动作组成的序偶，且满足：如果是从结点m到n的一条边，则有fn(,)fn(m),fn(n)fn(m)bn()且bn()fn()=.符号迁移图中的限制条件
8、bn()fn()=只是为了保证-循环和-边消去定理(见下面的定理4.1和4.2)的正确性.对于有穷控制-演算(包括和*)的任意进程项，均可利用附录A中的规则生成其有穷符号迁移图.2早强操作语义和早强互模拟给定STGG, 其状态n由结点n和替换构成，可用于对结点n出边上的Boole表达式计值以导出基迁移.用p,q表示状态.若p为状态n,则用pxz表示状态nxz,p表示状态n,fn(p)表示自由名集fn(n).定义2.1STG的早强基操作语义是状态上的基迁移关系，可由下列规则给出：定义2.2状态上的对称二元关系R称为早强基互模拟，如果(m,n)R且Act蕴涵：只要且bn()fn(m,n)=, 就有
9、且(m,n)R. 用men表示存在一个早强基互模拟R,使得(m,n)R. 称m与n是早强互模拟的，记作men, 如果对任意替换有men. 称两个STG和是早强互模拟的，如果rer, 其中r和r分别是和的根结点.对于给定的STG, 其项n亦由一结点n和一替换构成，也可记作(n,). n实际上表示nfn(n), 即限制于fn(n). 我们用t,u表示项，同样地可定义记号txz,t和fn(t).如果替换不用于对结点n出边上的Boole表达式计值，而只作用于Boole表达式和符号动作，则可定义STG的更为抽象的符号操作语义.定义2.3STG的早强符号操作语义是项上的符号迁移关系，可由下列规则给出：定义
10、2.4设S=S|BExp是由Boole表达式加标的项上对称二元关系族，称S是早强符号互模拟，如果(t,u)S蕴涵：只要其中bn()fn(t,u,)=, 则存在-划分B, 满足fn(B)bn()fn(t,u,),且对任意B,存在使得其中用表示存在一个早强符号互模拟S使得(t,u)S. 两个STG和称为相对于早强符号互模拟的，如果其中r和r分别为和的根结点.早强符号互模拟与早强基互模拟具有下列关系：定理2.1当且仅当对任意证()令R=(t,u)|且,可证R为早强基互模拟.() 令可证S=S为早强符号互模拟.证毕.3早弱操作语义和早弱互模拟为定义STG的早弱操作语义，首先引入STG结点间的早符号双迁
11、移关系如下：注意，对于STG中的路径：必须引入形如：的双迁移关系，以便区分x的自由和约束出现.对于约束输出动作(x)，由于x不同于其他已知名，故可将随后-迁移中的Boole表达式用vx替换，以避免x的这种混用，因而无需引入类似规则.定义3.1STG状态上的早基双箭头关系由下列规则给出：类似于文献11, 可定义早弱基互模拟e, 早弱互模拟e, 早基观察同余e和早观察同余e.定义3.2STG项上的早符号双箭头关系由下列规则给出：引理3.1若则必有下列情况之一成立：(1) =true,=且t=t；(2) 若, 则否则(3) 存在t,1,2, 使得且=12;(4) 存在t,1,2, 使得且=12.定义
12、3.3设S=S|BExp是由Boole表达式加标的项上对称二元关系族.称S是早弱符号互模拟，如果(t,u)S蕴涵：只要其中bn()fn(t,u,)=, 则存在-划分B，满足fn(B)bn()fn(t,u,),且对任意B, 存在使得且(t,u)S,其中用表示存在一个早弱符号互模拟S使得(t,u)S. 两个STG和称为相对于早弱符号互模拟的，如果其中r和r分别为和的根结点.类似地，可利用E定义早符号观察同余关系E. 早弱互模拟和早观察同余的符号版本和基版本之间具有以下关系：定理3.1(1) 当且仅当对任意(2) 当且仅当对任意下面仅依赖早符号双箭头关系给出早弱符号互模拟的另一等价刻画，它是我们的早
13、弱互模拟验证算法的基石.定理3.2设S=S|BExp是由Boole表达式加标的项上对称二元关系族.S是早弱符号互模拟，当且仅当对任意(t,u)S和,(x),x,(x)只要其中bn()fn(t,u,)=, 则存在-划分B,满足fn(B)bn()fn(t,u,),且对任意B,存在使得其中为了给出早符号观察同余的等价刻画，需要引入关系它们与的唯一差别就是排除了自反的情况.定理3.3项t,u是相对于早符号观察同余的，即, 当且仅当对任意,a(x),x,(x),只要其中bn()fn(t,u,)=, 则存在-划分B, 满足fn(B)bn()fn(t,u,),且对任意B,存在使得其中对u有对称的性质成立.4
14、早符号观察图和早符号同余图基于早符号双迁移、定理3.2和3.3，可将观察图和同余图12推广至早符号观察图(ESOG)和早符号同余图(ESCG)，以构造早弱互模拟和早观察同余的验证算法.对于给定的STG, 分别用D(), E()和r表示的结点集、边集和根结点，并用n表示项n.给定有穷STG，其相应的ESOGO定义为：ND(O)=ND()且由于mO的每个结点均有-自圈.的ESCGC是O的变种.设的根结点为r, 则C可定义如下：(1) 若r无入边(入度为0)，则在O中消去r的-自圈，即得C;(2) 否则在中引入新的根结点r, 对中每条边引入相应的新边得到新STG1. 显然且r无入边，在O1中消去r的
15、-自圈，即得C.本文所采用的符号化方法能有效避免因输入变元的实例化而产生的状态指数爆炸问题. 对于含有-循环和-边的有穷STG，虽然我们能保证生成有穷的O和C.但其边数较之本身将有不同程度的增加.不过当满足一定条件时，可先消去中某些-循环和-边得到一个等价的STG，然后再生成其ESOG和ESCG.下面总假设C是的形如的-循环，用ND(C)表示结点集m1,ml,用E(C)表示边集mi|i,mi+1|i=1,2,l,其中ml+1=m1.由于fn(mi+1)fn(mi),显然有fn(m1)=fn(m2)=fn(ml).定义4.1设STG含有-循环C，令1l. 称C在中是可收缩的，如果对任意边其中mi
16、ND(C)且nND()-ND(C), 均有.用0表示将C收缩成一新结点m得到的如下STG：(1)ND(0)=ND()m-ND(C)且fn(m)=fn(m1);(2) 称该变换为-循环收缩变换.若rND(C), 则令r0=r, 否则令r0=m.对结点nND()-ND(C),分别用n和n0表示其在和0中的出现.定理4.1设-循环C在STG中可收缩.令0为将C收缩成新结点m所得到的STG，=12l,则(1) 对nND()-ND(C), ntrueEn0,且miEm(i=1,2,l);(2) 对nND()-ND(C),进一步有ntrueEn0;(3) 若rND(C), 则r0=r且r0trueEr;(
17、4) 若rND(C)且=true,则r0=m.此时令0为在0中增加新根结点r和一条新边所得到的STG，则证只证(1)，其他类推.为此构造基于和0结点的早弱符号互模拟S如下：令A=(n,n0)|nND()-ND(C),B=(mi,m)|i=1,2,l,Strue1=AA-1,S1=BB-1,对其他易证S=S是早弱符号互模拟.定义4.2设STG含有-边e:称e在中是可收缩的，如果e是结点m1的唯一出边且对任意边均有.用*表示将e收缩成一新结点m得到的如下STG：(1)ND(*)=ND()m-m1,m2且fn(m)=fn(m2);称该变换为-边收缩变换.若rm1,m2,则令r*=r,否则令r*=m.
18、定理4.2设-边e:在中可收缩，令*为将e收缩成新结点m所得到的STG，则定理4.1的重要性不容置疑.定理4.2在某些情况下也非常有用.对迟弱互模拟和迟观察同余也有类似的结果.因此在应用任何弱互模拟和观察同余验证算法之前，均可利用这些定理对所给STG进行化简.5互模拟验证算法对于传值进程，文献7,8分别给出了基于STG和STGA的强互模拟验证算法.在此基础上，本文给出了-演算的早强互模拟验证算法，同时将它推广至早弱互模拟和早观察同余的验证.关于谓词等式系的概念和相关记号参见文献8.-演算的早强互模拟验证算法如下：bisim (, )=PES:=close (r,r,)其输入是两个根结点分别为r
19、和r的有穷STG和, 输出为一谓词等式系.与文献8不同，该算法从初始项对(r,r,)开始，通过函数close为每对匹配项(m,n,)引入谓词变元Xm,n和相应的谓词等式，从而使算法的描述和正确性证明变得清晰而简单.同时通过在函数close与match中引入W分量以记录搜索过的匹配项对，使我们无须事先确定所有的匹配环路入口，因此我们的算法更为实用和自然.其中NAType(m,n)表示以结点m和n为起点的一步迁移中动作类型的集合，动作,x,a(x)和(x)的类型分别为,fo,in和bo.算法的正确性可由下述定理保证：定理5.1给定两个STG和, 设PES=Xm,n(,)=m,n是由上述验证算法所返
20、回的谓词等式系，(1) 若是PES的符号解且(Xm,n)(,)=,则mEn;(2) 若是PES的最大符号解且mEn,则(Xm,n)(,).证只证(1)、(2)的证明略1). 构造早强符号互模拟如下：令S1=(m,n),(n,m)|Xm,n(,)=m,nPES且(Xm,n)(,)=,S=S1|,可证S=S确为一早强符号互模拟.定理5.2设BExp, 则存在一算法可将z化简为BExp,即z.上述定理之所以成立，是因为-演算的消息值域为可数无穷多个名字的平板(坦)集.例如对=(z=uz=v)(zuzv),显然有z=(u=v).利用定理1.1和定理5.2，我们可构造一个Oracle用于判定Boole表
21、达式的蕴涵问题和化简中间结果，即使Boole表达式中由函数matchin引入了全称量词. 有了这样一个Oracle，我们就能通过如下的迭代过程自动求出上述谓词等式系的最大符号解：初始化：0(Xm,n)(,)=true;迭代步：i+1(Xm,n)(,)=m,ni;终止条件：当对所有的Xm,n(,),均有i+1(Xm,n)(,)=i(Xm,n)(,)时，i即为谓词等式系的最大符号解.定理5.3上述迭代过程在有限步终止.本文的互模拟验证算法必须包括迭代过程才算完整.与文献36中的算法相比，符号迁移图和谓词等式系的产生过程是非常高效的，但迭代过程的效率不易精确估算.初步的实验表明我们的整个算法仍是高效
22、的.为了判定STG的早弱互模拟/早观察同余问题，我们必须首先将给定的STG和变换为相应的ESOG/ESCG和. 早弱互模拟/早观察同余的验证算法类似于上述算法，但必须作用于和之上.因此如定义3.2、定理3.2和3.3所揭示的，不仅应将match换成相应的match，而且还必须将matchin修改成：关于早弱互模拟和早观察同余验证算法，我们有相应的定理来保证其正确性.6结束语本文以符号迁移图为-演算进程的表示模型，提出了基于STG的强/弱早互模拟等价和早观察同余的符号验证算法.这一结果不仅将Hennessy和Lin关于传值进程的强互模拟验证算法推广至-演算，而且第1次给出了弱互模拟等价和观察同余
23、的符号验证算法.我们希望将-演算的互模拟验证算法和模型检验算法集成起来，设计和实现一个非平凡的宽谱的自动验证工具，促使进程代数的研究从理论走向实际应用.致谢本文第一作者特别感谢林惠民研究员在课题研究中提供的宝贵资料和对本文初稿提出的改进意见，同时对博士生钟广军、荔建琦所提供的帮助表示感谢.*国家“八六三”高技术计划和国家自然科学基金资助项目(批准号：69873045)1)Li Z J. Checking strong/weak bisimulation equivalences and observation congruence for value-passing processes and
24、 the -calculus processes. Ph D Theis, National University of Defense Technology, Changsha, 1998作者单位：国防科技大学计算机系，长沙410073参考文献1Milner R, Parrow J, Walker D. A calculus of mobile processes. Part I, II. Information and Computation, 1992, 100: 1772Milner R. Communication and Concurrency. New York: Prentic
25、e-Hall, 19893Dam M. On the decidabiliy of process equivalence for the -calculus. Theoretical Computer Science, 1997, 183: 2142284Montanari U, Pistore M. Checking bisimilarity for finitary -calculus. In: CONCUR95, LNCS 962. Berlin: Springer-Verlag, 19955Pistore M, Sangiorgi D. A partition refinement
26、algorithm for the -calculus. In: CAV96, LNCS 1 102. Berlin: Spinger-Verlag, 19966Victor B, Moller F. The mobility workbencha tool for the -calculus. In: CAV94, LNCS 818, Berlin: Springer-Verlag, 19947Hennessy M, Lin H. Symbolic bisimulations. Theoretical Computer Science, 1995, 138: 3533898Lin H. Sy
27、mbolic transition graph with assignment. In : CONCUR96, LNCS 1 119. Berlin: Springer-Verlag, 19969Boreale M, De Nicola R. A symbolic semantics for the -calculus. In: CONCUR94, LNCS 836. Berlin: Springer-Verlag, 1994 10Lin H. Symbolic bisimulations and proof systems for the -calculus. Report 7/94, Co
28、mputer Science, University of Sussex, 199411Lin H. Complete inference systems for weak bisimulation equivalences in the -calculus. In: TAPSOFT95, LNCS 915. Berlin: Springer-Verlag, 199512Cleaveland R, Parrow J, Steffen B. The concurrency workbench: a semantics based verification tool for the verific
29、ation of concurrent systems. ACM Transactions on Programming Language and Systems, 1993, 15(1): 3672 附录A符号迁移图的生成规则：此处省略了关于+和|的对称规则.为使STG的生成过程尽快收敛，除使用函数new()之外，我们还可引入进程项上的结构同余关系.对于有穷控制-演算的任意进程项，均可由上述规则生成满足定义1.1的有穷STG.对于-演算的扩展项xyt和t,我们也有类似于x=yt的规则.需要指出的是，对于形如tz/x的进程项，我们总假定z对t中的x是可代入的，否则需要对t中的约束名进行换名以避免冲突.