基于模拟理论的模型检测研究
| 摘要 | 第1-6页 |
| Abstract | 第6-11页 |
| 1 引言 | 第11-26页 |
| ·研究背景，目的及意义 | 第11-13页 |
| ·国内外概况 | 第13-24页 |
| ·主要研究工作 | 第24-26页 |
| 2 基本概念 | 第26-33页 |
| ·线性时序逻辑 | 第26-27页 |
| ·CTL~* | 第27-28页 |
| ·自动机 | 第28页 |
| ·博弈 | 第28-30页 |
| ·基于自动机的模型检测的原理 | 第30-31页 |
| ·LTL公式转换为自动机 | 第31-32页 |
| ·语言判空算法 | 第32页 |
| ·小结 | 第32-33页 |
| 3 基于K-模拟的Büchi自动机的优化 | 第33-60页 |
| ·引言 | 第33页 |
| ·普通模拟及其不足 | 第33-37页 |
| ·K-模拟的定义 | 第37-40页 |
| ·模拟博弈的构造 | 第40-43页 |
| ·基于博弈的模拟关系的计算 | 第43-47页 |
| ·K-模拟的性质 | 第47-51页 |
| ·Büchi自动机的优化 | 第51-59页 |
| ·小结 | 第59-60页 |
| 4 广义Büchi自动机的优化 | 第60-69页 |
| ·引言 | 第60-61页 |
| ·广义Büchi自动机的模拟 | 第61-63页 |
| ·基于模拟的广义Büchi自动机优化 | 第63-65页 |
| ·基于on-the-fly方法的GBA转化为BA | 第65-68页 |
| ·小结 | 第68-69页 |
| 5 基于左右语言的迁移系统优化 | 第69-80页 |
| ·引言 | 第69页 |
| ·优化的理论基础 | 第69-71页 |
| ·基于左语言的Kripke结构的优化 | 第71-72页 |
| ·基于左右语言的Büchi自动机优化 | 第72-78页 |
| ·基于左右语言的广义Büchi自动机的优化 | 第78-79页 |
| ·小结 | 第79-80页 |
| 6 基于广义Büchi自动机公平模拟的组合验证 | 第80-91页 |
| ·引言 | 第80页 |
| ·组合验证的思想 | 第80-83页 |
| ·模拟关系和系统组合 | 第83-86页 |
| ·性质保存 | 第86-87页 |
| ·最大结构 | 第87-90页 |
| ·基于公平模拟的A | 第90页 |
| ·小结 | 第90-91页 |
| 7 基于普通K-模拟的抽象 | 第91-103页 |
| ·引言 | 第91页 |
| ·抽象的作用及存在的问题 | 第91页 |
| ·抽象的理论基础及常见技术 | 第91-97页 |
| ·抽象框架 | 第97-98页 |
| ·抽象的计算 | 第98-100页 |
| ·基于模块化的抽象 | 第100-101页 |
| ·抽象的可靠性和完备性 | 第101-102页 |
| ·小结 | 第102-103页 |
| 8 总结与展望 | 第103-106页 |
| ·全文总结 | 第103-104页 |
| ·研究展望 | 第104-106页 |
| 致谢 | 第106-107页 |
| 参考文献 | 第107-114页 |
| 附录1 攻读学位期间发表的学术论文 | 第114页 |
