| 摘要 | 第1-12页 |
| ABSTRACT | 第12-14页 |
| 第一章 绪论 | 第14-32页 |
| ·引言 | 第14-18页 |
| ·模型检验技术及其特点 | 第15-17页 |
| ·时序逻辑的推理及检验 | 第17-18页 |
| ·研究目标及主要结果 | 第18-21页 |
| ·相关研究工作回顾 | 第21-30页 |
| ·从显式模型检验到符号化模型检验 | 第22-25页 |
| ·时序逻辑的推理与公理化 | 第25-28页 |
| ·ω-正规性质的检验方法 | 第28-30页 |
| ·本文组织结构 | 第30-32页 |
| 第二章 自动机、时序逻辑以及符号化模型检验 | 第32-68页 |
| ·ω-自动机 | 第32-40页 |
| ·字、树、布尔公式 | 第33-36页 |
| ·ω-自动机的定义及其分类 | 第36-40页 |
| ·时序逻辑 | 第40-57页 |
| ·线性结构及分支结构 | 第40-41页 |
| ·LTL、CTL、CTL* | 第41-46页 |
| ·MSOL、QTL、μ-演算 | 第46-51页 |
| ·从ETL 到PSL | 第51-55页 |
| ·公式的可满足性及有效性 | 第55-57页 |
| ·符号化模型检验 | 第57-68页 |
| ·模型检验问题 | 第57-60页 |
| ·二叉决策图：BDD | 第60-62页 |
| ·基于BDD 的 CTL 符号化模型检验 | 第62-68页 |
| 第三章 ETL 的公理化及其逻辑片断的实例公理化方法 | 第68-114页 |
| ·引言 | 第68-70页 |
| ·ETL_l 的公理系统L | 第70-81页 |
| ·ETL_l 重写系统及迁移图 | 第70-76页 |
| ·ETL_l 公理系统及可靠性、完备性 | 第76-81页 |
| ·ETL_f 的公理系统F | 第81-97页 |
| ·ETL_f 重写系统及迁移图 | 第81-85页 |
| ·ETL_f 公理系统及可靠性、完备性 | 第85-97页 |
| ·ETL_r 的公理系统R | 第97-107页 |
| ·ETL_r 重写系统及迁移图 | 第97-100页 |
| ·ETL_r 公理系统及可靠性、完备性 | 第100-107页 |
| ·ETL逻辑片断的实例化公理化 | 第107-113页 |
| ·本章小结 | 第113-114页 |
| 第四章 基于博弈的μ-演算公理化 | 第114-152页 |
| ·引言 | 第114-115页 |
| ·模态μ-演算的博弈系统及公理系统 | 第115-144页 |
| ·模态μ-演算的相关概念 | 第115-120页 |
| ·模态μ-演算的博弈系统 | 第120-132页 |
| ·模态μ-演算公理系统：完备性的证明 | 第132-143页 |
| ·相关工作 | 第143-144页 |
| ·线性μ-演算的博弈系统及公理系统 | 第144-151页 |
| ·线性μ-演算的相关概念及博弈系统 | 第144-147页 |
| ·线性μ-演算公理系统：完备性的证明 | 第147-150页 |
| ·相关工作 | 第150-151页 |
| ·本章小结 | 第151-152页 |
| 第五章 基于tableau 的交错ETL 和APSL 符号化模型检验 | 第152-210页 |
| ·引言 | 第152-154页 |
| ·公共概念及性质 | 第154-157页 |
| ·ATL_f 符号化模型检验 | 第157-168页 |
| ·ATL_f 公式的tableau | 第157-166页 |
| ·基于BDD 的ATL_f tableau 编码 | 第166-168页 |
| ·ATL_l 符号化模型检验 | 第168-175页 |
| ·ATL_l 公式的tableau | 第168-174页 |
| ·基于BDD 的 ATL_l tableau 编码 | 第174-175页 |
| ·ATL_r 符号化模型检验 | 第175-193页 |
| ·ATL_r 公式带rank 的拒绝例证 | 第175-180页 |
| ·ATL_r 公式的tableau | 第180-191页 |
| ·基于BDD 的 ATL_r tableau 编码 | 第191-193页 |
| ·APSL 符号化模型检验 | 第193-207页 |
| ·PSL 的变种：APSL | 第193-198页 |
| ·AFL 公式的tableau | 第198-205页 |
| ·基于BDD 的 AFL tableau 编码 | 第205-207页 |
| ·本章小结 | 第207-210页 |
| 第六章 线性μ-演算的符号化模型检验 | 第210-242页 |
| ·引言 | 第210-211页 |
| ·一般形式的线性μ-演算的符号化模型检验 | 第211-229页 |
| ·线性μ-演算公式的自动机表示 | 第212-219页 |
| ·从交错parity 自动机到非确定 B¨uchi 自动机 | 第219-224页 |
| ·检验算法及符号化实现 | 第224-229页 |
| ·特定形式的线性μ-演算的符号化模型检验 | 第229-241页 |
| ·线性μ-演算范式及迟滞迁移系统 | 第229-239页 |
| ·检验算法的符号化实现 | 第239-241页 |
| ·本章小结 | 第241-242页 |
| 第七章 扩展的符号化模型检验工具：ENuSMV | 第242-266页 |
| ·引言 | 第242-244页 |
| ·ENuSMV 基础语法及语法扩展 | 第244-252页 |
| ·NuSMV 原有语法 | 第244-248页 |
| ·ENuSMV 扩展语法 | 第248-251页 |
| ·ENuSMV 验证执行过程 | 第251-252页 |
| ·实验结果 | 第252-265页 |
| ·ETL_f 模型检验结果 | 第252-259页 |
| ·AFL 模型检验结果 | 第259-265页 |
| ·本章小结 | 第265-266页 |
| 第八章 结束语 | 第266-268页 |
| ·本文的主要工作 | 第266页 |
| ·进一步的工作 | 第266-268页 |
| 致谢 | 第268-270页 |
| 参考文献 | 第270-280页 |
| 作者在学期间取得的学术成果 | 第280页 |
