Why is LTL Model Checking in PSPACE
It is correct that writing the Buchi automaton to memory takes exponential space.....which is why you don't do that.

The construction for the Buchi automaton is however very regular and can be done in a forward manner. This allows you to construct it on-the-fly while you search for an accepting lasso in the product between the Buchi automaton and $T$.

In this way, you can find an accepting lasso in NPSPACE (it is exists): you build a Turing machine that builds the product on-the-fly, searches for a lasso by non-deterministically guessing which transition in the product to take, and non-determinstically guesses the lasso knot to store (which, w.l.o.g., could also be the required accepting state). If it finds a path to such a knot and then a path from the knot back to the knot, you know that there is a word in the product.

To make this algorithm always terminate, you also have a counter to keep track of the number of transitions observed so far. If it exceeds two times the size of the product, then the algorithm aborts with a "no" answer. Such a counter also only needs space polynomial in the size of the LTL formula.

Since PSPACE=NPSPACE, it follows that you only need polynomial space for such a Turing machine.