概率时间交替μ-演算的可满足性与模型检测研究
| 摘要 | 第5-7页 |
| abstract | 第7-8页 |
| 第一章 绪论 | 第13-19页 |
| 1.1 研究背景及意义 | 第13-14页 |
| 1.2 国内外研究现状 | 第14-16页 |
| 1.3 本文研究内容 | 第16-17页 |
| 1.4 本文组织结构 | 第17-18页 |
| 1.5 本章小结 | 第18-19页 |
| 第二章 基础知识与概念 | 第19-29页 |
| 2.1 概率并发博弈结构 | 第19-23页 |
| 2.2 时间交替μ-演算 | 第23-24页 |
| 2.2.1 AMC语法 | 第23页 |
| 2.2.2 AMC语义 | 第23-24页 |
| 2.3 概率模态μ-演算 | 第24-25页 |
| 2.3.1 PμTL语法 | 第24-25页 |
| 2.3.2 PμTL语义 | 第25页 |
| 2.4 概率时间交替时态逻辑 | 第25-27页 |
| 2.4.1 PATL与PATL*语法 | 第26页 |
| 2.4.2 PATL与PATL*语义 | 第26-27页 |
| 2.5 奇偶自动机 | 第27页 |
| 2.6 本章小结 | 第27-29页 |
| 第三章 概率时间交替μ-演算 | 第29-41页 |
| 3.1 PAMC语法 | 第29-31页 |
| 3.2 PAMC语义 | 第31-35页 |
| 3.3 可满足性问题与模型检测问题概述 | 第35-40页 |
| 3.4 本章小结 | 第40-41页 |
| 第四章 可满足性问题研究 | 第41-69页 |
| 4.1 预模型 | 第41-50页 |
| 4.2 PAMC可满足性判定算法 | 第50-61页 |
| 4.2.1 非形式化描述 | 第50-54页 |
| 4.2.2 形式化归约 | 第54-61页 |
| 4.3 良性预模型的构建 | 第61-67页 |
| 4.4 复杂度分析 | 第67-68页 |
| 4.5 本章小结 | 第68-69页 |
| 第五章 模型检测问题研究 | 第69-74页 |
| 5.1 PAMC模型检测算法 | 第69-72页 |
| 5.2 复杂度分析 | 第72-73页 |
| 5.3 本章小结 | 第73-74页 |
| 第六章 PAMCSolver工具与实验 | 第74-83页 |
| 6.1 PAMCSolver工具介绍 | 第74-77页 |
| 6.2 实验分析 | 第77-82页 |
| 6.3 本章小结 | 第82-83页 |
| 第七章 总结与展望 | 第83-85页 |
| 参考文献 | 第85-91页 |
| 致谢 | 第91-93页 |
| 学术科研情况 | 第93页 |
