模型检测是一种形式化的验证技术,它以数学理论为基础,自动化的确保整个被验证系统的正确性和可靠性。但是经典的模型检测在建模检测中有两方面的限制。其一,经典的模型检测是基于布尔逻辑展开的,它对于包含不确定和模糊信息的系统的验证无能为力。其二,状态空间可能非常大,甚至有些系统有无限多个状态。当状态数按照指数的形式增加到一定的程度时,状态空间爆炸将会是一个不可避免的问题。为了解决上述两方面的限制,一些模糊测度下的模型检测技术应运而生,如多值模型检测、模糊模型检测和可能性模型检测。但是当前这些技术还处于起步阶段,一些问题尚未得到根本的解决。因此,本文的主要目的是解决模糊测度下模型检测问题,主要包括建模、抽象、等价、最小化及算法生成。本文主要工作概括如下:1.状态属性和转移的多值不确定性使得状态空间爆炸的问题在多值模型检测中更加明显。为了解决多值状态空间爆炸的问题,给出了多值抽象、多值等价和多值最小化三种方法。作为多值抽象的方法,提出了多值模拟的概念,并在此基础上提出了多值抽象函数和多值抽象Kripke结构的概念,证明了多值模拟满足自反性和传递性,给出了多值Kripke结构中路径和迹满足多值模拟的条件;作为多值等价的方法,提出了多值互模拟的概念,证明了多值互模拟满足自反性,对称性和传递性,给出了多值Kripke结构中路径和迹满足多值互模拟的条件,验证了多值互模拟严格的优于多值模拟等价;作为多值最小化的方法,给出了多值商的构造,并通过一个急救决策的实例,说明多值商在多值模型状态简化中的作用。其次,为了解决多值商的实现过于数学化不易于计算机识别,特别的采用了多值计数器和多值集合划分的方法,设计了一类多值商算法,并通过示例演示了整个算法的过程。通过对比分析,所提出的多值商算法比传统商算法更易于计算机程序识别和理解,且更一般化。2.现有的抽象、等价和最小化方法都是限定在具体给定的模型中,无法在多个模型之间共用。为了实现抽象、等价和最小化的广义化,首先对不确定型模糊Kripke结构(NFKSs)进行了标准化变形,其次分别给出了不确定型模糊抽象、等价和最小化三种方法。作为不确定型模糊抽象的方法,提出了不确定型模糊模拟(NF模拟)和不确定型模糊粗模拟(CNF模拟)的概念,给出了 NF模拟适用于不同模型的满足条件,并在此基础上提出了模糊抽象函数、粗模糊抽象函数、抽象的NFKSs结构和粗抽象的NFKSs结构的概念,证明了 NF模拟和CNF模拟满足自反性和传递性,给出了NFKSs的路径在相同的策略下满足NF模拟和CNF模拟的条件,以及NFKSs的迹满足NF模拟和CNF模拟的条件;作为不确定型模糊等价的方法,提出了不确定型模糊互模拟(NF互模拟)的概念,给出了 NF互模拟适用于不同模型的满足条件,证明了 NF互模拟满足自反性,对称性和传递性,给出了 NFKSs的路径在相同的策略下满足NF互模拟的条件,以及NFKSs的迹满足NF互模拟的条件。作为不确定型模糊最小化的方法,给出了不确定型模糊商(NF商)的构造,通过一个试验性用药的实例,说明NF商是如何最简化NFKSs和精炼NFKSs中策略。最后,给出了改进的NF商算法,并通过实例演示了整个算法的过程。结果表明,这种改进的NF商算法更具一般化,适用于Kripke结构,多值Kripke结构,模糊Kripke结构和NFKSs。3.在一些可能性系统中,状态转移存在着损耗和奖励,如能量的损耗和获取。为了解决这一类系统的建模问题,给出了广义可能性奖励Kripke结构(GPR Kripke结构)和累计奖励的定义。根据累计奖励仅仅是代数和而不是析取运算,得知广义GPR Kripke结构并不完全与广义可能性Kripke(GP Kripke)结构性质相同,并在此基础上特别的给出广义可能期望奖励内可达的定义,以及广义可能性奖励计算树的语构定义和语义定义。其次,为了解决GPRKripke结构的抽象、等价和最小化问题,给出了广义可能性奖励模拟(GPR模拟)、广义可能性奖励互模拟(GPR互模拟)和广义可能性奖励商(GPR商)的定义,证明了 GPR模拟满足自反性和传递性,GPR互模拟满足自反性,对称性和传递性,证明了如果两个GPRKripke结构满足GPR模拟和GPR互模拟,那么其路径和迹一定满足GPR模拟和GPR互模拟,并且通过一个自动驾驶求路的实例说明广义可能性如何处理实时交通信息,GPR商如何最优化求路结果。最后给出GPR商的生成算法。