一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

发布时间：2019-09-18 06:16

【摘要】：多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。
【图文】：

状态,三值逻辑,模型检测,经典逻辑

Ｆｉｇｕｒｅ１Ｐｒｏｃｅｓｓｏｆｓｔａｔｅｍｅｒｇｉｎｇ图１状态合并过程运而生。本文提出一种基于三值逻辑的模型检测方法，可作为多值模型检测基矗在现有的多值逻辑模型检测方法中，一种方法是将多值逻辑转化为经典逻辑进行处理，如ＣｈｅｃｈｉｋＭ［２～５］和ＢｏｌｃＬ［６］等将已有三值问题分解成若干经典逻辑问题进行处理；而另一种方法是基于三值逻辑本身完成模型检测，如ＬｉＹｏｎｇ－ｍｉｎｇ等［７，８］通过人为设置状态不确定性的可接受度，采用模糊模型检测计算出系统满足性质的可接受度。而郭建等［９］通过算法在模型检测过程中对公式为真和未知的情况作出检查，再由此推断出公式为假的情况，这样可以及早发现未知公式，了解哪些状态需要信息细化，以便检验未知公式的真值，但其算法中并未涉及状态信息的细化，无法检测未知公式的真值，三值模型检测算法不完整。本文提出了一种三值逻辑模型检测过程，并给出三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比，该算法降低了算法的复杂度，完善了对于不确定或者不一致信息的处理，从而增强了三值逻辑模型检测的可应用性。２三值逻辑模型三值逻辑模型可以在经典逻辑模型的基础上，通过对经典逻辑模型中部分状态进行合并或抽取得到，从而减少系统状态数量，以避免系统检测中出现状态爆炸。值得注意的是，在状态迁移过程中状态变量的数量是不变的，所以当相邻的一个或多个状态进行合并时，只需考虑状态变量值存在不一致性的情况，即状态变量具有多个不同的值，记此类变量的值为Ｍ，生成三值逻辑模型。例如，图１（１）中，由于存在搜索路径［Ｓ０Ｓ２］ｗ、路径［Ｓ０Ｓ１］

过程图,三值逻辑,模型验证,过程

Ｋｌｅｅｎｅ最强三值逻辑命题；（３）三值系统模型要与原系统模型相一致。如图１（２）所示，若状态Ｓ０与Ｓ１合并，则只有Ａ不确定；若Ｓ０与Ｓ２合并，则存在Ａ、Ｂ两个不确定变量，所以应将Ｓ０与Ｓ１合并，其搜索路径为［（Ｓ０，１）ｗＳ２］ｗ，较图１（１）明显减少。三值模型检验是针对带有不确定和不一致信息的系统而建立起来的一套形式验证理论，是经典模型检验的扩展。下面给出了一种三值逻辑模型检测的基本过程，如图２所示。Ｆｉｇｕｒｅ２Ｐｒｏｃｅｓｓｏｆ３－ｖａｌｕｅｄｍｏｄｅｌｃｈｅｃｋｉｎｇｖａｌｉｄａｔｉｏｎ图２三值逻辑模型验证过程①经典逻辑模型抽象为三值逻辑模型；②在系统模型中，除要检测的状态变量外，其他变量都设置为Ｍ（因不同的待验证系统性质与不同的系统变量相关，，而系统模型却与所有系统变量相关，这样做的目的是为减少验证过程中不必要的计算），利用多值模型检测器检测状态是否满足系统所需的性质Ｐ；若模型检测器返回Ｔ或Ｆ，检测结束；③如果检测器返回Ｍ，返回原三值逻辑模型，增加信息，重新设置变量，再进行检测；④三值逻辑模型的所有确定信息都被检测后，检测器仍返回Ｍ，则返回到经典逻辑模型；⑤多值模型检测器对经典模型进行验证，验证未知性质的真值，检测结束。３三值逻辑模型检测实现模型检测是在描述系统的状态迁移系统Ｋ上验证时序逻辑公式ｐ描述的系统性质是否可满足的一个过程。经典模型检测使用Ｋｒｉｐｋｅ结构来对系统建模，而三值模型检验通常使用不完全Ｋｒｉｐ－ｋｅ结构对系统建模。本文对原有
【作者单位】：陕西师范大学计算机科学学院;
【基金】：国家自然科学基金资助项目(61003061;11271237)
【分类号】：TP306

【参考文献】