Definitions
Definition 1: Let $S$ be a set of words. We say that $S$ is nicely infinite prefix-free (made up name for the purpose of this answer) if there are words $u_0,\dots,u_n,\dots $ and $v_1,\dots,v_n,\dots $ such that:
For each $n\ge 1$, $u_n$ and $v_n$ are non-empty and start with distinct letters;
$S=\{u_0v_1,\dots,u_0\dots u_n v_{n+1},\dots\}$.
The intuition is that you can put all those words on an infinite rooted tree (the ■ is the root, the ▲ are the leaves, and the • are the remaining interior nodes) of the following shape such that the words in $S$ are exactly the labels of paths from the root to a leaf:
u₀ u₁ u₂
■-----•-----•-----•⋅⋅⋅
| | |
| v₁ | v₂ | v₃
| | |
▲ ▲ ▲
Proposition 1.1: A nicely infinite prefix-free set is prefix-free.
Proof of proposition 1.1: Suppose that $u_0\dots u_n v_{n+1}$ is a strict prefix of $u_0 \dots u_m v_{m+1}$. There are two cases:
If $n < m$ then $v_{n+1}$ is a prefix of $u_{n+1}\dots u_m v_{m+1}$. This is impossible because $u_{n+1}$ and $v_{n+1}$ have distinct first letters.
If $n > m$ then $u_{m+1}\dots u_n v_{n+1}$ is a prefix of $v_{m+1}$. This is impossible because $u_{m+1}$ and $v_{m+1}$ have distinct first letters.
Proposition 1.2: A nicely infinite prefix-free set is infinite.
Proof of proposition 1.2: In proof 1.1, we showed that if $n\not= m$ then $u_0\dots u_n v_{n+1}$ and $u_0 \dots u_m v_{m+1}$ are not comparable for the prefix order. They are therefore not equal.
Main proof
Proposition 2: Any infinite prefix-free set contains a nice infinite prefix-free set.
Proposition 3: A language contains an infinite prefix-free set if and only if it contains a nicely infinite prefix-free set.
Proof below.
Proof of proposition 3: $\boxed{\Rightarrow}$ by proposition 2. $\boxed{\Leftarrow}$ by propositions 1.1 and 1.2.
Proposition 4: The set of nicely-prefix-free subsets of a regular language (encoded as an infinite word $\overline{u_0}\widehat{v_1}\overline{u_1}\widehat{v_2}\overline{u_2}\dots$) is $\omega$-regular (and the size of the Büchi automaton recognizing it is polynomial in the size of the NFA recognizing the regular language).
Proof below.
Theorem 5: Deciding if a regular language described by a NFA contains an infinite prefix-free subset can be done in time polynomial in the size of the NFA.
Proof of theorem 5: By proposition 3, it is sufficient to test if it contains a nicely-infinite prefix-free subset, which can be done in polynomial time by building the Büchi automaton given by proposition 4 and testing the non-emptyness of its language (which can be done in time linear in the size of the Büchi automaton).
Proof of proposition 2
Lemma 2.1: If $S$ is a prefix-free set, then so is $w^{-1}S$ (for any word $w$).
Proof 2.1: By definition.
Lemma 2.2: Let $S$ be an infinite set of words. Let $w:=\operatorname{lcp}(S_n)$ be the longest prefix common to all words in $S$. $S$ and $w^{-1}S$ have the same cardinal.
Proof 2.2: Define $f:w^{-1}S\to S$ by $f(x)=wx$. It is well defined by definition of $w^{-1}S$, injective by definition of $f$ and surjective by definition of $w$.
Proof of proposition 2: We build $u_n$ and $v_n$ by induction on $n$, with the induction hypothesis $H_n$ composed of the following parts:
$(P_1)$ For all $k\in\{1,\dots,n\}$, $u_0\dots u_{k-1} v_k \in S$;
$(P_2)$ For all $k\in\{1,\dots,n\}$, $u_k$ and $v_k$ are non-empty and start with distinct letters;
$(P_3)$ $S_n:=(u_0\dots u_n)^{-1}S$ is infinite;
$(P_4)$ There is no non-empty prefix common to all words in $S_n$. In other words: There is no letter $a$ such that $S_n\subseteq a\Sigma^*$.
Remark 2.3: If we have sequences that verify $H_n$ without $(P_4)$, we can modify $u_n$ to make them to also satisfy $(P_4)$. Indeed, it suffices to replace $u_n$ by $u_n\operatorname{lcp}(S_n)$. $(P_1)$ is unaffected. $(P_2)$ is trivial. $(P_4)$ is by construction. $(P_3)$ is by lemma 3.
We now build the sequences by induction on $n$:
Initialization: $H_0$ is true by taking $u_0:=\operatorname{lcp}(S)$ (i.e. by taking $u_0:=\varepsilon$ and applying remark 3.1).
Induction step: Suppose that we have words $u_1,\dots,u_n$ and $v_1,\dots,v_n$ such that $H_n$ for some $n$. We will build $u_{n+1}$ and $v_{n+1}$ such that $H_{n+1}$.
Since $S_n$ is infinite and prefix-free (by lemma 1), it does not contain $\varepsilon$ so that $S_n=\underset{a\in \Sigma}{\bigsqcup}(S_n\cap a\Sigma^*)$. Since $S_n$ is infinite, there is a letter $a$ such that $S_n\cap a\Sigma^*$ is infinite. By $(P_4)$, there is a letter $b$ distinct from $a$ such that $S_n\cap b\Sigma^*$ is non-empty. Pick $v_{n+1}\in S_n\cap b\Sigma^*$. Taking $u_{n+1}$ to be $a$ would satisfy $(P_1)$, $(P_2)$ and $(P_3)$ so we apply remark 3.1 to get $(P_4)$: $u_{n+1}:=a\operatorname{lcp}(a^{-1}S_n)$.
$(P_1)$ $u_1\dots u_nv_{n+1}\in u_1\dots u_n(S_n\cap b\Sigma^*)\subseteq S$.
$(P_2)$ By definition of $u_{n+1}$ and $v_{n+1}$.
$(P_3)$ $a^{-1}S_n$ is infinite by definition of $a$, and $S_{n+1}$ is therefore infinite by lemma 3.
$(P_4)$ By definition of $u_{n+1}$.
Proof of proposition 4
Proof of proposition 4: Let $A=(Q,\to,\Delta,q_0,F)$ be a NFA.
The idea is the following: we read $u_0$, remember where we are, read $v_1$, backtrack to where we were after reading $u_0$, read $u_1$, remember where we are, ... We also remember the first letter that was read in each $v_n$ to ensure that $u_n$ starts with another letter.
I've been told that this could be easier with multi-head automata but I'm not really familiar with the formalism so I'll just describe it using a Büchi automaton (with only one head).
We set $\Sigma':=\overline{\Sigma}\sqcup\widehat{\Sigma}$, where the overlined symbols will be used to describes the $u_k$s and the symbols with hats for the $v_k$s.
We set $Q':=Q\times (\{\bot\}\sqcup (Q \times \Sigma))$, where:
$(q,\bot)$ means that you are reading some $u_n$;
$(q,(p,a))$ means that you finished reading some $u_n$ in the state $p$, that you are now reading $v_{n+1}$ that starts with an $a$, and that once you are done, you will go back to $p$ to read a $u_{n+1}$ that does not start with $a$.
We set $q_0':=(q_0,\bot)$ because we start by reading $u_0$.
We define $F'$ as $F\times Q \times \Sigma$.
The set of transitions $\to'$ is defined as follows:
"$u_n$" For each transition $q\overset{a}{\to}q'$, add $(q,\bot)\overset{\overline{a}}{\to'}(q',\bot)$;
"$u_n$ to $v_{n+1}$" For each transition $q\overset{a}{\to}q'$, add $(q,\bot)\overset{\widehat{a}}{\to'}(q',(q,a))$;
"$v_n$" For each transition $q\overset{a}{\to}q'$, add $(q,(p,a))\overset{\widehat{a}}{\to'}(q',(p,a))$;
"$v_n$ to $u_n$" For each transition $p\overset{a}{\to}p'$ where $p$ is final and letter $b$ distinct from $a$, add $(q,(p,b))\overset{\overline{a}}{\to'}(p',\bot)$;
Lemma 4.1: $\overline{u_0}\widehat{v_1}\overline{u_1}\widehat{v_2}\dots \overline{u_n}\widehat{v_{n+1}}$ is accepted by $A'$ iff for each $n\ge 1$, $u_n$ and $v_n$ are non-empty and start with distinct letters, and for each $n\ge 0$, $u_0\dots u_n v_{n+1}\in L(A)$.
Proof of lemma 4.1: Left to the reader.
