模型检测是一种形式化的自动验证技术。1981年,由Clarke,Emerson,Quielle和Sifakis提出。它的基本思想是:通过状态空间的穷举搜索来验证有穷状态系统上性质的正确性。它不仅可以自动执行,而且能在系统不满足性质时提供反例。但近些年随着系统复杂性的增加,系统中不确定信息亟待处理,且状态爆炸问题也越来越严峻,现有的模型检测技术已经不能完全适用于复杂系统的验证。因此,对模型检测技术进行扩展是重要的也是必要的。目前,国内外学者在经典的模型检测和概率模型检测领域对符号化模型检测做出了大量的研究,但对于可能性测度下的模型检测却没有相应的符号化研究。本文对可能性测度下符号化模型检测进行了研究,是对可能性测度下的模型检测技术和符号化模型检测技术的扩展,对于复杂系统的模型检测的实现与推广具有一定的意义。本文研究了可能性测度下并发系统的符号化模型检测,并设计了一个可能性测度下的符号模型检测器。一方面处理了复杂系统验证中的不确定信息,另一方面缓解了复杂系统验证中的状态爆炸问题。本文研究内容主要分为以下几点:(1)提出可能性测度下并发系统的符号化模型。当并发系统的状态较多时,符号化模型可以较好的表示系统状态及状态之间的迁移关系,以减少存储空间和提高验证效率。(2)研究了可能性测度下的符号化模型检测算法。将系统模型和状态利用多终端二叉树进行符号化表达,并且利用不动点技术实现了验证算法。(3)基于NuSMV的基础,研究并设计了一个可能性测度下的符号化模型检测器,给出了可能性测度下的模型检测器的实现方案,探讨了该模型检测器的实现方法。研究意义主要有:补充了可能性测度下并发系统的符号化模型检测理论,给出了可能性测度下的模型检测器的实现方案,为可能性测度下并发系统检测的推广奠定了基础。