| Summary: | 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.
|
|---|