状态转换系统的格值量化验证方法研究
| 摘要 | 第1-8页 |
| Abstract | 第8-12页 |
| 第一章 引言 | 第12-24页 |
| ·研究背景、现状、所关注的问题 | 第12-17页 |
| ·研究思路 | 第17-19页 |
| ·主要贡献 | 第19-21页 |
| ·章节安排 | 第21-24页 |
| 第二章 预备知识 | 第24-38页 |
| ·形式化方法的基本知识 | 第24-29页 |
| ·完备剩余格 | 第29-36页 |
| ·本章小结 | 第36-38页 |
| 第三章 格值互模拟等价关系 | 第38-74页 |
| ·引言 | 第38-39页 |
| ·格值双标号转换系统 | 第39-41页 |
| ·格值互模拟关系 | 第41-56页 |
| ·格值互模拟关系的逻辑刻画 | 第56-71页 |
| ·相关工作 | 第71页 |
| ·小结 | 第71-74页 |
| 第四章 格值迹等价关系 | 第74-112页 |
| ·引言 | 第74-75页 |
| ·格值Kripke结构 | 第75-77页 |
| ·格值迹语义 | 第77-95页 |
| ·格值线性时态逻辑 | 第95-104页 |
| ·格值迹语义的逻辑刻画 | 第104-109页 |
| ·相关工作 | 第109-110页 |
| ·结论 | 第110-112页 |
| 第五章 格值模型之间的关系 | 第112-138页 |
| ·引言 | 第112-113页 |
| ·格值标号转换系统的格值互模拟关系 | 第113-119页 |
| ·LLTS和LKS相互转换 | 第119-123页 |
| ·格值计算树时态逻辑 | 第123-132页 |
| ·LHML_(?)和LML相互转换 | 第132-135页 |
| ·相关工作 | 第135-136页 |
| ·结论 | 第136-138页 |
| 第六章 格值时间自动机 | 第138-168页 |
| ·引言 | 第138-139页 |
| ·预备知识 | 第139-143页 |
| ·格值时间自动机的语法与语义 | 第143-151页 |
| ·格值时间自动机的模型检测 | 第151-162页 |
| ·D—互模拟等价关系 | 第162-166页 |
| ·相关工作 | 第166页 |
| ·结论 | 第166-168页 |
| 第七章 总结与展望 | 第168-172页 |
| ·本文总结 | 第168-169页 |
| ·未来的研究工作 | 第169-172页 |
| 附录A 攻读博士学位期间科研成果 | 第172-174页 |
| 附录B 参与的科研项目 | 第174-176页 |
| 参考文献 | 第176-188页 |
| 后记 | 第188-189页 |
