Does a given regular language contain an infinite prefix-free subset? A set of words over a finite alphabet is prefix-free if there are no two distinct words where one is a prefix of the other.

The question is: 

What is the complexity of checking whether a regular language given as an NFA contains an infinite prefix-free subset?

Answer (due to Mikhail Rudoy, here below): It can be done in polynomial time, and I think in even in NL. 

Paraphrasing Mikhail's answer, let $(\Sigma,q_0,F,\delta)$ be the input NFA in the normal form (no epsilon transitions, trim), and let $L[p,r]$ (resp. $L[p,R]$) be the language obtained by having state $p$ as initial state and $\{r\}$ as final state (resp. state $p$ as inital and the set $R$ as final). For a word $u$ let $u^\omega$ be the infinite word obtained by iterating $u$.

The following are equivalent:


The language $L[q_0,F]$ contains an infinite prefix-free subset.
$\exists q \in Q$, $\exists u \in L[q,q]\smallsetminus\{\varepsilon\}$ $\exists v \in L[q,F]$ so that $v$ is not a prefix of $u^\omega$.
$\exists q \in Q$ $L[q,q] \neq \{\varepsilon\}$ $\forall u \in L[q,q]$ $\exists v \in L[q,F]$ so that $v$ is not a prefix of $u^\omega$.


Proof:

3$\Rightarrow$2 trivial.

For 2$\Rightarrow$1, it suffices to see that for any $w \in L[q_0,q]$ we have that $w (u^{|v|})^* v$ is an infinite prefix-free subset of $L[q_0,F]$.

Finally, 1$\Rightarrow$3 is the "correctness" proof in Mikhail's answer.
Your problem can be solved in polynomial time.

To begin, convert the given NFA to an equivalent NFA with the following additional properties:


There are no epsilon transitions
All states are reachable from the start state


Helpful subroutine

Suppose we have an NFA $N$, a state $q$, and a nonempty string $s$. The following subroutine will let us evaluate the truth value of the following statement: "every path in $N$ from state $q$ to an accept state corresponds to a string that is a prefix of string $s^n$ for some $n$." Furthermore, this subroutine will run in polynomial time.

First, construct the NFA $S$ with $|s| + 1$ states which accepts all strings that are not prefixes of $s^n$ for any $n$ ($|s|$ non-accept states in a loop to keep track of where in the "pattern" of $sssss\ldots$ we are so far, and one accept state for if we have already deviated from that pattern). Next, construct the NFA $N'$ which is exactly like $N$ but has $q$ as its start state. Finally, construct a final NFA $N''$ whose language $L(N'')$ is $L(S) \cap L(N')$ using the standard NFA intersection construction. Note that all of these constructions are polynomial in the size of the input.

Then simply test whether the language of $N''$ is empty (which can be done in polynomial time with a simple graph search). $L(N'') = \emptyset$ if and only if $L(S) \cap L(N') = \emptyset$, or in other words every string in $L(N')$ is not in $L(S)$. In other words, the language of $N''$ is empty if and only if $N'$ accepts only strings that are prefixes of $s^n$ for some $n$. This can be rephrased as exactly the statement we were trying to evaluate: "every path in $N$ from state $q$ to an accept state corresponds to a string that is a prefix of string $s^n$ for some $n$."

Main algorithm

Consider the set of states in the NFA that are in some loop. For each such state, $q$, do the following:

Let $P_2$ be any simple loop containing $q$. Let $s$ be the string corresponding to loop $P_2$. Since the NFA has no epsilon transitions, $s$ is not empty. Then apply the subroutine to the NFA, state $q$, and string $s$. If the subroutine tells us that every path starting at $q$ in the NFA and ending at an accept state corresponds to a prefix of $s^n$ for some $n$ then continue to the next state $q$. Otherwise, output that the given NFA's language contains an infinite prefex-free subset. 

If we try every state $q$ that is in a loop and the algorithm never outputs, then output that the given NFA's language does not contain an infinite prefex-free subset.

Correctness (first half)

First, suppose that the above algorithm asserts that the given NFA's language contains an infinite prefex-free subset. Let's say that this output was selected while considering some loop $P_2$ and some state $q$. As before, $s$ is the string corresponding to $P_2$. Then we know according to the subroutine that not every path starting at $q$ in the NFA and ending at an accept state corresponds to a prefix of $s^n$ for some $n$ (as this is the only output of the subroutine that would lead to the main algorithm outputting at that $q$).

Let $P_3$ be a path whose existence is asserted by the subroutine: a path from $q$ to an accept state such that the corresponding string $t$ is not a prefix of $s^n$ for any $n$. 

Let $P_2'$ consist of $m$ copies of $P_2$ where $m$ is sufficiently large that $m|s| &gt; |t|$. Since $P_2$ is a loop through $q$, $P_2'$ can be treated as a path from $q$ to $q$. The string corresponding to $P_2'$ is $s^m$

Let $P_1$ be a path from the start state to $q$ (which exists since every state is reachable from the start) and let $r$ be the string corresponding to this path.

Then the path consisting of $P_1$, $x$ copies of $P_2'$, and $P_3$ is an accepting computation path. The string corresponding to this path is $r(s^m)^xt$. Thus, the NFA accepts every string of the form $r(s^m)^xt$. This is an infinite set of strings accepted by the NFA, and I claim that this set of strings is prefix-free. In particular, suppose $r(s^m)^xt$ is a prefix of $r(s^m)^yt$ with $y &gt; x$. In other words, $t$ is a prefix of $(s^m)^{y-x}t$. Since $(s^m)^{y-x}$ has length $m(y-x)|s| \ge m|s| &gt; |t|$, this implies that $t$ is a prefix of $(s^m)^{y-x} = s^{m(y-x)}$. But we know by the output of the subroutine that $t$ is not a prefix of $s^n$ for any $n$. Thus, $r(s^m)^xt$ cannot be a prefix of $r(s^m)^yt$, and as desired the set of strings is prefix-free. 

Thus, I have shown that if the main algorithm outputs that the given NFA's language contains an infinite prefex-free subset then this is in fact the case.

Correctness (second half)

Next, I will show the other half: if the given NFA's language contains an infinite prefex-free subset then the main algorithm will output this fact.

Suppose the given NFA's language contains an infinite prefix-free subset. Let $A$ be the set of (accepting) computation paths corresponding to these strings. Notice that $A$ is an infinite set of accepting computation paths whose corresponding strings are never prefixes of each other.

Say that a state is "looping" in the NFA if there exists a loop in the NFA through that state and "non-looping" otherwise. Consider all paths from the start state to any looping state which pass through only non-looping states (except for the one looping state where they end up). Let $P$ be the set of these paths. Each path $p \in P$ cannot have a loop as then the states in that loop would be looping states and so $p$ would pass through a looping state. Thus, the lengths of paths in $P$ are bounded above by the number of states in the NFA and so $P$ is finite (for example, if the start state is a looping state then the only such path is the empty path). 

We can partition $A$ into $|P|+1$ subsets based on how that computation paths in $A$ starts. In particular, for $p \in P$, let $A_p$ be the set of all computation paths in $A$ that start with path $p$ and let $B$ be the set of all other paths in $A$. Clearly, all $A_p$s and $B$ are disjoint and their union is the entire set $A$. Furthermore, $B$ contains only paths that never pass through a looping state, and therefore never loop; thus $B$ is finite. We can conclude then that some $A_p$ must be infinite (otherwise $A$ would be a union of finitely many finite sets).

Since $A_p$ is infinite, there are infinitely many computation paths, none of whose strings are prefixes of each other, that are accepting paths starting with $p$. Let $q$ be the state reached at the end of path $p$. We can conclude that there are infinitely many accepting paths, call this set $A'$, starting at $q$ all of which correspond to strings that are not prefixes of each other. 

During the main algorithm, we run the subroutine on state $q$ and some string $s$. This subroutine tells us whether every accepting path starting at $q$ corresponds to a string that is a prefix of $s^n$ for some $n$. If this were the case, then all the infinitely many accepting paths in $A'$ would be prefixes of $s^n$ for various $n$, which would imply that they are all prefixes of each other. This is not the case, so we conclude that when the main algorithm runs the subroutine on state $q$, the result is the other possible outcome. This, however, leads the main algorithm to output that the NFA's language contains an infinite prefix-free subset.

This concludes the proof of correctness.