| 摘要 | 第5-7页 |
| ABSTRACT | 第7-8页 |
| 符号对照表 | 第12-16页 |
| 缩略语对照表 | 第16-20页 |
| 第一章 绪论 | 第20-30页 |
| 1.1 时序逻辑 | 第20-23页 |
| 1.1.1 投影时序逻辑及其研究现状 | 第22-23页 |
| 1.2 空间逻辑 | 第23-25页 |
| 1.2.1 分离逻辑及其研究现状 | 第24-25页 |
| 1.3 时空逻辑 | 第25-28页 |
| 1.3.1 形式化验证中的时空逻辑 | 第25-26页 |
| 1.3.2 其它领域中的时空逻辑 | 第26-28页 |
| 1.4 论文的主要工作与组织结构 | 第28-30页 |
| 第二章 技术背景 | 第30-48页 |
| 2.1 命题投影时序逻辑 | 第30-34页 |
| 2.2 一阶投影时序逻辑 | 第34-36页 |
| 2.3 分离逻辑 | 第36-46页 |
| 2.3.1 程序验证示例 | 第42-46页 |
| 2.4 本章小结 | 第46-48页 |
| 第三章 时空逻辑PPTLSL | 第48-82页 |
| 3.1 分离逻辑的一种可判定片段 | 第48-51页 |
| 3.2 SL的时序扩展 | 第51-53页 |
| 3.2.1 空间结构演化性质描述 | 第52-53页 |
| 3.3 从PPTLSL到PPTL | 第53-75页 |
| 3.3.1 等价可满足转换 | 第53-65页 |
| 3.3.2 判定过程 | 第65-74页 |
| 3.3.3 判定复杂度 | 第74-75页 |
| 3.4 基于SMT的PPTLSL公式的可满足性检查 | 第75-79页 |
| 3.4.1 从SL到SMT-LIB | 第75-78页 |
| 3.4.2 工具SAT-PPTLSL | 第78-79页 |
| 3.5 本章小结 | 第79-82页 |
| 第四章 内存演化性质验证 | 第82-98页 |
| 4.1 建模、仿真和验证语言MSVL | 第83-86页 |
| 4.2 指针程序和内存演化性质 | 第86-91页 |
| 4.3 基于SMT的统一模型检测 | 第91-96页 |
| 4.3.1 基本方法 | 第91-92页 |
| 4.3.2 模型检测器 | 第92-93页 |
| 4.3.3 验证实例 | 第93-96页 |
| 4.4 本章小结 | 第96-98页 |
| 第五章 智能规划中的时空搜索控制知识 | 第98-126页 |
| 5.1 智能规划问题 | 第98-101页 |
| 5.2 搜索控制知识 | 第101-107页 |
| 5.2.1 启发性规划问题 | 第103-107页 |
| 5.3 时空搜索控制知识描述 | 第107-112页 |
| 5.4 基于时空搜索控制知识的规划过程 | 第112-116页 |
| 5.5 IPC标准规划问题实验 | 第116-123页 |
| 5.5.1 PDDL的空间扩展 | 第116页 |
| 5.5.2 标准规划问题 | 第116-120页 |
| 5.5.3 空间公式转换的改进 | 第120-121页 |
| 5.5.4 实验结果分析 | 第121-123页 |
| 5.6 本章小结 | 第123-126页 |
| 第六章 总结与展望 | 第126-130页 |
| 6.1 工作总结 | 第126-127页 |
| 6.2 研究展望 | 第127-130页 |
| 附录 | 第130-138页 |
| 参考文献 | 第138-158页 |
| 致谢 | 第158-160页 |
| 作者简介 | 第160-162页 |