Abstract: In this paper, the computing process of fixpoint alternant iteration of local model checking for propositional [μ]-calculus 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.

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

关键词: &mu, -演算, 局部模型检测, 不动点, 偏序关系