The complexity of propositional linear temporal logics

Abstract

The complexity of satisfiability and determination of truth in a particular finite structure are considered for different propositional linear temporal logics. It is shown that these problems are NP-complete for the logic with F and are PSPACE-complete for the logics with F, X, with U, with U, S, X operators and for the extended logic with regular operators given by Wolper.