Abstract: Model checking is widely used in verifying properties of concurrent systems.Its bottleneck is always the problem of memory explosion，the method adding BDD technology to model checking can effectively alleviate the combination state explosion problem.However，the size of BDDs greatly increases with the system becoming larger and more complex.Wu’s method is an efficient method in symbolic computation，it is efficient to solve algebraic equations，and has succeeded in geometry theorem proving.This paper presents a framework to apply Wu’s method to calculate the characteristic sets of polynomials that represent Kripke structures as well as CTL formulas，and further alleviates the combination state explosion problem.

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