Formalizing MLTL Formula Progression in Isabelle/HOL

TL;DR

This paper formalizes the syntax, semantics, and progression algorithms of Mission-time Linear Temporal Logic (MLTL) in Isabelle/HOL, providing a trustworthy foundation for verification tools and correcting previous errors.

Contribution

It introduces a formal Isabelle/HOL library for MLTL, including properties, induction rules, and verified progression algorithms, enhancing reliability and future formalizations.

Findings

Formal syntax and semantics of MLTL established

Verified progression algorithms with correctness proofs

Identified and corrected errors in existing MLTL source material

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.