论文研究基于吴方法的符号模型检验.pdf

模型检验技术广泛应用于验证并发系统的性质。它的瓶颈一直是内存爆炸问题，将BDD技术引入到模型检验中的方法能有效地缓和状态组合爆炸问题。然而，随着系统规模的增大，BDD的大小仍呈指数增长。吴方法是一种处理多项式的符号计算方法，能有效地求解代数方程组并成功地应用于几何定理机器证明。给出应用吴方法计算表示Kripke结构和CTL公式的多项式的特征列的方法，从而实现对较大规模的系统性质的验证，进一步缓和状态组合爆炸问题。