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

Question

Как я могу сгенерировать автомат Buchi, исходя из формулы 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 )

---

Пример: создать автомат Buchi из следующей формулы LTL:

[](a <-> ! b)

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

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

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

---

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