In a seminal paper from 1985, Sistla and Clarke showed that satisfiability
for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete,
depending on the set of temporal operators used. If, in contrast, the set
of propositional operators is restricted, the complexity may decrease.
This paper undertakes a systematic study of satisfiability for LTL
formulae over restricted sets of propositional and temporal operators.
Since every propositional operator corresponds to a Boolean function,
there exist infinitely many propositional operators. In order to
systematically cover all possible sets of them, we use Post?s lattice.
With its help, we determine the computational complexity of LTL
satisfiability for all combinations of temporal operators and all but two
classes of propositional functions. Each of these infinitely many problems
is shown to be either PSPACE-complete, NP-complete, or in P.