  We study preprocessing techniques for clause normal forms of LTL formulas.
Applying the mechanism of labelled clauses enables us to reinterpret LTL
satisfiability as a set of purely propositional problems and thus to transfer
simplification ideas from SAT to LTL. We demonstrate this by adapting variable
and clause elimination, a very effective preprocessing technique used by modern
SAT solvers. Our experiments confirm that even in the temporal setting
substantial reductions in formula size and subsequent decrease of solver
runtime can be achieved.
