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

## TL;DR

This paper demonstrates that the satisfiability and model-checking problems for propositional LTL with a single variable are PSPACE-complete, providing an alternative proof that offers deeper insight into LTL's properties.

## Contribution

It presents a modified proof of PSPACE-completeness for LTL with one variable, enhancing understanding of its semantic and computational aspects.

## Key findings

- PSPACE-completeness holds for LTL with one variable
- Modified proof offers new insights into LTL complexity
- Results align with those for multiple 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.