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

Abstract

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 ${\bigwedge }_{i=1}^n\mathbf{GF}{\phi }_i\vee \mathbf{FG}{\psi }_i$, where ${\phi }_i$ and ${\psi }_i$ 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.

This is the extended version of the referenced conference paper and contains an appendix with additional material

References in corpus (1)

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

Cited by in corpus (1)

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