Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing MLTL Formula Progression in Isabelle/HOL

Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Rozier

TL;DR

The paper addresses the need for a formal, trustable foundation for MLTL by formalizing MLTL syntax and semantics in Isabelle/HOL, constructing a library of properties (duality, NNF, custom induction), and rigorously verifying the MLTL formula progression algorithm. It fixes gaps in prior proofs and ensures executability via Isabelle's code generator, yielding a central, extensible MLTL formalization. The key contributions include semantic equivalences and dualities, a robust induction framework (bnf_induct) with well-defined-interval assumptions, a comprehensive treatment of computation length (complen) and related lemmas, and corrected progressions with validated theorems (Decomposition, Satisfiability Preservation, Correctness). The work enables tool validation and provides a foundation for integrating MLTL formalization with existing and future verification tools, potentially impacting runtime verification and model checking workflows. The executable progression engine and formalization of computation-length concepts also pave the way for verified MLTL tooling and cross-logic bridges (e.g., MLTL-to-regex, VeriMon, Vydra).

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.

Formalizing MLTL Formula Progression in Isabelle/HOL

TL;DR

The paper addresses the need for a formal, trustable foundation for MLTL by formalizing MLTL syntax and semantics in Isabelle/HOL, constructing a library of properties (duality, NNF, custom induction), and rigorously verifying the MLTL formula progression algorithm. It fixes gaps in prior proofs and ensures executability via Isabelle's code generator, yielding a central, extensible MLTL formalization. The key contributions include semantic equivalences and dualities, a robust induction framework (bnf_induct) with well-defined-interval assumptions, a comprehensive treatment of computation length (complen) and related lemmas, and corrected progressions with validated theorems (Decomposition, Satisfiability Preservation, Correctness). The work enables tool validation and provides a foundation for integrating MLTL formalization with existing and future verification tools, potentially impacting runtime verification and model checking workflows. The executable progression engine and formalization of computation-length concepts also pave the way for verified MLTL tooling and cross-logic bridges (e.g., MLTL-to-regex, VeriMon, Vydra).

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.
Paper Structure (19 sections, 4 equations, 3 figures, 1 table)

This paper contains 19 sections, 4 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Encoding MLTL in Isabelle/HOL
  3. Syntax
  4. Semantics
  5. Properties
  6. Useful Functions and Custom Induction Rules
  7. Formula Progression
  8. Encoding the Formula Progression Algorithm
  9. Verifying Theorem 1: Decomposition
  10. Verifying Theorem 2: Satisfiability Preservation
  11. Verifying Theorem 3 and Corollary 1: Correctness
  12. Challenges and Insights
  13. Conclusion and Future Work
  14. Acknowledgements
  15. Appendix A
  16. ...and 4 more sections

Figures (3)

  • Figure 1: Prefix and suffix notation for traces.
  • Figure 2: Here, we have two Boolean variables, $p$ and $q$, and four timesteps. At time $0$, $p$ is true (and $q$ is false), at time $1$, $p$$q$ are both true, etc. In Isabelle, we represent this in the list $[\{p\},\{p, q\}, \{q\},\{p\}]$.
  • Figure 3: We summarize the top-level results for formula progression and our modifications, comparing the number of lines in the existing proof sketches LR18 with the corresponding LOC in Isabelle/HOL. As our formal proof of Theorem 3 required identifying and formalizing many properties of computation length (not present in the source material), we count these in the LOC.