### 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 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 an executable formalisation of 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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages
- Logic/General logic/Temporal logic

### Session LTL_Normal_Form

- Normal_Form
- Normal_Form_Complexity
- Normal_Form_Code_Export

### Depends on

- Linear Temporal Logic
- A Compositional and Unified Translation of LTL into ω-Automata

## Cite

×

LTL_Normal_Form-AFP

    @article{LTL_Normal_Form-AFP,
      author  = {Salomon Sickert},
      title   = {An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/LTL_Normal_Form.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- May 9, 2020 : Isabelle2020