I consider LTL on finite words. In this context, there are a couple of nice equivalence results for a language
Lis LTL-definable (i.e., there exists an LTL formula
Lis the set of all words satisfying
Lis FO[<, Succ]-definable
However, I am looking for a simple (sufficient) condition on the structure of a DFA, let us call it
A, that guarantees that the language
L(A) accepted by
A is indeed LTL-definable. I am aware that
L(A) is LTL-definable if and only if the syntactic monoid of
A is group-free, but this monoid is too large to compute in many cases.
Is there a "simpler", preferably structural property on DFAs/NFAs that guarantees that the accepted language is expressible by an LTL formula?