题目：多值模型检测器的研究与实现

模型检测是一种重要的对系统行为进行自动化检测的技术。经典的模型检测技术利用布尔逻辑建立系统模型，它要求对系统的所有行为给予确定性的描述。现有的模型检测器大多是基于经典模型检测技术实现的。然而，在许多大型复杂的系统开发过程中经常遇到包含不确定或不一致的信息需要处理，对于此类问题经典的模型检测技术无有效解决方法，现有的被广泛使用的模型检测器，例如NuSMV或者Spin，将不能够应用在这些系统的检测上。

多值逻辑可通过增加额外的真值来显示表示系统中的不确定和不一致信息。所以，多值模型检测作为经典模型检测的一种扩展，可用于检测包含此类信息的系统。随着多值模型检测技术的不断发展，开发实现多值模型检测器成为了迫切的需要。本文介绍了一种新的多值模型检测器MVMC的实现方法。MVMC使用格值表示多值逻辑真值；用多值Kripke结构描述系统模型。MVMC能够检测多值系统模型上的线性性质，包括安全性，不动性，活性，一致性，及对偶一致性等。

与现有的多值逻辑模型检测器xChek相比，本文设计实现的多值模型检测器检测的是LTL描述的系统性质，通过将多值模型转换为类经典模型进行检测，可有效减少检测过程中搜索的系统状态的数量，从而降低了检测过程对物理内存的需求，并提高了检测的效率。最后通过实例,对MVMC进行了测试,说明该检测器是有效的。