论文部分内容阅读
提出符号迁移图作为π 演算进程直观而高效的表示模型 ,并给出了符号迁移图多种版本 (强 /弱 ,基 /符号 )的早操作语义 ,在此基础上定义了相应版本的早互模拟和观察同余 .同时引入了符号观察图和符号同余图以及τ 循环和τ 边消去定理 .最后给出了关于强 /弱早互模拟等价和早观察同余的符号验证算法 ,并证明了其正确性 .将关于传值进程的强互模拟验证算法和关于纯CCS的弱互模拟和观察同余的验证技术融合和推广至有穷控制π 演算 .
A symbolic transition graph is proposed as an intuitive and efficient representation model of πcalculation process. The semantics of early operation of various versions of symbolic transition graph (strong / weak, base / symbol) are given. Based on this, Simulation and observation of congruence.At the same time introduced the symbol observation and the symbolic congruence graph and the τ-cycle and τ-edge elimination theorem.Finally, we give the symbolic verification algorithm for the equivalence and early observation congruency of strong / The correctness is proved, and the strong mutual simulation verification algorithm about the pass-through process and the weak mutual simulation and observation congruence verification techniques on pure CCS are fused and extended to the finite control π calculus.