如何从LTL公式开始生成布奇自动机？

Question

如何从LTL公式开始生成布奇自动机？

如

[] (a <-> ! b)

就是说

今后任何时候

• 如果 a 属实 b 是假的
• 如果 b 属实 a 是假的

Answer 1

一种选择是使用 gltl2ba，它的基础是 ltl2ba.

LTL 配方

一个LTL公式可能包含命题符号、布尔运算符、时间运算符和括号。

• 命题符号。

  true, false
  any lowercase string
  

• 布尔运算符

  !   (negation)
  ->  (implication)
  <-> (equivalence)
  &&  (and)
  ||  (or)
  

• 时间运算符：

   G   (always) (Spin syntax : [])
   F   (eventually) (Spin syntax : <>)
   U   (until)
   R   (realease) (Spin syntax : V)
   X   (next)
  

在任何符号之间使用空格。

(来源 ltl2ba网页)

---

例子。 从下一个LTL公式中生成一个Buchi自动机。

[](a <-> ! b)

这个公式是： 这句话的意思是： a 如果且仅如果 !b (反之亦然). 也就是说，这就是你要编码的公式。

下面的命令会生成与LTL公式相关联的never claim，也会生成Buchi Automaton(选项--------)。-g).

~$ ./gltl2ba -f "[](a <-> ! b)" -g
never { /* [](a <-> ! b) */
accept_init:
    if
    :: (!b && a) || (b && !a) -> goto accept_init
    fi;
}

---

更多的例子 此处.