Apparently, model checking LTL on Kripke structures is PSPACE-complete (see this question). Usually, when something in finite model theory is PSPACE-hard, there is a simple proof using the APTIME incarnation of PSPACE and alternation in the logic. Or there is a reduction from QBF (the evaluation problem for quantified boolean formulae).
In the case of LTL, I have difficulty to see any connection to alternation. In fact, the reduction in the paper cited in the linked question can make do with a single G operator and otherwise boolean connectives and (lots of) X operators. This makes sense, as it reduces from deterministic Turing machines (it uses the PSPACE incarnation of PSPACE), not alternating ones. Yet it implies that already a fragment of LTL which does not have any apparent alternation at all incurs the same complexity.
My question is: Is there some intuition linking LTL and alternation? In particular some intuition that still holds for fragments like above which, syntactically, do not appear to allow alternation.
