1
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ 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/…. $\endgroup$ May 15, 2012 at 13:04

2 Answers 2

3
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ You were faster in finding the link to the survey. I made the mistake of looking on Diekert's page. $\endgroup$ May 15, 2012 at 12:39
1
$\begingroup$

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

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