The complexity of propositional linear temporal logics. (English) Zbl 0632.68034

Sistla, A. P.; Clarke, E. M.

J. Assoc. Comput. Mach. 32, 733-749 (1985).

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.

MSC:

68Q65	Abstract data types; algebraic specification
03B70	Logic in computer science
68Q60	Specification and verification (program logics, model checking, etc.)

Keywords:

branching time temporal logic; decision procedures; complexity; satisfiability; determination of truth; propositional linear temporal logics; NP-complete; PSPACE-complete