RECORD
Efficient Normalization of Linear Temporal Logic
Logic in Computer Science · Submitted 19 Oct 2023
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim 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.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
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.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | 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. | background 1.00 | 0.02 | 0.03 | asserted 1.00 |
| s1 | Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. | background 1.00 | 0.03 | 0.02 | asserted 1.00 |
| s2 | 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. | background 0.84 | 0.08 | 0.04 | asserted 1.00 |
| s3 | We improve on both points. | contribution 0.89 | 0.70 | 0.19 | asserted 0.96 |
| s4 | 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. | contribution 0.96 | 0.97 | 0.85 | asserted 1.00 |
| s5 | As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. | contribution 0.85 | 0.95 | 0.12 | asserted 1.00 |
| s6 | 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. | method 0.98 | 0.90 | 0.09 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v2
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original 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.
Human review
How the literature uses it
Papers whose main result relates to this one's
States the same result 1 paper
-
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.
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata · 1.00
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.