### ?

## On complexity of propositional linear-time temporal logic with finitely many variables

It is known 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. In the present paper, we show that the same result can be obtained by modifying the original proof of PSPACE-hardness for LTL; i.e., we show how to modify the construction to model the computations of polynomially-space bound Turing machines using only formulas of one variable. We believe that our alternative proof gives additional insight into the semantic and computational properties of LTL.