model-checking - 如何解释 NuXMV 的 msat LTL 命令的结果

Question

我正在使用 NuXMV 在相当大的模型上使用 msat_check_ltlspec_bmc 命令检查 LTL 属性。结果显示在给定范围内没有找到反例。我是否将其解释为该属性为 True。或者它也可能意味着分析不完整。

这是因为，通过改变属性命题为真或假，结果总是没有反例。大多数结果是违反直觉的。

从基于实变量的属性开始，但由于无法理解结果，使用相同的命令转移到同一模型上基于布尔的属性。

Answer 1

有界模型检查是一种面向错误的技术，它检查执行跟踪上的属性的有效性，直到给定长度k。

• 当执行跟踪违反属性时，很好：发现了一个错误。

• 否则，（在一般情况下）模型检查结果没有提供有用的信息，应该这样对待。

在某些情况下，了解有关模型的其他信息会有所帮助。特别是，如果知道长度的每个执行轨迹都k必须循环回其中一个k-1状态，那么就有可能从缺少长度小于或等于的反例中得出更有力的结论k。