[isabelle] New in the AFP: An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.