# An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation

 Title: An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation Author: Salomon Sickert (s /dot/ sickert /at/ tum /dot/ de) Submission date: 2020-05-08 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. BibTeX: @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{http://isa-afp.org/entries/LTL_Normal_Form.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: LTL, LTL_Master_Theorem