<p>As mentioned in the comments, the translation is shown in:
Volker Diekert and Paul Gastin. &quot;First-order definable languages.&quot; (2008)
<a href="http://www.lsv.fr/Publis/PAPERS/PDF/DG-WT08.pdf" rel="nofollow noreferrer">http://www.lsv.fr/Publis/PAPERS/PDF/DG-WT08.pdf</a></p>
<p>And it goes via a characterization of <span class="math-container">$LTL$</span> as <span class="math-container">$FO[&lt;]$</span>.</p>

CC BY-SA 4.0
2021-05-29T20:07:40.737Z
This paper seems fantastic! Thank you!
Nicola Gigante
CC BY-SA 4.0
2021-05-29T18:51:30.620Z
2021-06-01T06:30:50.067Z
2021-06-01T06:30:50.067Z
Shaull
<p>Sorry to provide the same answer as for <a href="https://cstheory.stackexchange.com/q/49014">this question</a>,
but this was proved in [1, Theorem 3.1].</p>
<p>[1] J. Cohen, D. Perrin and J.-É. Pin, <a href="https://www.sciencedirect.com/science/article/pii/002200009390005H" rel="nofollow noreferrer">On the expressive power of temporal logic for finite words</a>, <em>J. Comput. System Sci.</em> <strong>46</strong> (1993), 271-294.</p>

CC BY-SA 4.0
2021-06-05T20:57:10.987Z
2021-06-05T20:57:10.987Z
J.-E. Pin
<p>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.</p>
<p>Is there any reference that shows such a translation?</p>
<p>[1] Wolfgang Thomas, Safety- and Liveness-properties in Propositional Temporal Logic: Characterisation and Decidability, Mathematical Problems in Computation Theory, Volume 21, 1988</p>

CC BY-SA 4.0
2021-05-29T15:13:40.517Z
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.
Bartosz Bednarczyk
<reference-request><automata-theory><linear-temporal-logic>
Translation of Counter-free automata into Linear Temporal Logic
Nicola Gigante
# Translation of Counter-free automata into Linear Temporal Logic

(Asked by: username_0 on 2021-05-29)

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

**Tags:** reference-request, automata-theory, linear-temporal-logic

> **Comments:**
> **username_1**: 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.  

---

## 2 answers

### Answer by username_2 on 2021-05-29. Score: 5 | Accepted answer

As mentioned in the comments, the translation is shown in:
Volker Diekert and Paul Gastin. "First-order definable languages." (2008)
<http://www.lsv.fr/Publis/PAPERS/PDF/DG-WT08.pdf>

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

> **Comments:**
> **username_0**: This paper seems fantastic! Thank you!  

---

### Answer by username_3 on 2021-06-05. Score: 4

Sorry to provide the same answer as for [this question](https://cstheory.stackexchange.com/q/49014),
but this was proved in [1, Theorem 3.1].

[1] J. Cohen, D. Perrin and J.-É. Pin, [On the expressive power of temporal logic for finite words](https://www.sciencedirect.com/science/article/pii/002200009390005H), *J. Comput. System Sci.* **46** (1993), 271-294.


---

