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

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.