超协调时序逻辑及其模型检测方法
| 摘要 | 第1-5页 |
| Abstract | 第5-7页 |
| 目录 | 第7-10页 |
| 第一章 绪论 | 第10-24页 |
| ·形式刻画中的非协调性问题 | 第11-16页 |
| ·相关工作 | 第16-21页 |
| ·目的和意义 | 第21-22页 |
| ·本文组织 | 第22-24页 |
| 第二章 超协调逻辑基础 | 第24-38页 |
| ·超协调性 | 第25-29页 |
| ·超协调逻辑系统 | 第29-34页 |
| ·超协调逻辑的应用 | 第34-38页 |
| 第三章 超协调时序逻辑系统 QCTL | 第38-54页 |
| ·时序逻辑介绍 | 第39-41页 |
| ·基本概念 | 第39-41页 |
| ·时序逻辑的分类 | 第41页 |
| ·QCTL 时序逻辑语法 | 第41-43页 |
| ·语义:paraKripke 结构 | 第43-54页 |
| 第四章 证明系统 | 第54-78页 |
| ·证明系统介绍 | 第55-61页 |
| ·分解和合成规则 | 第55-58页 |
| ·QCTL 推理关系 | 第58-61页 |
| ·可靠性和完备性 | 第61-78页 |
| ·证明系统的可靠性 | 第61-67页 |
| ·证明系统的完备性 | 第67-78页 |
| 第五章 QCTL 的表达能力 | 第78-86页 |
| ·QCTL 与 QCL | 第79-81页 |
| ·QCTL 与 CTL | 第81-86页 |
| 第六章 模型检测 | 第86-106页 |
| ·模型检测的介绍 | 第87-90页 |
| ·基于 QCTL 的模型检测问题 | 第90-99页 |
| ·paraKripke 模型的定义 | 第90-92页 |
| ·paraKripke 模型的性质 | 第92-99页 |
| ·算法基础 | 第99-106页 |
| 第七章 QCTL 的应用 | 第106-118页 |
| ·非协调性的管理框架 | 第106-109页 |
| ·实例分析 | 第109-118页 |
| 第八章 结论及展望 | 第118-124页 |
| ·结论 | 第119-121页 |
| ·展望 | 第121-124页 |
| 参考文献 | 第124-137页 |
| 致谢 | 第137页 |
