如何在 Promela - SPIN 中将 LTL 转换为 Automato？

Question

如何在 PROMELA 中将 LTL 转换为自动机？我知道使用命令 SPIN -f "ltl x" 可以将 LTL 转换为永不声明，但我想要 LTL 的自动机而不是否定自动机。如果我在生成 never claim 之前否定 LTL，这是正确的。谁能帮我？

Answer 1

Spin 生成与 Buchi Automaton 等效的 Promela 代码，它与 LTL 公式，并将其包含在 never 块中。

来自docs：

NAME never - declaration of a temporal claim.

SYNTAX never { sequence }

DESCRIPTION A never claim can be used to define system behavior that, for whatever reason, is of special interest. It is most commonly used to specify behavior that should never happen. The claim is defined as a series of propositions, or boolean expressions, on the system state that must become true in the sequence specified for the behavior of interest to be matched.

因此，如果您想查看与给定 LTL 公式匹配的代码，您只需键入：

~$ spin -f "LTL_FORMULA"

例如：

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

获取相同代码的另一种方法，加上 Buchi Automaton 的图形表示，是 follow this link。

查看你的评论和你的this other问题，你似乎想检查两个LTL公式 p与g相互矛盾，即是否一定是模型满足 p 必然违反 g 反之亦然。

这可以理论上使用spin完成。然而，这个工具并没有简化 Buchi Automaton 的代码，因此很难处理它的输出。

我建议您改为下载 LTL2BA（位于以下 link）。要设置它，您只需要解压 tar.gz 文件并在控制台中输入 make。

让我们看一个用法示例：

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

由于[] q0和<> ! q0相互矛盾，返回的Buchi自动机为空[n.b.: by empty 我的意思是它没有接受执行]。在这种情况下，代码 never { false; } 是 empty Buchi Automaton 的 canonical form，没有任何接受执行。

免责声明： 将输出与 never { false } 进行比较，以确定 Buchi Automaton 是否为空，如果 simplification 步骤无法转换所有 empty[=80=，则可能导致 spurious 结果] 规范形式的自动机。

如何在 Promela - SPIN 中将 LTL 转换为 Automato？

How to transform LTL into Automato in Promela - SPIN?

model-checking

spin

promela