不确定型多值Kripke结构的模型检测

Model checking for nondeterministic multi-valued Kripke structures

多值模型检测是经典模型检测的一种扩展,主要用于具有不一致信息的系统的验证。为了对具有不一致和不确定性的系统进行形式化分析,本文提出非确定型多值Kripke结构作为此类系统的模型,引入一种多值计算树逻辑作为非确定型多值Kripke结构的规范语言,给出一种多项式时间的模型检测算法。研究结果表明本文提出的模型检测技术适用于具有不确定行为的多值系统的自动验证。

Multi-valued model checking is an extension of the classical model checking to verify the properties of systems with uncertain information. To verify the properties of systems with both uncertain information and nondeterministic behavior, we introduce nondeterministic multi-valued Kripke structures（NMKSs）to allow nondeterministic choices among the possibilities of transitions. To formulate the properties of NMKSs,we present the syntax and semantics of multi-valued computation tree logic（MCTL）. We give a model checking algorithm for MCTL over NMKSs,and show that the algorithm has polynomial-time complexity in the size of the system. The techniques developed here are applicable to the automatic verification of multi-valued systems with nondeterministic behaviours.