  In the present paper we introduce the notion of strong backdoors into the
field of temporal logic for the CNF-fragment of linear temporal logic
introduced by Fisher. We study the parameterised complexity of the
satisfiability problem parameterised by the size of the backdoor. We
distinguish between backdoor detection and evaluation of backdoors into the
fragments of horn and krom formulas. Here we classify the operator fragments of
globally-operators for past or future, and the combination of both. Detection
is shown to be in FPT whereas the complexity of evaluation behaves different.
We show that for krom formulas the problem is paraNP-complete. For horn
formulas the complexity is shown to be either fixed parameter tractable or
paraNP-complete depending on the considered operator fragment.
