| 1 简介 | 第1-10页 |
| 2 背景知识 | 第10-17页 |
| ·带标识的迁移图 | 第10页 |
| ·模态μ演算 | 第10-12页 |
| ·博弈 | 第12-17页 |
| 3 上下文无关进程上的互模拟及其博弈刻画 | 第17-31页 |
| ·带标识的重写迁移图 | 第17-19页 |
| ·上下文无关进程上的互模拟 | 第19-25页 |
| ·互模拟博弈 | 第25-31页 |
| 4 模态μ演算上的可满足性博弈及其在模型检测上的应用 | 第31-49页 |
| ·Hennessy-Milner逻辑上的可满足性博弈 | 第31-34页 |
| ·模态μ演算上的可满足性博弈 | 第34-44页 |
| ·基于可满足性博弈的模型检测 | 第44-49页 |
| 5 进一步的工作 | 第49-50页 |
| 参考文献 | 第50-52页 |