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.

翻译：在20世纪80年代中期，Lichtenstein、Pnueli和Zuck证明了每个含过去算子的线性时序逻辑（Past LTL）公式都等价于形如$\mathbf{G}\mathbf{F} \varphi \vee \mathbf{F}\mathbf{G} \psi$的公式的合取，其中$\varphi$和$\psi$仅包含过去算子。几年后，Chang、Manna和Pnueli推导出LTL的类似规范形式。这两种规范化方法在最坏情况下都导致非初等规模的爆炸，且遵循一条复杂的路径：从公式到无计数器自动机，再到无星自由正则表达式，最后返回公式。2020年，Sickert和Esparza提出了一种直接且纯语法的LTL规范化方法，生成了类似于Chang、Manna和Pnueli的规范形式，其规模增长仅为单指数级，并将其应用于为给定公式构造简洁的确定性$\omega$-自动机的问题。然而，该方法的最佳情况时间复杂度仍为指数级，特别是对于已接近规范形式的公式性能并未提升。本文提出了一种基于简单重写规则集的替代规范化方法。