2
$\begingroup$

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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.