3
$\begingroup$

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

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$
    – Bartosz Bednarczyk
    Commented May 29, 2021 at 15:13

2 Answers 2

Reset to default
5
$\begingroup$

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[<]$.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ This paper seems fantastic! Thank you! $\endgroup$
    – Nicola Gigante
    Commented May 29, 2021 at 20:07
4
$\begingroup$

Sorry to provide the same answer as for this question, 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, J. Comput. System Sci. 46 (1993), 271-294.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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