# Translate a buchi automaton to LTL

How can I translate a Büchi automaton A to LTL(linear temporal logic) if $L(A)$ is definable in the LTL?

MY idea is : Büchi automaton $A$ ===> QPTL ===> LTL

I know that given any Buchi automaton, we can translate it to QPTL(Quantified Propositional Temporal Logic), formally speaking, For every B¨uchi automaton A over $Σ=2^{AP}$, there exists a QPTL formula $ϕ$ such that $models(ϕ)=L(A)$, and we can decide in PSPACE whether the accepted language $L⊆Σ^∞$ of a given B¨uchi automaton $A$ is aperiodic. It's well known that $L$ is aperiodic iff L is definable in the LTL, so we can use this algorithm to check whether $L(A)$ is definable in the LTL.

but how can I translate QPTL to LTL???

thanks!!

-
This question had a vote to close as too localized that I feel is inappropriate. The theory of Buchi automata is equivalent to the second order monadic theory of the natural numbers with a successor function. LTL is equivalent to the first order theory of the natural numbers with less than. Consult the nice book of Perrin and Pin liafa.jussieu.fr/~jep/Resumes/InfiniteWords.html or Straubing books.google.com/books/about/…. – Benjamin Steinberg May 15 '12 at 13:04

You can always go through the $\omega$-semigroup. It might not be the most straightforward algorithm, but at least it should work.

You can find details in http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf

The principle is to translate your automaton into an $\omega$-semigroup, via the transition matrices for instance. Then you can minimize this $\omega$-semigroup. If $L(A)$ is LTL-definable this should give you an aperiodic semigroup. You can then apply the proof that aperiodic implies LTL-definable, in order to get an LTL formula for your language.

-
You were faster in finding the link to the survey. I made the mistake of looking on Diekert's page. – Benjamin Steinberg May 15 '12 at 12:39

Look at the survey article:

First-order definable languages

Volker Diekert, Paul Gastin

In: Logic and Automata: History and Perspective (Eds. J. Flum and E. Grädel and Th. Wilke) Amsterdam University Press, Texts in Logic and Games (2008) 261--306 pdf File

-