
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: 
20200508 
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 nonelementary worstcase blowup, and
follow an involved path from formulas to counterfree automata to
starfree 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 blowup. 
BibTeX: 
@article{LTL_Normal_FormAFP,
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://isaafp.org/entries/LTL_Normal_Form.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
LTL, LTL_Master_Theorem 
