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

<ul>
<li><code>L</code> is LTL-definable (i.e., there exists an LTL formula <code>phi</code> such that <code>L</code> is the set of all words satisfying <code>phi</code>)</li>
<li><code>L</code> is FO[&lt;, Succ]-definable</li>
<li><code>L</code> is star-free</li>
</ul>

<p>However, I am looking for a simple (sufficient) condition on the <strong>structure of a DFA</strong>, let us call it <code>A</code>, that guarantees that the language <code>L(A)</code> accepted by <code>A</code> is indeed LTL-definable. I am aware that <code>L(A)</code> is LTL-definable if and only if the syntactic monoid of <code>A</code> is group-free, but this monoid is too large to compute in many cases.</p>

<p>Is there a "simpler", preferably structural property on DFAs/NFAs that guarantees that the accepted language is expressible by an LTL formula?</p>

CC BY-SA 3.0
2017-05-05T23:39:49.067Z
Deciding whether a DFA recognizes an aperiodic language is PSPACE-complete (see http://www.sciencedirect.com/science/article/pii/030439759190075D). So I doubt that there is an affirmative answer to your question: any structural property you may find would be PSPACE-complete to decide.
Boson
CC BY-SA 3.0
2017-05-06T14:09:06.777Z
https://en.wikipedia.org/wiki/Aperiodic_finite_state_automaton
Sylvain
<dfa><linear-temporal-logic><nfa>
Structural property of DFAs/NFAs accepting LTL-definable languages
Dan
# Structural property of DFAs/NFAs accepting LTL-definable languages

(Asked by: username_0 on 2017-05-05)

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?

**Tags:** dfa, linear-temporal-logic, nfa

> **Comments:**
> **username_1**: Deciding whether a DFA recognizes an aperiodic language is PSPACE-complete (see http://www.sciencedirect.com/science/article/pii/030439759190075D). So I doubt that there is an affirmative answer to your question: any structural property you may find would be PSPACE-complete to decide.  
> **username_2**: https://en.wikipedia.org/wiki/Aperiodic_finite_state_automaton  

---

## 0 answers

