模型检测时态知识逻辑及其应用
| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第1章 绪论 | 第8-10页 |
| 第2章 模型检测技术 | 第10-20页 |
| ·时态逻辑 | 第10-14页 |
| ·模型检测的原理 | 第14-15页 |
| ·二值判定图 | 第15-18页 |
| ·符号化模型检测 | 第18-20页 |
| 第3章 知识与多智能体系统 | 第20-30页 |
| ·知识的定义 | 第20-26页 |
| ·多智能体系统中的知识 | 第26-30页 |
| 第4章 模型检测时态知识逻辑 | 第30-38页 |
| ·时态知识逻辑CKL_n | 第30-32页 |
| ·符号化模型检测CKL_n | 第32-35页 |
| ·时态知识逻辑的模型检测工具MCTK | 第35-38页 |
| 第5章 应用一：验证对弈中的必胜策略 | 第38-44页 |
| ·引言 | 第38-39页 |
| ·对弈模型及其验证方法 | 第39-41页 |
| ·实例分析 | 第41-43页 |
| ·小结 | 第43-44页 |
| 第6章 应用二：验证基于知识的安全协议 | 第44-54页 |
| ·引言 | 第44-45页 |
| ·验证保密家就餐协议 | 第45-48页 |
| ·验证俄罗斯牌协议 | 第48-52页 |
| ·小结 | 第52-54页 |
| 第7章 总结及展望 | 第54-56页 |
| 参考文献 | 第56-66页 |
| 附录A 井字棋的模型描述 | 第66-70页 |
| 附录B 保密家就餐协议的模型和规范描述 | 第70-72页 |
| 附录C 俄罗斯牌协议的模型和规范描述 | 第72-78页 |
| 发表论文情况 | 第78-79页 |
| 致谢 | 第79-80页 |
| 原创性声明 | 第80页 |
