| 1 引言 | 第1-10页 |
| ·研究背景 | 第8-9页 |
| ·本文的研究工作 | 第9页 |
| ·本文的组织结构 | 第9-10页 |
| 2 SPIN模型检测器 | 第10-18页 |
| ·概述 | 第10-11页 |
| ·SPIN的结构 | 第11-12页 |
| ·SPIN的基础 | 第12-15页 |
| ·时态逻辑属性 | 第13-15页 |
| ·核心算法 | 第15-18页 |
| ·嵌套的深度优先遍历(NDFS) | 第15-16页 |
| ·偏序规约(Partial Order Reduction) | 第16-18页 |
| 3 SPIN中的状态压缩技术 | 第18-36页 |
| ·无损压缩 | 第18-27页 |
| ·Collapse Compression | 第18-22页 |
| ·Minimized Automaton Representation | 第22-27页 |
| ·有损压缩 | 第27-36页 |
| ·Bitstate Hashing | 第27-33页 |
| ·Hash-Compact | 第33-36页 |
| 4 基于属性的状态向量优化(SOBP) | 第36-52页 |
| ·案例研究 | 第36-39页 |
| ·SOBP的使用条件 | 第39页 |
| ·SOBP的原理 | 第39-41页 |
| ·SOBP的伪码实现 | 第41-47页 |
| ·DFS算法的修改 | 第42-44页 |
| ·BFS算法的修改 | 第44-47页 |
| ·SOBP与COLLAPSE COMPRESSION的结合 | 第47-48页 |
| ·性能分析 | 第48-52页 |
| ·空间性能 | 第48-50页 |
| ·时间性能 | 第50-52页 |
| 5 结论与展望 | 第52-53页 |
| 参考文献 | 第53-56页 |
| 在学期间的研究成果 | 第56-57页 |
| 致谢 | 第57-58页 |
| 附录 | 第58-59页 |
