基于符号迁移图的互模拟验证算法  

Bisimulation Checking Algorithms Based on Symbolic Transition Graphs

作　　者：李舟军[1] 陈火旺[1] 

机构地区：[1]国防科技大学计算机学院

出　　处：《计算机工程与科学》2002年第2期34-41,共8页Computer Engineering & Science

基　　金：国家自然科学基金资助项目 (60 0 73 0 0 1;6993 3 0 3 0 );高等学校重点实验室访问学者基金资助项目

摘　　要：符号迁移图是传值进程的一种直观而简洁的语义表示模型。该模型由Hennessy和Lin首先提出 ,随后又被Lin推广至带赋值的符号迁移图。本文不但定义了符号迁移图各种版本 (基 /符号 )的强操作语义和强互模拟 ,提出了相应的强互模拟算法 ,而且通过引入符号观察图和符号同余图 ,给出了其弱互模拟等价和观察同余的验证算法 ,给出并证明了τ 循环和τ 边消去定理 ,在应用任何弱互模拟和观察同余验证算法之前 ,均可利用这些定理对所给符号迁移图进行化简。A symbolic transition graph is an intuitive and concise semantic model for value passing processes It is firstly introduced by Hennessy and Lin,and then generalized by Lin to symbolic transition graph with assignment This paper not only defines various versions of strong operational semantics and strong bisimulation for symbolic transition graphs,and proposes strong bisimulation algorithms for them,but also presents corresponding checking algorithms for weak bisimulations and observation congruence by means of symbolic observation graphs and symbolic congruence graphs Theorems ensuring the elimination of τ cycles and τ edges are given and proved,and therefore symbolic transition graphs can be simplified significantly once weak bisimulation and observation congruence are to be checked

关 键 词：符号迁移图 互模拟验证算法 互模拟 谓词等式系 计算机 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]