3

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

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

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

4

2 回答 2

4

查看 NuSMV 用户手册中关于 LTL 模型检查的章节。它附带了一个如何在模块中表达和检查 LTL 规范的示例:

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

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

于 2016-01-21T20:56:17.153 回答
0

一种方法是使用 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)。

于 2017-07-28T06:24:17.070 回答