| 基于符号迁移图的互模拟验证算法 |
| |
| 引用本文： | 李舟军,陈火旺.基于符号迁移图的互模拟验证算法[J].计算机工程与科学,2002,24(2):34-41. |
| |
| 作者姓名： | 李舟军 陈火旺 |
| |
| 作者单位： | 1. 国防科技大学计算机学院,湖南,长沙,410073;武汉大学软件工程国家重点实验室,湖北,武汉,430072
2. 国防科技大学计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 国家自然科学基金资助项目 (60 0 73 0 0 1，6993 3 0 3 0 )，高等学校重点实验室访问学者基金资助项目 |
| |
| 摘 要： | 符号迁移图是传值进程的一种直观而简洁的语义表示模型，该模型由Hennessy和Lin首先提出，随后又被Lin推广至带赋值的符号迁移图，本文不但定义了符号迁移图各种版本（基／符号）的强操作语义和强互模拟，提出了相互的强互模拟算法，而且通过引入符号观察图和符号同余图，给出了其弱互模拟等价和观察同余的验证算法，给出并证明了了τ－循环和τ－边消去定理，在应用任何弱互模拟观察同余验证算法之前，均可利用这些定理对所给符号迁移图进行化简。
|
| 关 键 词： | 符号迁移图 互模拟验证算法 互模拟 谓词等式系 计算机 |
| 文章编号： | 1007-130X(2002)02-0034-08 |
Bisimulation Checking Algorithms Based on Symbolic Transition Graphs |
| |
| LI Zhou jun ,CHEN Huo wang.Bisimulation Checking Algorithms Based on Symbolic Transition Graphs[J].Computer Engineering & Science,2002,24(2):34-41. |
| |
| Authors: | LI Zhou jun CHEN Huo wang |
| |
| Affiliation: | LI Zhou jun 1,2,CHEN Huo wang 1 |
| |
| Abstract: | 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 |
| |
| Keywords: | Value passing processes symbolic transition graph bisimulation observation congruence predicate equation system |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
