I consider LTL on finite words. In this context, there are a couple of nice equivalence results for a language L:

  • L is LTL-definable (i.e., there exists an LTL formula phi such that L is the set of all words satisfying phi)
  • L is FO[<, Succ]-definable
  • L is star-free

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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.