Email Gateway (Aug 23 2022 at 09:06): Email Gateway (Aug 23 2022 at 09:06):From: Manuel Eberl <eberlm@in.tum.de>
I'm happy to present some more cutting-edge research formalised in
Isabelle by Salomon Sickert, now in the AFP:
An Efficient Normalisation Procedure for Linear Temporal Logic:
Isabelle/HOL Formalisation
by Salomon Sickert
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 ⋀_{i=1..n}
GF φi ∨ FG ψ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 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.
https://www.isa-afp.org/entries/LTL_Normal_Form.html
Enjoy,
Manuel
Last updated: Apr 20 2024 at 16:18 UTC