logic - 使用 SPIN 进行 LTL 模型检查

Question

我在看 SPIN 软件。我想用它来寻找 LTL 理论的模型。所有的手册和教程都在讨论验证算法的属性，但我对此一点也不感兴趣。我只是想找到 LTL 公式的模型（我想是相应的 Büchi 自动机），就像 mace4 或悖论模型检查器可以找到 FOL 公式的模型一样。我相信 SPIN 应该能够做到这一点，但我无法在文档中找到如何做到这一点。有人可以指出任何有用的资源吗？

Answer 1

为了从LTL公式生成 Buchi 自动机，您可以使用ltl2ba工具。该工具可以提供Buchi 自动机或其Promela代码版本的图形表示，如下例所示：

~$ ./ltl2ba -f "([] q0) && (<> ! q0)"
never {    /* ([] q0) && (<> ! q0) */
T0_init:
    false;
}

---

您也可以使用Spin生成 Buchi Automaton 的Promela版本，使用以下命令：

~$ spin -f "LTL_FORMULA"

例如：

~$ spin -f "[] (q1 -> ! q0)" 
never  {    /* [] (q1 -> ! q0) */
accept_init:
T0_init:
    do
    :: (((! ((q0))) || (! ((q1))))) -> goto T0_init
    od;
}

然而，与ltl2ba 相比，Spin在生成源代码时似乎并未简化 Buchi Automaton，因此有时难以解释其输出；例如，尝试运行spin -f "([] q0) && (<> ! q0)"并将输出自动机与使用ltl2ba获得的自动机进行比较。

---

编辑

您现在可以使用gltl2ba替代ltl2ba的网站，例如：

~$ gltl2ba.py -f "([] p0) || (<> p1)" -g

never { /* ([] p0) || (<> p1) */
T0_init:
    if
    :: (1) -> goto T0_S1
    :: (p1) -> goto accept_all
    :: (p0) -> goto accept_S2
    fi;
T0_S1:
    if
    :: (1) -> goto T0_S1
    :: (p1) -> goto accept_all
    fi;
accept_S2:
    if
    :: (p0) -> goto accept_S2
    fi;
accept_all:
    skip
}

生成以下图表：