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
As mentioned in the comments, the translation is shown in:
Diekert, Volker, and Paul Gastin. &quot;First-order definable languages.&quot; (2008)
http://www.lsv.fr/Publis/PAPERS/PDF/DG-WT08.pdf
And it goes via a characterization of $LTL$ as $FO[&lt;]$.