| 摘要 | 第3-5页 |
| Abstract | 第5-6页 |
| 第一章 绪论 | 第9-17页 |
| 1.1 研究背景与意义 | 第9-11页 |
| 1.2 模型检测技术研究现状 | 第11-14页 |
| 1.3 本文的主要工作 | 第14-17页 |
| 第二章 预备知识 | 第17-27页 |
| 2.1 Kripke结构 | 第17-18页 |
| 2.2 时态逻辑 | 第18-21页 |
| 2.2.1 线性时序逻辑(LTL) | 第18-19页 |
| 2.2.2 计算树逻辑(CTL) | 第19-20页 |
| 2.2.3 分支时态逻辑(CTL~*) | 第20-21页 |
| 2.3 模糊集和模糊矩阵的基本概念 | 第21-22页 |
| 2.4 可能性测度理论 | 第22-23页 |
| 2.5 广义可能性Kripke结构及其广义可能性测度 | 第23-25页 |
| 2.6 Knaster-Tarski不动点定理 | 第25-27页 |
| 第三章 基于决策过程的广义可能性CTL模型检测 | 第27-53页 |
| 3.1 广义可能性决策过程 | 第27-36页 |
| 3.2 广义可能性计算树逻辑 | 第36-38页 |
| 3.3 广义可能性计算树模型检测 | 第38-48页 |
| 3.4 实例应用 | 第48-52页 |
| 3.5 本章小结 | 第52-53页 |
| 第四章 基于决策过程的广义可能性线性时间属性模型检测 | 第53-79页 |
| 4.1 广义可能性线性时间属性 | 第53-58页 |
| 4.2 广义可能性线性时间属性的可达可能性 | 第58-69页 |
| 4.2.1 最终可达事件的可能性 | 第58-60页 |
| 4.2.2 总是可达事件的可能性 | 第60-62页 |
| 4.2.3 限制可达事件的可能性 | 第62-64页 |
| 4.2.4 重复可达事件的可能性 | 第64-66页 |
| 4.2.5 持久可达事件的可能性 | 第66-69页 |
| 4.3 广义可能性线性时间属性的可能性测度 | 第69-76页 |
| 4.3.1 广义可能性正则安全属性的可能性测度 | 第69-73页 |
| 4.3.2 广义可能性ω-正则属性的可能性测度 | 第73-76页 |
| 4.4 本章小结 | 第76-79页 |
| 第五章 基于决策过程的GPoCTL~*模型检测和可能性互模拟 | 第79-101页 |
| 5.1 GPoCTL~*语法和语义 | 第79-80页 |
| 5.2 GPoLTL模型检测算法 | 第80-90页 |
| 5.2.1 GPoLTL PNF语法和语义 | 第80-82页 |
| 5.2.2 GPoLTL模型检测算法 | 第82-90页 |
| 5.3 GPoCTL~*模型检测算法 | 第90-92页 |
| 5.4 最大可能性互模拟及其逻辑刻画 | 第92-100页 |
| 5.4.1 最大可能性互模拟 | 第92-95页 |
| 5.4.2 GPoCTL/GPoCTL~*与最大可能性互模拟的等价性 | 第95-100页 |
| 5.5 本章小结 | 第100-101页 |
| 第六章 总结与展望 | 第101-103页 |
| 6.1 研究内容的总结 | 第101-102页 |
| 6.2 研究展望 | 第102-103页 |
| 参考文献 | 第103-115页 |
| 致谢 | 第115-117页 |
| 攻读博士学位期间的研究成果 | 第117页 |
