论文部分内容阅读
本文致力于基于余代数的模型检测和定理证明。
形式化验证的一种主要方法是模型检测，其优势是可以自动化，并能在系统不满足性质时提供反例路径;劣势是当系统并发程度较高时，存在状态爆炸问题且一般不能验证无穷状态系统。形式化验证的另一种主要方法是定理证明，其优势是与状态无关，可以验证无穷状态系统;劣势是这种方法一般不是完全自动化的，需要人工交互。余代数是代数的对偶概念，可以描述无穷动态结构，由于有些性质是余归纳定义的，因此须用基于余代数的余归纳证明原则来验证系统是否满足这些性质。论文主要分为三部分。
第一部分，我们从余归纳的角度研究模型检测中状态空间爆炸的问题。我们用余归纳的方法证明了:(1)对于任意给定的一类Kripke结构（记为K），在互模拟等价意义下K中最小Kripke结构（记为K0）的存在唯一性。K0描述了K中所有Kripke结构的行为而且没有冗余的状态;(2)对于任意的M∈K（M可能包含无穷多个状态），在互模拟等价意义下的相对于M(且基于K0)的最小Kripke结构(记为KM)的存在唯一性。由此提出一个求解KM的算法并用Ocaml予以简单实现。其应用之一在于我们可以用状态空间更小的KM代替M进行模型检测。该方法可自然地推广到基于其它类型函子的余代数结构。
第二部分，我们研究了定理证明方法Deduction Modulo。将DeductionModulo中理论(theory)子句范式化，提高了Deduction Modulo的搜索证明的效率。在Deduction Modulo中一个理论是一个重写系统，重写系统将一个命题重写成一个任意形式的命题，在证明搜索的过程中，这些命题需要动态地转换成子句。当重写系统是一个子句范式化的重写系统时，可以避免这些耗时的动态转化。我们提供了一种子句范式化的方法，将任意一个重写系统转化成与其等价的子句范式重写系统，从而避免了这些动态转化，提高了证明搜索的效率。
第三部分，我们提出了一种新的形式化验证方法，将模型检测和定理证明两种方法的优势结合起来，自动化地验证无穷状态系统是否满足某一性质。对每一个下推系统（可能包含无穷多个格局），我们建立了一个可判定的验证方法:带模型参数的CTL相继式演算(CTL-like sequent calculus parameterized withM，简称SCTL(M))。并证明了对带有一层模态词的CTL公式，SCTL(M)是可靠完备的。对于带有一层模态词的CTL公式，其可证性是可判定的。为了证明其可判定性，我们引入“合一”(merge)的技术，根据合一的技术，我们可以将一个无穷的证明搜索空间局部化成一个余归纳定义的性质。对于余归纳定义的性质，例如EG性质，我们须用余归纳证明原则证明系统是否满足这些性质。此外，我们将CTL和Kripke结构公理化成Resolution Modulo中的重写系统(rewritesystem)Rctl，并且证明SCTL(M)和Resolution ModuloRctl的等价性。