| 弱互模拟等价类算法改进 |
| 其他题名 | Improving the Algorithms for Computing Weak Bisimulation Equivalences
|
| 李伟松
|
| 导师 | 张文辉
|
| 2009-06-02
|
| 学位授予单位 | 中国科学院研究生院
|
| 学位 | 硕士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 关键词 | 模型检测
|
| 摘要 | 大量的硬件和软件系统广泛应用在一些重要的领域，在许多情况下错误和失效是不可接受的。需要提供方法来检验软硬件的正确性，增强我们对软硬件系统的信心。形式化验证提供了提高软硬件可靠性的方法。
互模拟等价类和弱互模拟等价类可以用来降低形式化验证中模型的规模。弱互模拟等价类有两种算法：一种是先计算迁移关系的自反传递闭包，然后调用互模拟等价类的算法。另一种是作为IGPTPartEF的一个特例，直接在原图上用划分精化的方法计算。针对这些计算弱互模拟等价类的算法，我们提出两种改进算法。
首先，我们观察到有些状态在划分精化的过程中不会被再次切分，可以事先将它们归类到一个组，在划分精化过程中以这些组为基本单位进行切分，可以在很大程度上减小算法花费的时间。我们用该思想给设计出了改进算法一。
然后，我们观察在Paige-Tarjan算法中引入了“处理比较小的一半”的思想来改进计算互模拟等价类的算法，它使得计算互模拟等价类的算法的时间复杂度从O(mn)（其中m是边数，n是顶点数）改进到O(mlgn)，而在前面所述的弱互模拟等价类算法中并没有引入“处理比较小的一半”。我们引入这一思想，设计出了改进算法二。
之后，我们设计实现了原型工具，并进行了数据实验来证实算法在时间上与原算法相比有明显改进。 |
| 学科领域 | 计算机可靠性理论
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/183
|
| 专题 | 基础软件与系统重点实验室
|
推荐引用方式
GB/T 7714 |
李伟松. 弱互模拟等价类算法改进[D]. 中国科学院软件研究所. 中国科学院研究生院,2009.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论