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

Model checking for nondeterministic multi-valued Kripke structures

作　　者：郦丽[1] 沈应兄[1] 潘海玉[1,2] 

机构地区：[1]泰州学院计算机科学与技术学院,江苏泰州225300 [2]陕西师范大学计算机科学学院,陕西西安710062

出　　处：《模糊系统与数学》2016年第5期60-70,共11页Fuzzy Systems and Mathematics

基　　金：国家自然科学基金(11301321;11401361);中国博士后科学基金资助项目(2014M552408)

摘　　要：多值模型检测是经典模型检测的一种扩展,主要用于具有不一致信息的系统的验证。为了对具有不一致和不确定性的系统进行形式化分析,本文提出非确定型多值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.

关 键 词：多值模型检验 计算树逻辑 模糊自动机 DE MORGAN代数 

分 类 号：O141[理学—数学] O159[理学—基础数学]