An Efficient Normalisation Procedure for Linear Temporal Logic

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a normal form for
formulas of LTL with past operators, which Manna and Pnueli then used as
the basis of their famous classification of temporal formulas. Some years
later, Chang, Manna, and Pnueli built on this result to derive a similar normal
form for the future fragment of LTL. Both normalisation procedures had a
non-elementary worst-case blow-up, and followed an involved path from LTL formulas to
counter-free automata to star-free regular expressions and back to LTL.

We improve on both points. We present a purely syntactic normalisation
procedure from LTL to LTL, with single exponential blow-up, that can be
implemented in a few dozen lines of Standard ML code. As an application, we derive a simple
algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the
formula, translates it into a special very weak alternating automaton,
and applies a simple determinisation procedure, valid only for these
special automata.