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

Question

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

Answer 1

Spin 生成与LTL 公式 匹配的Buchi Automaton 等效的Promela 代码，并将其封装起来进入一个 never 块。

来自docs：

NAME 从不 - 声明临时声明。

语法从不{序列}

DESCRIPTION 永不声明可用于定义系统行为： 无论出于何种原因，都特别感兴趣。它是最常用的 指定不应该发生的行为。索赔定义为 一系列关于系统状态的命题或布尔表达式 这必须在为行为指定的顺序中变为真 兴趣匹配。

因此，如果您想查看与给定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。

---

查看您的 您的 cmets 和 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 自动机 是 empty [n.b.: by empty 我的意思是它没有接受执行]。在这种情况下，代码 never { false; } 是 empty Buchi Automaton 的规范形式，没有任何接受执行。

---

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