Как сгенерировать автомат Бучи из формулы LTL?

Один из вариантов — использовать 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:

[](a <-> ! b)

Это звучит так: всегда верно, что a тогда и только тогда, когда !b (и наоборот). То есть это формула, которую вы хотите закодировать.

Следующая команда генерирует требование «никогда», связанное с формулой LTL, а также с автоматом Бучи (опция -g).

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

Другие примеры доступны здесь.