How to generate a Buchi Automaton from a LTL formula?

Question

How can I generate a Buchi Automaton starting from an LTL formula?

e.g.

[] (a <-> ! b)

That is,

At all times in the future

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

Answer 1

One option is to use 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)

---

Example: generate a Buchi Automaton from the next LTL formula:

[](a <-> ! b)

This reads: it is always true that a if and only if !b (and viceversa). That is, this is the formula you want to encode.

The following command generates the never claim associated with the LTL formula, and also the Buchi Automaton (option -g).

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

---

More examples are available here.