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.


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
    Oct 2 '19 at 5:22
  • 1
    $\begingroup$ @kafka There is an answer for that case on mathoverflow: mathoverflow.net/questions/96963/… $\endgroup$
    – DCTLib
    Oct 2 '19 at 6:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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