Formalizing MLTL Formula Progression in Isabelle/HOL
Abstract
Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trustworthy tool base for analyzing MLTL. In this work, we formalize the syntax and semantics of MLTL and a library of key properties, including useful custom induction rules. We envision this library as being useful for future formalizations involving MLTL and as serving as a reference point for theoretical work using or developing MLTL. We then formalize the algorithm and correctness theorems for MLTL formula progression; along the way, we identify and fix several errors and gaps in the source material. A main motivation for our work is tool validation; we ensure the executability of our algorithms by using Isabelle's built-in code generator.
Cite
@article{arxiv.2410.03465,
title = {Formalizing MLTL Formula Progression in Isabelle/HOL},
author = {Katherine Kosaian and Zili Wang and Elizabeth Sloan and Kristin Rozier},
journal= {arXiv preprint arXiv:2410.03465},
year = {2025}
}