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

Question

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

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

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

Answer 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 检查规范是否适用于所有可能的路径。要检查您的公式是否存在模型（即路径），您可以输入否定，如果存在，模型检查器将为您提供 counter-example。 counter-example 将作为原始公式的示例。

Answer 2

一种方法是使用 PolSAT。这将 LTL 公式作为输入，并将其提供给许多不同的 LTL 求解器。这通常比单独使用 NuSMV 更快。如果您用 /bin/false 和运行 ./polsat 'Gp & F X ~ p' 替换 NuSMV 二进制文件，它将中止并留下一个文件 ../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 has a bit of difficulty on modern machines, you may need to downgrade bison to version 2.7 (See e.g. https://askubuntu.com/questions/444982/install-bison-2-7-in-ubuntu-14-04) 下载。

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

How to check LTL satisfiability using NuSMV?

logic

model-checking

nusmv