不确定型多值Kripke结构的模型检测
多值模型检测是经典模型检测的一种扩展,主要用于具有不一致信息的系统的验证.为了对具有不一致和不确定性的系统进行形式化分析,本文提出非确定型多值Kripke结构作为此类系统的模型,引入一种多值计算树逻辑作为非确定型多值Kripke结构的规范语言,给出一种多项式时间的模型检测算法.研究结果表明本文提出的模型检测技术适用于具有不确定行为的多值系统的自动验证.
多值模型检验、计算树逻辑、模糊自动机、De Morgan代数
30
O141;O159(数理逻辑、数学基础)
国家自然科学基金;国家自然科学基金;中国博士后科学基金
2017-03-31(万方平台首次上网日期,不代表论文的发表时间)
60-70