  In the mid 80s, Lichtenstein, Pnueli, and Zuck showed that every formula of
Past LTL (the extension of Linear Temporal Logic with past operators) is
equivalent to a conjunction of formulas of the form $\mathbf{G}\mathbf{F}
\varphi \vee \mathbf{F}\mathbf{G} \psi$, where $\varphi$ and $\psi$ contain
only past operators. Some years later, Chang, Manna, and Pnueli derived a
similar normal form for LTL. Both normalization procedures have a
non-elementary worst-case blow-up, and follow an involved path from formulas to
counter-free automata to star-free regular expressions and back to formulas. In
2020, Sickert and Esparza presented a direct and purely syntactic normalization
procedure for LTL yielding a normal form similar to the one by Chang, Manna,
and Pnueli, with a single exponential blow-up, and applied it to the problem of
constructing a succinct deterministic $\omega$-automaton for a given formula.
However, their procedure had exponential time complexity in the best case. In
particular, it does not perform better for formulas that are almost in normal
form. In this paper we present an alternative normalization procedure based on
a simple set of rewrite rules.
