良结构下推系统上的可终止性和有界性问题研究

摘要

在形式化验证领域，下推系统（pushdown systems）常用来建模单线程递归程序，良结构迁移系统（well-structured transition systems），比如向量加法系统（vector addition systems），常用来建模非递归多线程程序。结合这两种系统及目前对于递归并发程序分析的需求，Cai和Ogawa提出了建模递归并发程序的框架：良结构下推系统（well-structured pushdown systems）[1]。良结构下推系统可以看做是下推系统和良结构迁移系统的结合：与下推系统比较，它将下推系统的状态集和栈字符集从有限集扩展为良拟序集（well quasi order）；与良结构迁移系统比较，它在良结构迁移系统的基础上配置了一个栈。良结构下推系统的表达能力十分强大，但其上的很多模型检测问题的可判定性目前都还是公开问题。本文我们主要研究良结构下推系统的可终止性问题及有界性问题：
　　扩展了删枝可达树算法[2]证明良结构下推系统的可终止性和有界性问题是可判定的，在扩展的删枝可达树上证明了一个良结构下推系统有一条无限长的路径当且仅当它的删枝可达树中包含一个可泵节点（pumpable node），一个严格良结构下推系统的可达集是无限的当且仅当它的删枝可达树中包含一个严格可泵节点（strictly pumpable node）；
　　提出另外一种证明良结构下推系统的可终止性和有界性问题的可判定性的算法：后继自动机算法（P ost?-automata algorithm）。证明了一个良结构下推系统是不可终止的当且仅当它的简化后继自动机（reduced P ost?-automaton）中存在一条可泵边（pumpable edge），一个严格良结构下推系统是无界的当且仅当它的简化后继自动机中存在一条严格可泵边（strictly pumpable edge）；
　　通过将格局迁移路径抽象为嵌套序列（nested sequence），利用嵌套序列的一些性质证明了良结构下推系统的子模型受控良结构下推系统（bounded well-structured pushdown systems）的删枝可达树的大小的上界为高阶阿克曼的（hyper-Ackermannian）；下界则由受控良结构下推系统的一类子模型的下界得到，也是高阶阿克曼的；
　　证明了一个良结构下推系统的删枝可达树与简化后继自动机的关系：一个良结构下推系统的删枝可达树中包含一个可泵节点当且仅当它的简化后继自动机中存在一条可泵边。并证明了简化后继自动机的大小的上下界与删枝可达树的大小的上下界相同。
　　为了比较两种算法的实际效率，我们设计并实现了这两种算法，并提出一个良结构下推系统的随机模型生成测试样本，在这些样本上分析比较两种算法的效率；实验结果表明在一些简单的良结构下推系统实例上两种算法的表现不相上下，但在复杂的实例上后继自动机算法比删枝可达树算法要快很多数量级，而删枝可达树算法只在简单的实例上运行速度比较快。

目录

声明

主要符号对照表

第一章 绪论

1.1 研究背景

1.2 本文贡献

1.3 相关工作

1.4 章节安排

第二章 背景知识

2.1 良拟序

2.2 良结构迁移系统

2.3 下推系统和P-automata

2.4 本章小结

第三章 良结构下推系统

3.1 良结构下推系统

3.2 良结构下推系统的表达能力

3.3 可终止及有界性问题

3.4 本章小结

第四章 删枝可达树算法

4.1 良结构下推系统的可达树

4.2 可终止性问题

4.3 有界性问题

4.4 本章小结

第五章 后继自动机算法

5.1 依赖关系

5.2 可终止性问题

5.3 有界性问题

5.4 本章小结

第六章 复杂性分析

6.1 快速增长函数

6.2 良拟序上的嵌套序列

6.3 复杂性分析

6.4 本章小结

第七章 实现及实验

7.1 算法设计与实现

7.2 随机模型

7.3 实验结果分析

7.4 本章小结

全文总结

参考文献

致谢

攻读学位期间发表的学术论文

攻读学位期间参与的项目