使用 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 生成 Promela 版本的 Buchi Automaton，命令为：

~$ 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
}

生成下图：

使用 SPIN 检查 LTL 模型

LTL model checking with SPIN

logic

formal-verification

model-checking

spin

promela