ALL_{REGEX} in PSPACE algorithm

$ALL_{REGEX}$ is the computational problem of determining for regular expression x if $L(x) = \Sigma^*$. In a proof for $ALL_{REGEX} \in PSPACE$, the following non-deterministic turing machine $M(R)$ on regular expression $R$ is given

Convert R to an NFA $N = (Q,\Sigma,\delta,S,F)$; $K = S$;

While $K \cap F \neq \emptyset$

1. Non-deterministically guess a character $a \in \Sigma$
2. S' = Compute the new set of states from character $a$ and states $K$
3. K = S'

The proof states that iff $M$ does not halt, then $L(R) = \Sigma^*$. Suppose we have $\Sigma = \{a,b\}$ and R = a*. Why doesn't this machine halt? Won't there be a single path of guesses (namely, a*) that goes on forever, implying the whole machine does as well?

The algorithm goes prove that after $2^{|Q|}$ steps, we know the language must be $\Sigma^*$, so we accept instead of looping. I understand the intuition of the algorithm and how it would be implemented deterministically , but I'm confused as to how the algorithm above works when the NTM formalism accepts if any path accepts and it is making me question my understanding of NTMs.

• @DavidRicherby - see edits – dfb Mar 12 '14 at 17:50

The idea is that if a DFA having $n$ states isn't universal (doesn't accept $\Sigma^*$) then there must be some word of length at most $n$ which it doesn't accept. The proof is similar to the proof of the pumping lemma: take any word not accepted by the DFA, and trace its route through the DFA. You can always shorten it to a word which ends up in the same state, and additionally all states encountered are distinct. Since there are only $n$ distinct states, this finished up the proof.
An NFA having $n$ states is equivalent, via the powerset construction, to a DFA having $2^n$ states. Therefore if it is not universal then it rejects some word of length at most $2^n$. The non-deterministic algorithm you describe guesses such a word and verifies that it is indeed rejected by the NFA. Since NPSPACE=PSPACE, we can convert this into a deterministic algorithm (in fact, one using space $O(n^2)$).