| 摘要 | 第3-4页 |
| Abstract | 第4-5页 |
| 目录 | 第6-7页 |
| 第1章 前言 | 第7-11页 |
| 第2章 预备知识 | 第11-19页 |
| 2.1 Kripke结构 | 第11-12页 |
| 2.2 Buchi自动机 | 第12-13页 |
| 2.3 线性时序逻辑(LTL)的语法和语义 | 第13-14页 |
| 2.4 计算树逻辑的语法与语义 | 第14-16页 |
| 2.5 可能性Kripke结构 | 第16-17页 |
| 2.6 基于可能性Kripke结构的计算树逻辑(PoCTL) | 第17-18页 |
| 2.7 本章小结 | 第18-19页 |
| 第3章 多处理器任务调度算法TDS的建模与验证 | 第19-33页 |
| 3.1 TDS算法介绍 | 第19-21页 |
| 3.2 多处理器调度算法TDS的模型 | 第21-26页 |
| 3.3 算法合理性描述 | 第26-27页 |
| 3.4 扩展Buchi自动机对应的Kripke结构 | 第27页 |
| 3.5 应用不动点算法进行模型检测 | 第27-31页 |
| 3.6 本章小结 | 第31-33页 |
| 第4章 基于可能性测度的工程管理决策的研究 | 第33-43页 |
| 4.1 带有成本的可能性Kripke结构 | 第33-36页 |
| 4.2 可达性质的期望成本(收益) | 第36-37页 |
| 4.3 多种属性的决策 | 第37-39页 |
| 4.4 融合了成本的PoCTL—PoCCTL | 第39-40页 |
| 4.5 对于工程管理决策问题的验证 | 第40-41页 |
| 4.6 本章小结 | 第41-43页 |
| 总结 | 第43-45页 |
| 参考文献 | 第45-49页 |
| 致谢 | 第49-51页 |
| 攻读硕士学位期间的研究成果 | 第51页 |