Propositional linear temporal logic (PLTL) is the basic logical tool that is utilized for the specification and verification of reactive systems. The main syntactic feature of PLTL is that it uses the temporal operators X (next), U (until), and F (sometimes). Their semantics is defined using linear-time structures. (S,i) denotes the state of the structure at time i and, for example, and for some .

The satisfiability and the model checking problems for PLTL are known to be PSPACE-complete. This paper undertakes the task of analyzing the computational complexity of the restrictions of PLTL that are obtained by limiting (a) the temporal operators (considering only formulas with F, or only with F, X, and so on); (b) the number of propositional variables; and (c) the temporal height (the number of nested temporal connectives). Virtually all fragments of PLTL that can be obtained by combining these restrictions are analyzed. In many important cases, the computational complexity drops from PSPACE-complete to NP-complete, which of course means that the problem is still infeasible.