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?