10
$\begingroup$

Linear temporal logic and deterministic Büchi automata are incomparable: DBA cannot express $FGa$, and LTL cannot express "at least each odd letter is 'a'". But sometimes it is interesting to know whether the language of a DBA can be expressed in LTL.

I need an algorithm that decides whether a language of a given DBA is describable in LTL. Do you know algorithms for that?

Improve this question
$\endgroup$
8
  • $\begingroup$ We conjecture that the other direction is decidable (convert formula to NBA, apply power-set construction, check equivalence) but have had no idea about the one you want so far. $\endgroup$
    – Raphael ♦
    Mar 5, 2012 at 17:15
  • $\begingroup$ I am not sure if it's possible at all, but I'd like to note that by Buchi automata people usually mean NBA (which is more expressive than DBA). NBA is also strictly more expressive than LTL. $\endgroup$
    – Daniil
    Apr 8, 2012 at 10:35
  • $\begingroup$ @Daniil from you reference (First Order Definable languages): "We also show that aperiodicity (i.e., first-order definability (LTL difinability)) of a regular ∞-language can be decided in polynomial space".nice ref! $\endgroup$
    – Ayrat
    Apr 9, 2012 at 19:29
  • $\begingroup$ @Ayrat, thanks, it's indeed a good introduction, I was very happy when I found it. There is also a whole book on infinite words. Unfortunately, I haven't got around to reading it yet. $\endgroup$
    – Daniil
    Apr 10, 2012 at 15:11
  • 1
    $\begingroup$ Equivalence of Büchi automata and linear $\mu$-calculus might provide some interesting insights. $\endgroup$
    – Gilles 'SO- stop being evil'
    Jul 14, 2012 at 13:08

1 Answer 1

Reset to default
5
$\begingroup$

You may find the algorithm in Diekert and Gastin's paper, Section 12. It works for both NBW and DBW (provided that you have the $\omega$-expression), and this can be decided in polynomial time.

Improve this answer
$\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.