模型检测(Model Checking)是一种重要的形式化验证方法,广泛用于软硬件系统行为的自动验证.为了使包含非确定性信息、不完全信息和不一致信息的并发系统得到有效验证,在时序逻辑(Temporal Logic)和决策过程(Decision Process,DP)的基础上,本文研究了具有多值决策过程(Multi-valued Decision Process,MvDP)的广义可能性多值时序逻辑模型检测算法,以及在非确定性系统验证中的应用.首先构造了刻画系统模型的MvDP,引入描述系统属性的多值时序逻辑,然后给出基于MvDP的广义可能性多值时序逻辑模型检测算法.该算法利用决策过程中的调度,将模型检测问题转换为多项式时间内的模糊矩阵运算或模糊矩阵不动点计算.得到的多值计算树逻辑(Multi-valued Computation Tree Logic,MvCTL)模型检测算法的时间复杂度为O(size(M)·|Φ|),多值线性时序逻辑(Multi-valued Linear Temporal Logic,MvLTL)和多值分支时序逻辑(Multi-valued Branching Temporal Logic,MvCTL*)模型检测算法的时间复杂度均为O(size(M)·exp(|(φ|).本文的主要工作如下:1.构造MvDP作为有限状态系统的模型.给出MvDP和MvDP上调度的定义,并讨论状态转移、前驱和后继状态、有穷和无穷路径的形式化表示;讨论多值决策过程的初始分布、状态转移分布等相关概念的矩阵表示;给出基于MvDP建模,路径上可能性测度的定义和有穷路径柱集的定义,并给出有穷路径柱集的矩阵表示.2.给出多值时序逻辑的语构和语义.分别给出MvCTL、MvLTL、MvCTL*的语构定义,继而讨论这三种时序逻辑在可能性测度和必然性测度下的语义解释并分别给出语义的归纳定义,讨论了MvLTL的语言语义和路径语义在可能性测度下的等价性.3.给出基于MvDP的广义可能性多值时序逻辑模型检测算法.首先给出算法的问题描述并给出子公式个数的递归定义;然后讨论了“O”,“(?)”,“(?)≤n”等MvCTL时序算子的矩阵计算方法,以及“□”算子,“(?)”算子和“◇”算子的不动点计算方法,并给出基于MvDP的广义可能性MvCTL模型检测算法(GPo-MvCTL算法)并讨论其时间复杂度;接下来,讨论MvLTL的几种特殊可达事件的可能性测度求解,结合MvLTL PNF的语构和语义,给出基于MvDP的广义可能性MvLTL模型检测算法(GPo-MvLTL算法)并讨论其时间复杂度;最后,结合基于MvDP的广义可能性MvLTL和MvCTL模型检测算法,给出基于MvDP的广义可能性MvCTL*模型检测算法(GPo-MvCTL*算法)并讨论其时间复杂度.