MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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???


share|cite|improve this question
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 or Straubing…. – Benjamin Steinberg May 15 '12 at 13:04
up vote 3 down vote accepted

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

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.

share|cite|improve this answer
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

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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