《π-演算的符号迁移图及其早互模拟验证算法》由会员分享，可在线阅读，更多相关《π-演算的符号迁移图及其早互模拟验证算法（14页珍藏版）》请在金锄头文库上搜索。
1、-演算的符号迁移图及其早互模拟验证算法演算的符号迁移图及其早互模拟验证算法* *李舟军 陈火旺 王兵山摘要摘要 提出符号迁移图作为 -演算进程直观而高效的表示模型，并给出了 符号迁移图多种版本(强/弱，基/符号)的早操作语义，在此基础上定义了相应 版本的早互模拟和观察同余.同时引入了符号观察图和符号同余图以及 -循环 和 -边消去定理. 最后给出了关于强/弱早互模拟等价和早观察同余的符号验 证算法，并证明了其正确性. 将关于传值进程的强互模拟验证算法和关于纯 CCS 的弱互模拟和观察同余的验证技术融合和推广至有穷控制 -演算. 关键词关键词 -演算演算 符号迁移图符号迁移图 互模拟互模拟 观察
2、同余观察同余 谓词等式系谓词等式系-演算1是 Milner 在其代表作通信系统演算 CCS2的基础上提出 的移动通信演算，其不同之处在于允许进程之间传送通道名.因此 -演算具有 很强的表达能力，可描述动态演变的系统.目前关于 -演算的一个研究热点是互模拟验证算法.已有的验证算法可分 为两类：一类基于传统的划分求精算法(partition refinement algorithm) 35，划分求精算法本身是高效的.但待验证进程的有穷迁移图的生成过程既繁琐又低效，且生成的迁移图相对庞大，此类方法对弱互模拟的验证尤为困难. 另一类采用“on the fly”方法验证开互模拟6，进程的状态空间是动态生
3、 成的，由于需要不断的回溯，该算法的时空效率均较差.因此能否将 Hennessy 和 Lin7,8关于传值进程的强互模拟验证算法推广至 -演算，是一个令人关注的问题3,9.由于 -演算允许传名和限名，以及通 道名和值的混用，这一推广远非平凡.至于对实际应用中最为重要的弱互模拟等 价和观察同余，是否存在相应的符号验证算法，更是一个尚未解决的难题 3,7,8.本文提出了 -演算的符号迁移图及其生成规则，并给出了符号迁移图多 种版本(强/弱，基/符号)的早操作语义和早互模拟定义，同时提出了这些互模 拟的符号验证算法，对于迟互模拟，我们也得到了类似的结果1)，限于篇幅不再赘述.1 1 -演算和符号迁移
4、图演算和符号迁移图令是通道名的可数无穷集，其元素用 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的函数，满足： Ev(x=
5、x)=true; 若 x 不同于 y，则 Ev(x=y)=false. 用 vx表示文献9中的 Boole 表达式 Rx( ).等名式是上等名测试(形如 x=y)的有穷合取式，条件式是上等名测 试或不等名测试(形如 xy)的有穷合取式.等名式和条件式也可看成名字测试 的有穷集.显然等名式和条件式均为 Boole 表达式之特例.令 和 *分别为在 -演算中扩充了形如xyt 和 t 的项所得到的语言.本文结果不仅对 - 演算成立，而且对 和 *均成立.我们总假定 V 为的有穷集，并用 new(V)表示不属于 V 的最小名字 x. 用 n( )表示出现在 中的名字集.若 n( )V, 则称 为 V
6、上的 Boole 表达式. 对于 -演算，我们只涉及形如的有穷替换.若则记故当 xn(),y=x 当且仅当 y=x. 表示空替换，表示替换 与 的复合，xz表示将 在 x 处的值修改为 z 的替换. V 表示 在 V 上的限制.称替换 满足 , 记作如果 Ev( )=true. 表示对任意替换 ，只要就有 , = 表示 且 .设 B 为 Boole 表达式的 有穷集，如果B=,则称 B 为一个 -划分.称 Boole 表达式 为协调的，若不 存在 x,y，使得x=y 且xy.称12m为 V 上的 Boole 表 达式 的析取范式，如果 =12m且每个i均为 V 上的协调条件式. 同样地，可定义
7、合取范式.利用范式和文献11中的命题 2.1，易证得定理定理 1.11.1 对于任意 Boole 表达式 和 ， 是可判定的.设 为 V 上协调的条件式.称 为 V 上极大协调的，如果对任意 x,yV, 或 者x=y 或者xy.称条件式 为 在 V 上的极大协调扩张，如果 且 为 V 上极大协调的.用 MCEV( )表示协调条件式 在 V 上极大协调扩张的 集合.当12m为 V 上的 Boole 表达式 的析取范式时，记 MCDV( )为并称 MCDV( )为 在 V 上的极大协调析取子.利用析取范式和文献11中的引理 2.2，可知下列定理成立：定理定理 1.21.2 若 为 V 上的 Boo
8、le 表达式，则MCDV( )= .下面我们引入符号迁移图作为 -演算进程的直观而紧凑的表示模型.令 SAct=a(x), x, (x)|a,x,Act=ax, x, (x) |a,x,其中 (x)为导出的约束输出动作，而 ax 为自由输入动作，是为 刻画早基互模拟特意引入的.并引入记号：若 , 则 =.定义定义 1.11.1 符号迁移图(简称 STG)是一具有根结点的有向图，其每个结点 n 标有一有穷自由名字集 fn(n), 每条边标有由 Boole 表达式和符号动作组成的序偶，且满足：如果是从结点 m 到 n 的一条边，则有 fn( ,)fn(m),fn(n)fn(m)bn()且 bn()
9、fn( )= .符号迁移图中的限制条件 bn()fn( )= 只是为了保证 -循环和 -边消去定理(见下面的定理 4.1 和 4.2)的正确性.对于有穷控制 -演算(包括 和 *)的任意进程项，均可利用附录 A 中的规则生成其有穷符号迁移图.2 2 早强操作语义和早强互模拟早强操作语义和早强互模拟给定给定 STGGSTGG, 其状态 n由结点 n 和替换 构成， 可用于对结点 n 出边上 的 Boole 表达式计值以导出基迁移.用 p,q 表示状态.若 p 为状态 n,则用 px z表示状态 nxz,p 表示状态 n,fn(p)表示自由名集 fn(n).定义定义 2.12.1 STG 的早强基
10、操作语义是状态上的基迁移关系，可由下列规则给 出：定义定义 2.22.2 状态上的对称二元关系 R 称为早强基互模拟，如果(m,n)R 且 Act 蕴涵：只要且 bn()fn(m,n)= , 就有且(m,n)R. 用 men表示存在一个早强基互模拟 R,使得(m,n) R. 称 m与 n是早强互模拟的，记作 men, 如果对任意替换 有 men. 称两个 STG和是早强互模拟的，如果 r er , 其中 r 和 r分别是和的根结点.对于给定的 STG, 其项 n亦由一结点 n 和一替换 构成，也可记作(n,). n实际上表示 nfn(n), 即 限制于 fn(n). 我们用 t,u 表示项，同
11、样地可定义记号 txz,t 和 fn(t).如果替换 不用于对结点 n 出边上 的 Boole 表达式计值，而只作用于 Boole 表达式和符号动作，则可定义 STG 的 更为抽象的符号操作语义.定义定义 2.32.3 STG 的早强符号操作语义是项上的符号迁移关系，可由下列规则 给出：定义定义 2.42.4 设 S=S | BExp是由 Boole 表达式加标的项上对称二元关 系族，称 S 是早强符号互模拟，如果(t,u)S 蕴涵：只要其中 bn()fn(t,u, )= , 则存在 -划分 B, 满足 fn(B)bn()fn(t,u, ),且对任意 B,存在使得其中用表示存在一个早强符号互模
12、拟 S 使得(t,u)S . 两个 STG和称为相对于 早强符号互模拟的，如果其中 r 和 r分别为和的根结点.早强符号互模拟与早强基互模拟具有下列关系：定理定理 2.12.1 当且仅当对任意证证 ()令 R=(t,u)|且 ,可证 R 为早强基互模拟.() 令可证 S=S 为早强符号互模拟.证毕.3 3 早弱操作语义和早弱互模拟早弱操作语义和早弱互模拟为定义 STG 的早弱操作语义，首先引入 STG 结点间的早符号双迁移关系如 下：注意，对于 STG 中的路径：必须引入形如：的双迁移关系，以便区分 x 的自由和约束出现.对于约束输出动作 (x)，由于 x 不同于其他已 知名，故可将随后 -迁
13、移中的 Boole 表达式 用 vx 替换，以避免 x 的这种 混用，因而无需引入类似规则.定义定义 3.13.1 STG 状态上的早基双箭头关系由下列规则给出：类似于文献11, 可定义早弱基互模拟e, 早弱互模拟e, 早基观察同 余e和早观察同余e.定义定义 3.23.2 STG 项上的早符号双箭头关系由下列规则给出：引理引理 3.13.1 若则必有下列情况之一成立：(1) =true,= 且 t=t；(2) 若 , 则否则(3) 存在 t,1,2, 使得且 =12;(4) 存在 t,1,2, 使得且 =12.定义定义 3.33.3 设 S=S | BExp是由 Boole 表达式加标的项上
14、对称二元关 系族.称 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.13.1 (1) 当且仅当对任意(2) 当且仅当对任意下面仅依赖早符号双箭头关系给出早弱符号互模拟的另一等价刻画，它是 我们
15、的早弱互模拟验证算法的基石.定理定理 3.23.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.33.3 项 t,u 是相对于 早符号观察同余的，即, 当且仅当对任意 ,a(x), x, (x),只要其中 bn()fn(t,u, )= , 则存在 -划分 B, 满足fn(B)bn()fn(t,u, ),且对任意 B,存在使得其中对 u 有对称的性质成立.4 4 早符号观察图和早符号同余图早符号观察图和早符号同余图基于早符号双迁移、定理 3.2 和 3.3，可将观察图和同余图12推广至早 符号观察图(ESOG)和早符号同余图(ESCG)，以构造早弱互模拟和早观察同余的 验证算法.对于
