2
$\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

$\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$ May 29 at 15:13
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[<]$.

$\endgroup$
1
  • 1
    $\begingroup$ This paper seems fantastic! Thank you! $\endgroup$
    – gigabytes
    May 29 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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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