| 摘要 | 第1-5页 |
| Abstract | 第5-8页 |
| 第一章 绪论 | 第8-14页 |
| ·研究背景 | 第8-10页 |
| ·存在的问题 | 第8页 |
| ·可能的解决方法 | 第8-10页 |
| ·本文的研究方向 | 第10页 |
| ·研究现状 | 第10-13页 |
| ·模型检查技术研究现状 | 第11-12页 |
| ·时序逻辑研究现状 | 第12-13页 |
| ·本文的研究工作和章节安排 | 第13-14页 |
| 第二章 模型检查 | 第14-24页 |
| ·模型检查原理 | 第14-15页 |
| ·模型检查的主要方法 | 第15-16页 |
| ·模型检查技术的优点及局限性 | 第16-18页 |
| ·模型检查技术优点 | 第16-17页 |
| ·模型检查技术的局限性 | 第17-18页 |
| ·缩减状态空间的相关技术 | 第18-24页 |
| ·状态空间爆炸 | 第18页 |
| ·二叉判定图（BDD）的符号化状态空间表示 | 第18-19页 |
| ·内存管理策略 | 第19-21页 |
| ·偏序约简（Partial-order Reduction） | 第21-22页 |
| ·等价归约（Reduction through Equivalences） | 第22-24页 |
| 第三章 命题投影时序逻辑 | 第24-32页 |
| ·语法 | 第24页 |
| ·语义 | 第24-26页 |
| ·可满足性和有效性 | 第26页 |
| ·导出公式 | 第26-28页 |
| ·导出的常用操作符 | 第26-28页 |
| ·其它导出公式 | 第28页 |
| ·优先级规则 | 第28页 |
| ·等价关系 | 第28-29页 |
| ·PPTL公式的正则形与可判定性 | 第29-32页 |
| ·PPTL公式的正则形 | 第29-31页 |
| ·PPTL公式的可判定性问题 | 第31-32页 |
| 第四章 基于无穷模型PPTL公式的模型检查 | 第32-46页 |
| ·Büchi 自动机 | 第32-33页 |
| ·PPTL公式的正则图 | 第33-34页 |
| ·模型检查PPTL公式 | 第34-45页 |
| ·模型检查PPTL公式总体方案 | 第34-36页 |
| ·从PPTL公式到Büchi自动机的转化 | 第36-40页 |
| ·构造积自动机 | 第40-41页 |
| ·Büchi自动机的判空 | 第41-45页 |
| ·本章小结 | 第45-46页 |
| 第五章 模型检查器的设计 | 第46-52页 |
| ·模型检查PPTL公式与SPIN | 第47-48页 |
| ·模型检查器的设计 | 第48-49页 |
| ·实例分析 | 第49-52页 |
| 结束语 | 第52-54页 |
| 致谢 | 第54-56页 |
| 参考文献 | 第56-60页 |
| 研究成果 | 第60页 |