HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Algorithm to translate a deterministic Büchi automaton to LTL (when possible)

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
ltlbüchitranslatealgorithmpossibledeterministicwhenautomaton

Problem

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?

Solution

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.

Context

StackExchange Computer Science Q#2739, answer score: 5

Revisions (0)

No revisions yet.