
In the mid 1980s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of Linear Temporal Logic (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 φ i and ψ 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.
Weak alternating automata, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Normal form, deterministic automata, Temporal logic, Linear temporal logic, Formal languages and automata, 1102.03 Lógica Formal, linear temporal logic, Automata and formal grammars in connection with logical questions, Deterministic automata, Logic in Computer Science (cs.LO), 1102.15 Teoría de Lenguajes Formales, normal form, Lógica simbólica y matemática (Matemáticas), F.4.1, weak alternating automata
Weak alternating automata, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Normal form, deterministic automata, Temporal logic, Linear temporal logic, Formal languages and automata, 1102.03 Lógica Formal, linear temporal logic, Automata and formal grammars in connection with logical questions, Deterministic automata, Logic in Computer Science (cs.LO), 1102.15 Teoría de Lenguajes Formales, normal form, Lógica simbólica y matemática (Matemáticas), F.4.1, weak alternating automata
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
