Efficient Normalization of Linear Temporal Logic

TL;DR

This paper introduces a direct, syntactic normalization method for Linear Temporal Logic (LTL) that reduces complexity and facilitates the translation of LTL formulas into deterministic Rabin automata.

Contribution

It presents a novel normalization procedure for LTL with only a single exponential blow-up, improving over previous non-elementary methods, and enables simpler automata translation.

Findings

Normalization exhibits only a single exponential blow-up.

Enables a straightforward translation of LTL into deterministic Rabin automata.

Provides a syntactic, direct approach to LTL normalization.

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{G}\mathbf{F}\, \varphi_i \vee \mathbf{F}\mathbf{G}\, \psi_i $, where $\varphi_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 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. We improve on both points. We present direct and purely syntactic normalization procedures for LTL, yielding a normal form very similar to the one by Chang, Manna, and Pnueli, that exhibit only a single exponential blow-up. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalizes the formula, translates it into a special very weak alternating automaton, and applies a simple determinization procedure, valid only for these special automata.