  We introduce and investigate a number of fragments of propo- sitional
temporal logic LTL over the flow of time (Z, <). The fragments are defined in
terms of the available temporal operators and the structure of the clausal
normal form of the temporal formulas. We determine the computational complexity
of the satisfiability problem for each of the fragments, which ranges from
NLogSpace to PTime, NP and PSpace.

Logic in Computer Science;Computational Complexity