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.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.