随着软硬件系统的日益复杂,保证系统的安全性至关重要。模型检测是自动验证系统正确性的有效技术,目前已经广泛应用于计算机软硬件系统,通信协议,安全协议等方面的分析与验证中。针对包含非确定性信息、不完备信息的并发系统的形式化验证问题,本文研究了两种定量模型检测算法。(1)基于可能性理论,模糊逻辑等理论,研究了基于广义可能性决策过程的μ-演算模型检测算法。首先引入广义可能性决策过程作为系统模型,接着对经典的命题μ-演算进行改进和扩展,给出广义可能性μ-演算的概念,用于描述非确定系统的属性特征。然后提出广义可能性μ-演算模型检测算法,并将模型检测问题简化为模糊矩阵运算,最后通过具体的实例进行了分析与验证。与经典的μ-演算相比,广义可能性μ-演算具有更强的表达力,能够刻画不确定系统的属性特征,模型检测算法能够给出系统满足属性的可能性程度,研究成果扩大了广义可能性测度在模型检测中的应用范围。(2)在格理论,多值逻辑的基础上,研究了基于多值Kripke结构的多值μ-演算模型检测算法,将多值Kripke结构作为系统模型,对经典μ-演算语言进行扩展,用于描述多值系统的属性,提出了多值μ-演算模型检测算法,最后给出具体的实例进行了分析与验证。研究成果为非确定系统的模型检测问题提供一种新的思路与方法。