Language Partitioning for Mission-time Linear Temporal Logic

Zili Wang 📧, Katherine Kosaian 📧 and Alec Rosentrater 📧

March 3, 2025

Abstract

Building on the existing formalization of Mission-time Linear Temporal Logic (MLTL), we formalize the notions of language decomposition and language partition for MLTL. More specifically, we formalize an algorithm to compute a language partition for MLTL and formally prove its correctness. Our algorithm is executable, and we export it to Haskell via Isabelle/HOL's code generator.

License

BSD License

Topics

Related publications

  • Alec Rosentrater, Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. Language Partitioning for Mission-time Linear Temporal Logic. To appear in NASA Formal Methods (NFM) 2025.

Session Mission_Time_LTL_Language_Partition

Depends on

Cite

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

Download

× Download latest