From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Two new AFP entries revolve around Mission-time LTL (MLTL), a sibling of metric temporal logic.
Mission-time Linear Temporal Logic
by Katherine Kosaian, Zili Wang, and Elizabeth Sloan
We formalize the syntax, semantics, and some useful properties of Mission-time Linear Temporal Logic (MLTL), following the literature. MLTL is a variant of Linear Temporal Logic, which has already been formalized in Isabelle/HOL. In contrast to LTL, MLTL includes finite discrete time bounds on the temporal operators. We do not directly build on the LTL AFP entry, but aim to mirror its style; in particular, we found it useful when defining our syntactic sugar binding precedences. Another closely related AFP entry is the formalization of MFOTL.
https://www.isa-afp.org/entries/Mission_Time_LTL.html
Mission-time Linear Temporal Logic to Regular Expressions
by Zili Wang and Katherine Kosaian
We formalize the WEST algorithm for translating from Mission-time Linear Temporal Logic Formulas to regular expressions and prove it correct, building upon the previous Mission_time_LTL entry in Isabelle/HOL. Additionally, we formalize an algorithm for checking the equivalence of a restricted subset of regular expressions. Both of these algorithms are executable, and the code export is used to validate the existing (previously unverified) WEST tool.
https://www.isa-afp.org/entries/Mission_Time_LTL_to_Regular_Expression.html
Enjoy!
Last updated: Jan 30 2025 at 04:21 UTC