| 摘要 | 第1-4页 |
| Abstract | 第4-6页 |
| 目录 | 第6-7页 |
| 前言 | 第7-11页 |
| 第1章 预备知识 | 第11-15页 |
| ·线性时序逻辑(LTL) | 第11-13页 |
| ·计算树逻辑(CTL) | 第13页 |
| ·研究可能性模型检测的理论基础 | 第13-15页 |
| 第2章 可能性测度下的LTL与CTL | 第15-21页 |
| ·可能的Kripke结构 | 第15-18页 |
| ·可能的线性时序逻辑(PoLTL) | 第18页 |
| ·可能的计算树逻辑(PoCTL) | 第18-21页 |
| 第3章 可能性测度下LTL性质的研究 | 第21-33页 |
| ·可达可能性测度与可达瞬时可能性测度 | 第21-26页 |
| ·基于可能的Kripke结构的基本性质 | 第26-27页 |
| ·基于可能的Kripke结构的LTL的性质 | 第27-33页 |
| 第4章 可能性测度下对CTL的进一步研究 | 第33-45页 |
| ·公式Po_J(φ)在非运算下成立 | 第33-34页 |
| ·CTL与PoCTL的关系 | 第34-38页 |
| ·可能性测度下PoCTL的性质 | 第38-41页 |
| ·PoCTL模型检测 | 第41-45页 |
| 总结 | 第45-47页 |
| 参考文献 | 第47-51页 |
| 致谢 | 第51-53页 |
| 攻读硕士学位期间研究成果 | 第53页 |