无限状态系统上分支互模拟等价验证

摘要

等价验证是自动验证领域的主流方法之一，另一个主流方法是模型检测。等价验证研究的重点是互模拟等价验证。互模拟等价验证起始于上世纪80年代。互模拟等价验证研究关注的模型大都是无限状态系统，大部分无限状态系统都可以在一个一般的框架—进程重写系统(Process Rewrite System,PRS)中定义。从上世纪80年代开始，有大量进程重写系统上互模拟等价验证的工作。这些工作表明在进程重写系统上进行弱互模拟等价验证是非常困难的，主要体现在两个方面：其一,在绝大部分无限状态系统上，如进程重写系统中BPA或BPP之上的模型，弱互模拟等价验证是不可判定的；其二,在非常基本的无限状态系统—BPA和BPP上，弱互模拟等价验证的判定性至今仍然是公开的。与此同时，弱互模拟等价的一个加细版本—分支互模拟等价最近被证明在赋范BPA和赋范BPP上都是可判定的。分支互模拟等价与弱互模拟等价的区别是前者区分了改变状态的内部动作和不改变状态的内部动作，并且要求只有不改变状态的内部动作才可以忽略。从自动验证角度看，分支互模拟等价是比弱互模拟等价更恰当的等价关系。本文的研究聚焦在进程重写系统上分支互模拟等价验证问题上，关注的是这类问题的可判定性，算法及复杂性，主要贡献有以下几个方面。
　　BPA和BPP等价验证下界。通过构造从EXPTIME-完备问题Hit-or-Run博弈到赋范BPA上的分支互模拟博弈的一个归约，本文证明了赋范BPA上的分支互模拟等价验证有EXPTIME-难下界。这与目前赋范BPA分支互模拟等价验证最好的上界是匹配的，同时也与弱互模拟等价验证目前最好的下界一致。另外，通过构造量词化可满足性问题到赋范BPP上的分支互模拟博弈的一个归约，本文证明了赋范BPP上的分支互模拟等价验证是PSPACE-难的。这与BPP上弱互模拟等价验证的目前最好的下界一致。此外，本文同时证明了这两个下界对介于分支互模拟与弱互模拟之间的所有等价关系在对应的模型上也是成立的。
　　赋范BPA分支互模拟正则性复杂性。本文证明了赋范BPA上分支互模拟正则性的复杂性介于PSPACE和EXPTIME之间。为了证明上界，我们利用赋范BPA上的分支互模拟等价判定的指数时间算法，设计了一个指数时间算法判定一个给定的赋范BPA进程是否是分支互模拟正则；为了证明下界，我们构造了一个从量词化可满足性问题的归约。本文同时证明了，PSPACE-难下界对于弱互模拟正则性也成立。
　　进程重写系统上分支互模拟等价验证的不可判定性。通过构造一个从Post字对应问题到赋范进程代数上分支互模拟博弈的归约，本文证明了分支互模拟验证在赋范进程代数上是不可判定的。另外，本文将Mayr关于单计数器网上的弱互模拟等价不可判定的结论推广到了分支互模拟等价验证上。此外，本文说明了这两个归约对介于分支互模拟等价与弱互模拟等价之间所有等价关系都是成立的。根据进程重写系统的表达能力分层，分支互模拟等价验证在进程重写系统分层中存在一条明显的可判定界线。
　　下推系统上分支互模拟等价验证的高阶不可判定性。本文证明了在下推系统上分支互模拟等价验证是高阶不可判定的。更具体的讲，证明了这个问题落在分析谱系的第一层，并且是Σ11-完备的。即使限制内部动作为入栈操作，分支互模拟验证也是Σ11-完备的。这个结果与弱互模拟行等价验证在下推系统上的高阶不可判定性一致。
　　技术贡献。为了完成本文的研究，本文推广了经典的防御者力迫技术，设计了适用于分支互模拟博弈的防御力迫技术—防御者语义力迫技术。

目录

声明

主要符号对照表

第一章 引言

1.1 研究背景

1.2 研究现状

1.3 相关工作

1.4 本文贡献

1.5 章节安排

第二章 基本术语

2.1 互模拟关系

2.2 互模拟等价的博弈刻画

2.3 经典防御者力迫技术

2.4 防御者语义力迫技术

2.5 进程重写系统

2.6 本章小结

第三章 分支互模拟等价验证下界

3.1 冗余变量

3.2 二进制表示

3.3 nBPA上的EXPTIME-难下界

3.4 nBPP上的PSPACE-难下界

3.5 本章小结

第四章 BPA分支正则性判定复杂性

4.1 研究问题

4.2 EXPTIME上界

4.3 非正则性充要条件

4.4 PSPACE-难下界

4.5 本章小结

第五章 进程重写系统的不可判定性

5.1 nPA的不可判定性

5.2 OCN的不可判定性

5.3 本章小结

第六章 下推系统的高阶不可判定性

6.1 研究动机

6.2 证明思路

6.3 计数器

6.4 控制流

6.5 PDA∈+的高阶不可判定性

6.6 nPDA∈+的可判定性探讨

6.7 本章小结

第七章 全文总结

7.1 主要结论

7.2 工作展望

附录A 第三章证明

A.1 引理3.1的证明

A.2 引理3.3的证明

A.3 命题3.6的证明

A.4 引理3.12的证明

A.5 引理3.15的证明

附录B 第四章证明

B.1 引理4.12的证明

附录C 第五章证明

C.1 推论5.3的证明

C.2 引理5.7的证明

附录D 第六章证明

D.1 命题6.3的证明

D.2 引理6.4的证明

参考文献

致谢

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

攻读学位期间参与的项目