随着计算机软件系统、硬件系统的发展,系统也变得越来越复杂,因此设法保证系统的正确性和可靠性变得越来越重要。为此,许多学者投入到该问题的研究中,并提出了很多理论与方法,模型检测因高度自动化而引起了学者的关注。模型检测是一种形式化验证技术。其过程就是通过对系统建立模型,然后验证该模型是否满足给定的性质。在模型检测常用的逻辑中,命题μ-演算吸引了很多学者的兴趣,它是由Kozen提出的,是个表达能力很强的逻辑语言,其较强的表达能力主要来自于最大不动点算子和最小不动点算子的交替嵌套。由于命题μ-演算有着较强的表达能力,因此其它一些逻辑验证都可以转换为命题μ-演算来验证,而且验证效率也较高。模型检测需要对系统状态空间进行穷举搜索,验证并发系统时,其状态数是呈指数增长的。目前已经有许多关于命题μ-演算的模型检测算法,这些算法可以分为全局模型检测算法和局部模型检测算法。对于命题μ-演算,目前已知的最好的局部模型检测算法的时间复杂度与交替嵌套深度d呈指数关系,其复杂度较高,本文将对其不动点交替嵌套迭代过程进行分析,提出时间复杂度较低的局部模型检测算法。本文从命题μ-演算出发,研究不动点交替嵌套迭代的中间结果之间的偏序关系,设计高效的局部模型检测算法,并对算法的复杂度进行研究分析。本文主要分为三个部分:第一部分主要分析基于命题μ-演算的局部模型检测算法,对其不动点交替嵌套迭代过程进行分析,然后从三支决策的角度改进算法。第二部分主要分析不动点交替嵌套迭代过程的中间结果之间的一组偏序关系,并根据该关系设计了一个局部模型检测算法。第三部分主要开发设计了模型检测器MuFPAL-MC的词法语法分析器模块,并阐述了模型检测器MuFPAL-MC的研究框架。