On complexity of propositional Linear-time Temporal Logic with finitely many variables

Abstract

It is known [DemriSchnoebelen02] that both satisfiability and model-checking problems for propositional Linear-time Temporal Logic, LTL, with only a single propositional variable in the language are PSPACE-complete, which coincides with the complexity of these problems for LTL with an arbitrary number of propositional variables [SislaClarke85]. In the present paper, we show that the same result can be obtained by modifying the original proof of SPACE-hardness for LTL from [SislaClarke85]; i.e., we show how to modify the construction from [SislaClarke85] to model the computations of polynomially-space bound Turing machines using only formulas of one variable. We believe that our alternative proof of the results from [DemriSchnoebelen02] gives additional insight into the semantic and computational properties of LTL.

References in corpus (3)

• Complexity and expressivity of propositional dynamic logics with finitely many variables
• Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
• Complexity of finite-variable fragments of propositional modal logics of symmetric frames