| 摘要 | 第5-6页 |
| ABSTRACT | 第6页 |
| 缩略语对照表 | 第9-12页 |
| 第一章 绪论 | 第12-18页 |
| 1.1 相关研究背景 | 第12-13页 |
| 1.2 国内外研究现状和发展趋势 | 第13-15页 |
| 1.2.1 模型检测理论的研究进展 | 第13-14页 |
| 1.2.2 LTL转换算法的研究现状和发展 | 第14-15页 |
| 1.3 论文的主要工作和内容安排 | 第15-18页 |
| 第二章 相关基础理论 | 第18-30页 |
| 2.1 线性时序逻辑 | 第18-20页 |
| 2.1.1 时序逻辑简介 | 第18页 |
| 2.1.2 LTL的定义 | 第18-19页 |
| 2.1.3 否定范式的改写规则 | 第19页 |
| 2.1.4 LTL公式的简化操作 | 第19-20页 |
| 2.2 应用到模型检测中的自动机理论 | 第20-25页 |
| 2.2.1 自动机理论的提出与发展 | 第20页 |
| 2.2.2 自动机理论的中心概念 | 第20-21页 |
| 2.2.3 典型自动机介绍 | 第21-23页 |
| 2.2.4 交替式自动机的定义 | 第23页 |
| 2.2.5 Biichi自动机的定义 | 第23-24页 |
| 2.2.6 基于迁移的广义Buchi自动机的定义 | 第24-25页 |
| 2.2.7 极弱交替式co-Buichi自动机的定义 | 第25页 |
| 2.3 CF范式 | 第25-28页 |
| 2.3.1 CF范式的定义 | 第25-26页 |
| 2.3.2 LTL公式到CF范式的改写 | 第26-27页 |
| 2.3.3 范式图 | 第27-28页 |
| 2.4 小结 | 第28-30页 |
| 第三章 经典LTL转换算法及其改进 | 第30-40页 |
| 3.1 on-the-fly直接转换算法 | 第30-34页 |
| 3.1.1 算法流程描述 | 第30-32页 |
| 3.1.2 构造带标记的有向图 | 第32-33页 |
| 3.1.3 利用有向图构造LGBA | 第33-34页 |
| 3.2 基于VWAA的转换算法 | 第34-39页 |
| 3.2.1 LTL公式到VWAA的转换 | 第35-36页 |
| 3.2.2 VWAA到TGBA的转换 | 第36-38页 |
| 3.2.3 LTL2BA改进工具LTL3BA的简要介绍 | 第38-39页 |
| 3.3 小结 | 第39-40页 |
| 第四章 基于CF范式的LTL转换改进算法 | 第40-54页 |
| 4.1 LTL公式到CF范式的转换 | 第40页 |
| 4.2 CF范式到TGBA的转换 | 第40-48页 |
| 4.2.1 CF范式到NFG的转换 | 第40-41页 |
| 4.2.2 NFG到TGBA的转换 | 第41-43页 |
| 4.2.3 基于alternating公式的改进措施 | 第43-45页 |
| 4.2.4 TGBA到BA的转换 | 第45-46页 |
| 4.2.5 自动机简化方法的改进 | 第46-47页 |
| 4.2.6 程序设计上的改进 | 第47-48页 |
| 4.3 简单实例分析 | 第48-52页 |
| 4.4 本章小结 | 第52-54页 |
| 第五章 实验结果及分析 | 第54-58页 |
| 第六章 总结与展望 | 第58-60页 |
| 6.1 本文总结 | 第58-59页 |
| 6.2 未来的研究发展 | 第59-60页 |
| 参考文献 | 第60-64页 |
| 致谢 | 第64-66页 |
| 作者简介 | 第66页 |
