模型检测是一种很重要的自动验证技术.1981年,由Clarke和Emerson以及Quielle和Sifakis最早提出,它主要通过状态搜索或不动点计算来验证有穷状态并发系统的命题性质.它可以自动执行,并能在系统不满足性质时提供反例.在很多情况下,可以把模型检测和各种归纳原则结合起来验证非有穷状态系统.在经典的模型检测中,Kripke结构是很重要的一种研究模型,线性时序逻辑(LTL)是一种研究线性性质的重要时序逻辑工具.将二者联系起来研究系统满足线性时间性质是非常有必要的.2008年,Baier和Katoen详细研究了基于概率测度下以马尔科夫链为概率系统模型的模型检测方法和相关应用.另一方面,自Zadeh在1965年提出模糊集的理论以来,许多学者致力于模糊集理论及应用方面的研究工作.模糊测度作为模糊集理论的一个分支是经典测度的延拓,它重点研究一种非可加情况,而大多数复杂的实际问题都是非可加的情况.因此有必要研究具有非可加测度的非确定系统的模型检测的理论及应用问题.本文针对一种常见的非可加测度：可能性测度,研究基于可能性测度情形下的模型检测理论.具体来说,我们主要针对可能性测度下的线性性质的模型检测进行研究.论文的主要工作表现在以下方面：1.定义了可能的Kripke结构,分析了可能的Kripke结构在可能性测度下的线性时间属性(LTL)模型检测.并对可能性测度和概率测度的一些性质进行了比较.2.首先给出了有穷的可能的Kripke结构满足可达性、受限可达性的可能性测度的代数表达形式及相应的计算方法,并与马尔科夫链满足线性性质的概率测度进行了比较.其次通过使用有穷自动机将可能的Kripke结构满足可达性等性质推广到了满足正则安全性、ω-正则性等一般的线性时间(LT)性质.进而得出结论：在可能的Kripke结构上的正则安全性、ω-正则性的验证可以转化为乘积可能Kripke结构(可能的Kripke结构和非确定型有穷自动机的乘积)上的可达性和重复可达性的验证问题,并对该方法的应用进行了实例分析.最后对本文的基本内容作了总结,提出将来可以研究的问题.