Given a Büchi automaton what is the procedure to build an equivalent LTL formula? And what is its size?

I'm looking for references but I haven't found them so far.


1 Answer 1


Since Büchi automata are strictly more expressive than LTL, such a translation is not possible in the general case.

For instance, the language $L = \{w_0 w_1 w_2 \ldots \in (2^{\{a\}})^\omega \mid \exists^\infty i \in \mathbb{N}. w_{2i} = \{a\} \}$ is representable by a Büchi automaton with 3 states, but is not expressible in LTL as it is a counting language.

  • $\begingroup$ Do you know how to translate a counter-free Buchi automaton in LTL ? I am moslty interested in it. $\endgroup$
    – kafka
    Commented Oct 2, 2019 at 5:22
  • 1
    $\begingroup$ @kafka There is an answer for that case on mathoverflow: mathoverflow.net/questions/96963/… $\endgroup$
    – DCTLib
    Commented Oct 2, 2019 at 6:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.