# An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata

arXiv: https://arxiv.org/abs/2005.00472 · HTML: https://mlsanity.com/paper/2005.00472/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 May 2020.

## Built on by (most cited first, 3 of 3)

- [Good-for-MDP State Reduction for Stochastic LTL Planning](https://mlsanity.com/paper/2511.09073/) (2025)
- [Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions](https://mlsanity.com/paper/2602.06746/) (2026)
- [SemML 2.0: Synthesizing Controllers for LTL](https://mlsanity.com/paper/2604.24102/) (2026)

## Abstract (arXiv)

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form bigwedgei=1n GF varphii vee FG psii, where varphii and psii contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation 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. We improve on both points. We present a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. 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.