投影时序逻辑的完备公理系统与形式验证
| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 第一章 绪论 | 第11-19页 |
| ·研究背景与意义 | 第11-12页 |
| ·形式化方法 | 第12-14页 |
| ·模型检测 | 第13页 |
| ·定理证明 | 第13-14页 |
| ·时序逻辑 | 第14-16页 |
| ·相关研究工作 | 第16-17页 |
| ·论文的主要工作与组织结构 | 第17-19页 |
| 第二章 投影时序逻辑 | 第19-27页 |
| ·语法 | 第19-20页 |
| ·语义 | 第20-22页 |
| ·PTL操作符特点分析 | 第22-24页 |
| ·一些特殊形式的PTL公式 | 第24-25页 |
| ·小结 | 第25-27页 |
| 第三章 PTL的公理系统 | 第27-53页 |
| ·PTL的公理系统 | 第27-30页 |
| ·公理系统的可靠性 | 第30-40页 |
| ·常用定理 | 第40-51页 |
| ·小结 | 第51-53页 |
| 第四章 有穷时间PTL公理系统的完备性 | 第53-83页 |
| ·PTL的范式 | 第53-66页 |
| ·范式的定义 | 第53-55页 |
| ·范式的存在性 | 第55-62页 |
| ·范式的计算算法 | 第62-66页 |
| ·范式图 | 第66-79页 |
| ·范式图的定义 | 第66-69页 |
| ·范式图的构造算法 | 第69-77页 |
| ·范式图的一些性质 | 第77-79页 |
| ·范式图的局限性 | 第79页 |
| ·有穷时间PTL的判定算法 | 第79-81页 |
| ·有穷时间公理系统的完备性证明 | 第81页 |
| ·小结 | 第81-83页 |
| 第五章 无穷时间PTL公理系统的完备性 | 第83-129页 |
| ·标记范式与标记范式图的引入 | 第83-85页 |
| ·标记范式 | 第85-90页 |
| ·标记范式的定义 | 第85-86页 |
| ·标记范式的计算算法 | 第86-90页 |
| ·标记范式图 | 第90-93页 |
| ·QFPTL公式的判定算法 | 第93-113页 |
| ·QFPTL公式LNFG的特殊性质 | 第93-101页 |
| ·LNFG的化简 | 第101-104页 |
| ·QFPTL的判定算法 | 第104-108页 |
| ·QFPTL的判定实例 | 第108-113页 |
| ·PTL公式的判定算法 | 第113-126页 |
| ·从QPTL到QFPTL的转换 | 第115-126页 |
| ·PTL的判定算法 | 第126页 |
| ·PTL公理系统的完备性证明 | 第126-128页 |
| ·小结 | 第128-129页 |
| 第六章 基于PTL的形式化验证 | 第129-149页 |
| ·PTL与完全正则语言 | 第129-133页 |
| ·完全正则语言 | 第129-131页 |
| ·从FRE到PTL公式 | 第131-132页 |
| ·从PTL公式到FRE | 第132-133页 |
| ·使用PTL进行系统建模 | 第133-138页 |
| ·MSVL | 第134-136页 |
| ·扩展Kripke结构 | 第136-138页 |
| ·验证实例 | 第138-146页 |
| ·问题描述 | 第138-139页 |
| ·系统建模 | 第139-141页 |
| ·系统验证 | 第141-146页 |
| ·小结 | 第146-149页 |
| 第七章 总结与展望 | 第149-153页 |
| ·论文总结 | 第149-150页 |
| ·进一步的研究展望 | 第150-153页 |
| 致谢 | 第153-154页 |
| 参考文献 | 第154-161页 |
| 攻读博士学位期间的研究成果 | 第161页 |
