Regular Linear Temporal Logic with Past
Past operators are easily introduced in \RLTL via a single
previous-step operator for basic state formulas. The satisfiability
and model checking problems for \RLTL are PSPACE-complete, which is
optimal for extensions of \LTL. This result is shown using a novel
linear size translation of \RLTL expressions into $2$-way
alternating parity automata on words.
Unlike previous automata-theoretic approaches to \LTL, this
construction is compositional (bottom-up). As alternating parity
automata can easily be complemented, the treatment of negation is
simple and does not require an upfront transformation of formulas
into any normal form.