Mission-time Linear Temporal Logic

Katherine Kosaian 📧, Zili Wang 📧 and Elizabeth Sloan 📧

January 24, 2025

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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.

License

BSD License

Topics

Session Mission_Time_LTL