| 摘要 | 第1-6页 |
| Abstract | 第6-11页 |
| 图表清单 | 第11-12页 |
| 注释表 | 第12-13页 |
| 第一章 绪论 | 第13-24页 |
| ·形式化方法 | 第13-14页 |
| ·转换系统 | 第14-15页 |
| ·互模拟及其模态逻辑特征 | 第15-17页 |
| ·互模拟概念 | 第15-16页 |
| ·互模拟的模态特征 | 第16-17页 |
| ·行为近似等价理论 | 第17-21页 |
| ·行为近似等价理论研究背景 | 第17-18页 |
| ·近似互模拟方法和度量方法 | 第18-20页 |
| ·近似等价理论的应用案例1:软件正确性与可靠性的统一框架 | 第20-21页 |
| ·近似等价理论的应用案例2:控制器的形式化设计与验证 | 第21页 |
| ·本文的主要工作 | 第21-23页 |
| ·本文的内容安排 | 第23-24页 |
| 第二章 基于λ-互模拟的行为拟度量 | 第24-36页 |
| ·λ-互模拟和Breugel的猜想 | 第24-27页 |
| ·λ-行为拟度量 | 第27-30页 |
| ·函数d_I的不动点刻画 | 第30-34页 |
| ·本章小结 | 第34-36页 |
| 第三章 (η,α)-互模拟和分岔距离 | 第36-59页 |
| ·(η,α)-互模拟概念 | 第36-43页 |
| ·(η,α)-互模拟诱导出的距离函数 | 第43-45页 |
| ·分岔距离的互模拟刻画:非死锁情形 | 第45-50页 |
| ·分岔距离与(η,α)-互模拟:非死锁—有限分岔情形 | 第50-53页 |
| ·(η,α)-互模拟的分层 | 第53-57页 |
| ·本章小结 | 第57-59页 |
| 第四章 交替近似互模拟的逻辑特征 | 第59-78页 |
| ·交替转换系统、交替互模拟及其逻辑特征 | 第59-63页 |
| ·交替近似互模拟 | 第63-65页 |
| ·ATL_ε逻辑、H_(Ag)~ε和E_Ag~ε | 第65-70页 |
| ·交替近似互模拟的模态逻辑特征 | 第70-77页 |
| ·本章小结 | 第77-78页 |
| 第五章 交替转换系统的控制策略算法 | 第78-95页 |
| ·交替转换系统和LTL_(-X)(P) | 第79-81页 |
| ·Kabanza等人的规划算法 | 第81-85页 |
| ·控制策略算法 | 第85-94页 |
| ·本章小结 | 第94-95页 |
| 第六章 控制策略算法的完备性 | 第95-105页 |
| ·预备知识 | 第95-96页 |
| ·控制策略算法的完备性证明 | 第96-104页 |
| ·本章小结 | 第104-105页 |
| 第七章 带扰动控制系统的形式化设计 | 第105-137页 |
| ·带扰动线性系统及其有限抽象 | 第106-110页 |
| ·带扰动的线性控制系统 | 第107-108页 |
| ·带扰动的线性控制系统的有限抽象 | 第108-110页 |
| ·线性时序逻辑LTL_(-X) | 第110-117页 |
| ·规范转换 | 第117-126页 |
| ·转换∑的规范到T_τ(∑)的规范 | 第119-121页 |
| ·转换T_τ(∑)的规范到有限抽象的规范 | 第121-126页 |
| ·基于有限抽象控制策略的控制器 | 第126-133页 |
| ·相关工作讨论 | 第133-135页 |
| ·本章小结 | 第135-137页 |
| 第八章 总结 | 第137-139页 |
| 附录 | 第139-146页 |
| 参考文献 | 第146-151页 |
| 致谢 | 第151-152页 |
| 在学期间的研究成果及发表的学术论文 | 第152页 |
