软件的安全性问题越来越突出,当下,除了应用同行评审和软件测试等进行验证外,还可应用形式化验证在项目早期尽快发现软件缺陷。形式化验证指采取数学方式对软件系统建模并分析,目的是通过严格的数学推理来建立正确的系统。而且,对于一些要求较高安全性的系统而言,形式化方法是最佳的验证技巧。对这些系统的验证一般是通过提供基于系统的抽象数学模型上的形式化证明、数学模型和被验证的系统之间的相关性来实现的。当前,用于建模系统的一些数学模型包括:有限状态集,标记迁移系统,Petri网,向量加法系统,时间自动机,进程代数等。并发理论是理论计算机科学中众多一直比较活跃的研究领域之一。一些用于建模和验证并发系统的形式化模型被相继提出,比如Petri网和向量加法系统、进程演算等。尽管Petri网主要是提供在物理世界上的计算方法,而向量加法系统主要用于并发编程的形式化模型,但之后他们被证明是数学上等价的。向量加法系统由有限个整数向量组成,系统的格局是自然数向量的集合,每一步的迁移是对当前的格局应用一个整数向量而到达另一个格局。向量加法系统上的一些研究主要围绕的问题包括可达性问题、可覆盖性问题等。为了增加向量加法系统的表达能力,在其基础上进行扩增又衍生出了一些其他模型,如带状态的向量加法系统、递归向量加法系统、交替向量加法系统等。Cai和Ogawa将下推系统和向量加法系统相结合,提出良结构下推系统,可用于建模递归多线程程序。良结构下推系统具有强大的表达能力,向量加法系统及一些对其扩展的模型可被规约到良结构下推系统上,例如分支向量加法系统、递归向量加法系统等。因此,良结构下推系统的研究结论可直接被用于这些模型上。尽管向量加法系统的扩展模型的一些可覆盖性问题还未被解决,但可以对该问题的难度进行一定的衡量,即可以通过寻找该问题难度的上界和下界,通过二者之间差距的不断缩小而确定。本文提出一个用于证明模型可覆盖性问题下界的一般性框架,并基于重置0(即不测试一个变量值的情况下直接对其赋值为0),利用规约的方式得到下界。基于本文提出的框架,验证了下推向量加法系统的可覆盖性问题的难度下界为TOWER难的,与已知的Lazic提出的下界难度相一致。并证明了对以3维自然数向量为状态的且栈字符集有限的良结构下推系统和状态集有限且以3维自然数向量为栈字符集的良结构下推系统,其可覆盖性问题的难度下界是Ackermann难的;状态集有限且栈字符集为n+3维良拟序集的良结构下推系统,其可覆盖性问题的下界是Hyper-Ackermann难的。本文还提出良结构的带有范围限制匹配关系的多栈下推系统(简记为WSMPDS),对多栈下推系统中的弹栈操作进行限制,即仅当一个栈顶符号是上k个轮回里被压入栈中的才可被执行弹栈操作(其中k为某个固定的常量),而且栈字符集为良拟序集,然后介绍其可覆盖性问题的定义。并通过向量加法系统的可覆盖性问题到此模型的可覆盖性问题的规约,得出了其可覆盖性问题的下界是EXPSPACE难的。