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

Question

我试图使用NuSMV作为LTL公式的可满足性检查器，也就是说，我想知道是否存在给定公式的模型。我知道NuSMV也可以用于这个目的，这既是因为它在理论上是可能的，也是因为我在许多关于可满足性的论文中引用了它(其中一篇文章还声称NuSMV是世界上最快的可满足性检查器之一)。

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

那么，如何使用NuSMV来检验LTL公式的可满足性呢？有地方记录这个用例吗？

Answer 1

看一看关于NuSMV用户手册中的LTL模型检查一章。它附带了一个示例，说明如何在模块中表示LTL规范并检查：

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

NuSMV检查规范是否符合所有可能的路径。要检查您的公式是否存在模型(即路径)，您可以输入否定，如果存在，模型检查器将给出一个反例。然后，反示例将是原始公式的示例。

Answer 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 < ../NuSMV/tmpin.smv。

如果您想安装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)。