Institutional Repository
| 模态逻辑公式为见证的互模拟等价判定 | |
| 李明 | |
| Supervisor | 柳欣欣 |
| 2009-05-20 | |
| Degree Grantor | 中国科学院研究生院 |
| Degree Level | 硕士 |
| Place of Degree Grantor | 中国科学院软件研究所 |
| Keyword | 形式化验证 有限状态进程 强互模拟 分支互模拟 诊断公式 |
| English Abstract | 判定两个进程是否具有某种等价关系，是形式化验证的重要组成部分，很多种等价关系被定义出来以满足不同的验证需求，强互模拟等价和分支互模拟等价是其中两个重要的两种等价关系。强互模拟等价可以用HML(Hennessy-Milner Logic)逻辑刻画，分支互模 拟等价可以用HMLU(HML with Until)等逻辑刻画。两个模型不能强互模拟等价或者分支互模拟等价时，存在一个作为见证的相应逻辑描述的公式，该公式只能被其中一个模型满足，称之为诊断公式。诊断公式的意义在于有助于分析理解模型为什么不具有相应的等价关系，给出诊断公式是对判定算法有意义的扩充。修改后的PT(Paige-Tarjan)算法可以用于计算有限状态进程之间的强互模 拟等价关系，修改后的GV(Groote-Vaandrager)算法可以用于计算分支互模拟，对它们相应的扩充可以为不能强互模拟等价或分支互模拟等价的进程生成诊断公式。 主要工作如下：分析为强互模拟等价和分支互模拟等价生成诊断公式的方法。设计处理有限状态进程表达式并将其转化为标号迁移系统的算法。扩展PT 算法，使其适用于标号迁移系统，并在判定强互模拟等价的过程中为不能强互模拟的进程生成HML 描述的诊断公式。扩展GV 算法，使其能够在判定标号迁移系统上分支互模拟的同时，为不能分支互模拟的进程生成HMLU 描述的诊断公式。 |
| Subject | 计算机科学技术基础学科其他学科 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/109 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | 李明. 模态逻辑公式为见证的互模拟等价判定[D]. 中国科学院软件研究所. 中国科学院研究生院,2009. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 200628015029010_pape（489KB） | 开放获取 | License | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment