# Translation of Counter-free automata into Linear Temporal Logic

There is a well-known equivalence between counter-free automata and Linear Temporal Logic (which is cited for example by [1]). However, I cannot find a concrete way to obtain an LTL formula from a counter-free automaton.

Is there any reference that shows such a translation?

[1] Wolfgang Thomas, Safety- and Liveness-properties in Propositional Temporal Logic: Characterisation and Decidability, Mathematical Problems in Computation Theory, Volume 21, 1988

• Have you tried to look at translations from counter-free automaton into FO[<]? It is known that LTL = FO[<], so maybe you can find something in this direction. May 29 at 15:13

And it goes via a characterization of $$LTL$$ as $$FO[<]$$.