中文摘要：

命题μ-演算局部模型检测算法中，目前最好的算法的时间复杂度与不动点算子交替嵌套深度d呈指数关系。针对命题μ-演算局部模型检测算法的计算过程进行分析，得到迭代计算的中间迭代值间满足的一组偏序关系，然后利用该偏序关系设计了一个局部模型检测算法，算法时间复杂度的指数部分为d2，大大提高了算法的计算效率。

英文摘要：

In this paper,the computing process of fixpoint alternant iteration of local model checking for propositionalμ-alculus is analyzed and a set of partial order relation about intermediate values of iterative calculation is proven.Then a local model checking algorithm is designed by the partial order relation.At present,the index of time complexity of existing local model checking algorithm is d(d is the alternation depth of the formula).The index of time complexity is reduced from d to d2.The computational efficiency of the algorithm is improved greatly.