Mission-time Linear Temporal Logic Formula Progression

Katherine Kosaian 📧 and Zili Wang 📧

July 28, 2025

Abstract

We build on the Isabelle/HOL formalization of Mission-time Linear Temporal Logic (MLTL) to formalize a formula progression algorithm for MLTL formulas (https://dblp.org/rec/conf/rv/LiR18.html), a key algorithm in the FPROGG tool for generating MLTL benchmarks. The formula progression algorithm takes a MLTL formula and steps through a given trace to partially evaluate a logically equivalent simpler formula at each step, ultimately checking whether or not the trace satisfies the original formula. Our formalization is executable and we export it to code in SML.

License

BSD License

Topics

Related publications

  • Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Yvonne Rozier. Formalizing MLTL Formula Progression in Isabelle/HOL. To appear in Conference on Intelligent Computer Mathematics (CICM 2025).

Session Mission_Time_LTL_Formula_Progression

Depends on

Cite

× 
@article{Mission_Time_LTL_Formula_Progression-AFP,
  author  = {Katherine Kosaian and Zili Wang},
  title   = {Mission-time Linear Temporal Logic Formula Progression},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2025},
  note    = {\url{https://isa-afp.org/entries/Mission_Time_LTL_Formula_Progression.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download