如何使用 NuSMV 检查 LTL 可满足性？答案

【问题标题】：How to check LTL satisfiability using NuSMV?如何使用 NuSMV 检查 LTL 可满足性？
【发布时间】：2016-01-21 15:30:40
【问题描述】：

我正在尝试使用 NuSMV 作为 LTL 公式的可满足性检查器，即我想知道给定公式是否存在模型。我知道 NuSMV 也可以用于此目的，既因为它在理论上是可能的，也因为我看到它在许多处理可满足性的论文中被引用（其中一篇还声称 NuSMV 是最快的可满足性检查器之一那里）。

我看到 NuSMV 附带了一个名为 ltl2smv 的工具，它显然将 LTL 公式转换为 SMV 模块，但是我不知道如何使用输出。将它直接提供给 NuSMV 会返回一条关于“主”未定义的错误消息，所以我想我必须定义一个主模块并以某种方式使用另一个。由于我从未将 NuSMV 用作模型检查器，因此我不知道它的语言是如何工作的，而且鉴于我只需要这个特定的用例，用户指南是压倒性的，顺便说一句，该指南中的任何地方都没有提到。

那么如何使用 NuSMV 检查 LTL 公式的可满足性？是否有记录此用例的地方？

【问题讨论】：

标签： logic model-checking nusmv

【解决方案1】：

看看chapter about LTL model checking in NuSMV's user manual。它附带了一个如何在模块中表达和检查 LTL 规范的示例：

MODULE main
  VAR
    ...
  ASSIGN
    ...
  LTLSPEC <LTL specification 1>
  LTLSPEC <LTL specification 2>
...

NuSMV 检查规范是否适用于所有可能的路径。要检查您的公式是否存在模型（即路径），您可以输入否定，如果存在，模型检查器将为您提供一个反例。然后，反例将成为您原始公式的示例。

【讨论】：

好的，所以LTL公式被放入LTLSPEC指令中。 ltl2smv 工具与此无关？它的目的是什么？
@gigabytes：好像是供NuSMV内部使用的，见this page。
我明白了....您能否在答案中提供一个最小的工作示例？
我目前没有安装正常工作的 NuSMV。但手册的示例会找到!G (proc1.state = entering -> F proc1.state = critical) 的模型。
是的，与此同时，我已经设法通过您的回答和链接的手册部分使其工作。谢谢你:)

【解决方案2】：

一种方法是使用 PolSAT。这将 LTL 公式作为输入，并将其提供给许多不同的 LTL 求解器。这通常比单独使用 NuSMV 更快。如果您将 NuSMV 二进制文件替换为 /bin/false 并运行 ./polsat 'Gp & F X ~ p'，它将中止并留下一个文件 ../NuSMV/tmpin.smv，其中包含以下内容：

MODULE main
VAR
Gp:boolean;
p:boolean;
LTLSPEC
!(((Gp)&(F (X (!(p))))))

（请注意，PolSAT 将 Gp 解释为单个变量）。然后，您可以使用命令../NuSMV/nusmv/NuSMV < ../NuSMV/tmpin.smv 直接运行 NuSMV。

如果您想安装 PolSAT，目前可以从https://lab301.cn/home/pages/lijianwen/ 下载。 v0.1 在现代机器上有点困难，您可能需要将bison 降级到版本 2.7（参见例如https://askubuntu.com/questions/444982/install-bison-2-7-in-ubuntu-14-04）。

【讨论】：