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.