# Büchi automaton to Linear Temporal Logic

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.

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.