Logo image
Back
Formalizing MLTL Formula Progression in Isabelle/HOL
Preprint   Open access

Formalizing MLTL Formula Progression in Isabelle/HOL

Katherine Kosaian, Zili Wang, Elizabeth Sloan and Kristin Rozier
ArXiv.org
Cornell University
10/04/2024
DOI: 10.48550/arxiv.2410.03465
url
https://doi.org/10.48550/arxiv.2410.03465View
Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

Abstract

Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification, model checking, and other formal methods, driving a need for a larger tool base for analysis of this logic. To that end, we formalize formula progression for MLTL in the theorem prover Isabelle/HOL. As groundwork, we first formalize the syntax and semantics for MLTL as well as a verified 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 formula progression, following the literature. 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 functionality to generate a code export. This enables both a formal basis for correctly evaluating MLTL formulas and for automatically generating provably correct benchmarks for evaluating tools that reason about MLTL.
Computer Science - Logic in Computer Science

Details

Metrics

7 Record Views
Logo image