| 摘要 | 第5-7页 |
| ABSTRACT | 第7-8页 |
| 符号对照表 | 第12-14页 |
| 缩略语对照表 | 第14-18页 |
| 第一章 绪论 | 第18-32页 |
| 1.1 定理证明 | 第19页 |
| 1.2 模型检测 | 第19-22页 |
| 1.2.1 基于自动机的模型检测 | 第21-22页 |
| 1.2.2 基于BDD的符号模型检测 | 第22页 |
| 1.3 时序逻辑 | 第22-26页 |
| 1.3.1 基于区间的时序逻辑 | 第23-25页 |
| 1.3.2 时序逻辑在开放系统中的应用 | 第25-26页 |
| 1.4 多智能体系统 | 第26-29页 |
| 1.4.1 多智能体系统的应用 | 第27-28页 |
| 1.4.2 多智能体系统的形式化验证方法研究现状 | 第28-29页 |
| 1.5 本文的研究目的和主要工作 | 第29-31页 |
| 1.6 论文的组织结构 | 第31-32页 |
| 第二章 交替投影时序逻辑 | 第32-46页 |
| 2.1 并发博弈结构 | 第32-34页 |
| 2.2 基于并发博弈结构的自动机 | 第34-37页 |
| 2.3 基于区间的交替时序逻辑 | 第37-40页 |
| 2.3.1 AITL语法语义 | 第37-38页 |
| 2.3.2 APTL语法语义 | 第38-40页 |
| 2.4 运算符优先级 | 第40页 |
| 2.5 APTL的逻辑规则 | 第40-43页 |
| 2.6 APTL公式的应用 | 第43-44页 |
| 2.7 小结 | 第44-46页 |
| 第三章 APTL符号模型检测 | 第46-78页 |
| 3.1 APTL的判定方法 | 第46-64页 |
| 3.1.1 范式定义 | 第46-50页 |
| 3.1.2 范式构造算法 | 第50-54页 |
| 3.1.3 范式图 | 第54-58页 |
| 3.1.4 构造BCG | 第58-60页 |
| 3.1.5 BCG的化简及判定方法 | 第60-64页 |
| 3.2 二值判断图 | 第64-69页 |
| 3.2.1 状态集合的特征函数 | 第67-69页 |
| 3.2.2 迁移关系集合的特征函数 | 第69页 |
| 3.3 APTL符号模型检测方法 | 第69-75页 |
| 3.3.1 解释系统 | 第70-71页 |
| 3.3.2 符号化表示解释系统 | 第71页 |
| 3.3.3 APTL符号模型检测算法 | 第71-75页 |
| 3.4 小结 | 第75-78页 |
| 第四章 APTL模型检测器 | 第78-94页 |
| 4.1 可满足性检查工具 | 第78-87页 |
| 4.1.1 工具框架 | 第78-79页 |
| 4.1.2 语法树构造 | 第79-80页 |
| 4.1.3 构造BCG过程 | 第80-84页 |
| 4.1.4 实例展示 | 第84-86页 |
| 4.1.5 实验分析 | 第86-87页 |
| 4.2 符号模型检测器 | 第87-90页 |
| 4.2.1 MCMAS | 第87-88页 |
| 4.2.2 MCMAS APTL框架 | 第88页 |
| 4.2.3 MCMAS APTL的实现过程 | 第88-90页 |
| 4.2.4 实例展示 | 第90页 |
| 4.3 小结 | 第90-94页 |
| 第五章 模型检测器MCMAS APTL的应用 | 第94-112页 |
| 5.1 解释系统编程语言 | 第94-95页 |
| 5.2 单点登录系统 | 第95-102页 |
| 5.2.1 Open ID协议 | 第96-97页 |
| 5.2.2 基于Open ID协议的SSO系统验证 | 第97-102页 |
| 5.3 机器人足球赛 | 第102-110页 |
| 5.3.1 机器人足球赛的策略模型 | 第102-104页 |
| 5.3.2 实验展示 | 第104-110页 |
| 5.4 小结 | 第110-112页 |
| 第六章 论文总结和未来工作 | 第112-116页 |
| 6.1 论文总结 | 第112-113页 |
| 6.2 未来工作 | 第113-116页 |
| 参考文献 | 第116-128页 |
| 致谢 | 第128-130页 |
| 作者简介 | 第130-132页 |