中文摘要：

状态爆炸是模型检验需解决的一个关键问题．基于GPVW算法，以及从LTL公式导出识别该公式的Bachi自动机，用OBDD符号表示，通过符号操作求解自动机乘积．采用符号方法求解出含有初始状态或接受状态的最大连通图，判断自动机是否存在初始状态能否到达含有接收状态的最大连通分支，从而判定所接受的语言是否非空来模型检验LTL公式．采用本文所提出模型检验LTL公式的方法，能在一定程度上解决空间爆炸问题．

英文摘要：

State ＂explosion＂ is a key problem to deal with by using model checking. By using GPVW algorithm and LTL formula, the Büchi automata was derived, which could identify the foregoing formula and was denoted by means of OBDD symbol. The solution of automata product was conducted with symbolic manipulation. Then a maximal connection graph which included initial state or accepted state was solved with symbolic approach, and it was judged whether there was the initial state with the automat as well as whether the automata could reach the maximal connected branching which included the accepted state, so that it could be decided whether the language accepted was an empty LTL formula of model checking.