Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP x 2


view this post on Zulip Email Gateway (Jan 28 2025 at 18:47):

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