ALL_{REGEX} in PSPACE algorithm
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)$).