model-checkingpromelaspinautomatonformal-methods

How to generate a Buchi Automaton from a LTL formula?

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
Solution

  • 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;
}

    enter image description here

    More examples are available here.