Membership testing in transformation monoids "Given a finite set $A$, a set of functions $S=\left\{f_{1}, f_{2}, \ldots, f_{k}\right\}$, each $A \to A$, and a candidate function $g:A \to A$, is $g$ in the monoid generated by $S$ with respect to composition?"

Kozen's paper "Lower bounds for natural proof systems" shows that this problem is PSPACE-complete. The following question is about his argument that the problem is in PSPACE.

He argues that it is easy to compute function composition if we represent the functions as bipartite graphs. Now we just guess a sequence of $f_{i}$s, compose them, and check whether it equals $g$. Thus, it can be done in nondeterministic linear space, and by Savitch's theorem, the problem is in PSPACE.

But is this really sufficient to see that the problem is in nondeterministic linear space? The representation of $g$ using terms from $S$ might itself be exponentially long. The paper concedes this just before definition 3.2.2, and is an otherwise interesting little fact about permutations (which are a special case of the system being considered) -- the order of a permutation over $n$ elements may be exponentially large in $n$ (See this).
The nondeterministic polynomial-space algorithm for this problem works as follows:


Initialize h: A→A to the identity mapping.
Is h=g?  If so, we found out that g is in the monoid generated by S; accept and halt.
Guess one element f∈S.
Update h to f∘h.
Go to step 2.


As you correctly pointed out, the sequence can be exponentially long in the input size, so this algorithm may take exponential time before accepting.

Note that the algorithm does not guess a whole sequence at once and store this sequence in the work space—doing so would require exponential space.