资源描述：
《π-演算的符号迁移图及其早互模拟验证算法》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。
1、π-演算的符号迁移图及其早互模拟验证算法*李舟军 陈火旺 王兵山摘要 提出符号迁移图作为π-演算进程直观而高效的表示模型，并给出了符号迁移图多种版本(强/弱，基/符号)的早操作语义，在此基础上定义了相应版本的早互模拟和观察同余.同时引入了符号观察图和符号同余图以及τ-循环和τ-边消去定理.最后给出了关于强/弱早互模拟等价和早观察同余的符号验证算法，并证明了其正确性.将关于传值进程的强互模拟验证算法和关于纯CCS的弱互模拟和观察同余的验证技术融合和推广至有穷控制π-演算.关键词 π-演算 符号迁移图 互模拟 观察同余 谓词等式系 π-演算［1］是Mi
2、lner在其代表作——通信系统演算CCS［2］的基础上提出的移动通信演算，其不同之处在于允许进程之间传送通道名.因此π-演算具有很强的表达能力，可描述动态演变的系统. 目前关于π-演算的一个研究热点是互模拟验证算法.已有的验证算法可分为两类：一类基于传统的划分求精算法(partitionrefinementalgorithm)［3～5］，划分求精算法本身是高效的.但待验证进程的有穷迁移图的生成过程既繁琐又低效，且生成的迁移图相对庞大，此类方法对弱互模拟的验证尤为困难.另一类采用“onthefly”方法验证开互模拟［6］，进程的状态空间是动态生成的，由于
3、需要不断的回溯，该算法的时空效率均较差. 因此能否将Hennessy和Lin［7,8］关于传值进程的强互模拟验证算法推广至π-演算，是一个令人关注的问题［3,9］.由于π-演算允许传名和限名，以及通道名和值的混用，这一推广远非平凡.至于对实际应用中最为重要的弱互模拟等价和观察同余，是否存在相应的符号验证算法，更是一个尚未解决的难题［3,7,8］. 本文提出了π-演算的符号迁移图及其生成规则，并给出了符号迁移图多种版本(强/弱，基/符号)的早操作语义和早互模拟定义，同时提出了这些互模拟的符号验证算法，对于迟互模拟，我们也得到了类似的结果1)，限于篇幅不
4、再赘述.1 π-演算和符号迁移图 令是通道名的可数无穷集，其元素用a,x,y,z表示.π-演算由如下BNF语法给出：关于这些算子的含义参见文献［1,9,10］.在a(x).t和(x)t中，x为具有辖域t的约束名.由此引出进程项t的约束名字集bn(t)和自由名字集fn(t).为了描述π-演算的符号语义和验证算法，下面首先引入关于Boole表达式的可判定理论.Boole表达式由如下BNF语法给出：我们用BExp表示Boole表达式的集合，其元素用,ψ表示.其他逻辑联结词∨和→均是作为缩写引入的.计值Ev是从BExp至｛true,false｝的函数，满足：E
5、v(x=x)=true;若x不同于y，则Ev(x=y)=false.用vx表示文献［9］中的Boole表达式Rx(). 等名式是上等名测试(形如x=y)的有穷合取式，条件式是上等名测试或不等名测试(形如x≠y)的有穷合取式.等名式和条件式也可看成名字测试的有穷集.显然等名式和条件式均为Boole表达式之特例.令π≠和π*分别为在π-演算中扩充了形如［x≠y］t和t的项所得到的语言.本文结果不仅对π-演算成立，而且对π≠和π*均成立. 我们总假定V为的有穷集，并用new(V)表示不属于V的最小名字x.用n()表示出现在中的名字集.若n()V,则称为V上
6、的Boole表达式.对于π-演算，我们只涉及形如的有穷替换.若则记故当x∈n(σ),yσ=x当且仅当y=x.表示空替换，σσ′表示替换σ与σ′的复合，σ［xz］表示将σ在x处的值修改为z的替换.σV表示σ在V上的限制. 称替换σ满足,记作如果Ev(σ)=true.ψ表示对任意替换σ，只要就有σψ,=ψ表示ψ且ψ.设B为Boole表达式的有穷集，如果∨B=χ,则称B为一个χ-划分.称Boole表达式为协调的，若不存在x,y∈，使得x=y且x≠y.称1∨2∨…∨m为V上的Boole表达式的析取范式，如果=1∨2∨…∨m且每个i均为V上的协调条件式.同样地，
7、可定义合取范式.利用范式和文献［11］中的命题2.1，易证得 定理1.1 对于任意Boole表达式和ψ，ψ是可判定的. 设为V上协调的条件式.称为V上极大协调的，如果对任意x,y∈V,或者x=y或者x≠y.称条件式′为在V上的极大协调扩张，如果′且′为V上极大协调的.用MCEV()表示协调条件式在V上极大协调扩张的集合.当1∨2∨…∨m为V上的Boole表达式的析取范式时，记MCDV()为并称′∈MCDV()为在V上的极大协调析取子.利用析取范式和文献［11］中的引理2.2，可知下列定理成立： 定理1.2 若为V上的Boole表达式，则∨MCDV(
8、)=. 下面我们引入符号迁移图作为π-演算进程的直观而紧凑的表示模型.令SAc
