如何从 LTL 公式生成 Buchi 自动机？

Question

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

例如

[] (a <-> ! b)

即

At all times in the future

• if a is true b is false
• if b is true a is false

Answer 1

一种选择是使用 gltl2ba, which is based on ltl2ba。

LTL Formulas

An LTL formula may contain propositional symbols, boolean operators, temporal operators, and parentheses.

• Propositonal Symbols:

  true, false
  any lowercase string
  

• Boolean operators:

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

• Temporal operators:

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

Use spaces between any symbols.

(source: ltl2ba webpage)

---

示例： 从下一个 LTL 公式生成 Buchi 自动机：

[](a <-> ! b)

内容如下：当且仅当 !b（反之亦然） 时，a 始终为真。也就是说，这是你要编码的公式。

以下命令生成与 LTL 公式以及 Buchi Automaton（选项 -g）关联的 never claim。

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

---

有更多示例可用 here。