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

Question

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

Answer 1

Spin生成等同于与LTL 公式匹配的Buchi Automaton的Promela代码，并将其封装成一个never块。

从文档：

NAME 从不 - 声明临时声明。

语法 从不 { 序列 }

描述 从不声明可用于定义系统行为，无论出于何种原因，它都具有特殊意义。它最常用于指定不应该发生的行为。声明被定义为系统状态的一系列命题或布尔表达式，这些命题或布尔表达式必须按照指定的顺序变为真，以匹配感兴趣的行为。

因此，如果您想查看与给定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图形表示的另一种方法是点击此链接。

---

查看您的评论和您的另一个问题，您似乎想检查两个LTL 公式 p和g是否相互矛盾，也就是说，满足 p的模型是否肯定会违反g并且反之亦然反之亦然。

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

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

让我们看一个用法示例：

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

由于[] q0和<> ! q0相互矛盾，返回的Buchi 自动机是空的 [nb：空我的意思是它没有接受执行]。在这种情况下，代码永远不会 { false; }是没有任何接受执行的空Buchi Automaton的规范形式。

---

免责声明：将输出与never { false }进行比较以确定Buchi Automaton是否为空，如果简化步骤无法将所有空自动机转换为规范形式，则可能会导致虚假结果。