Formalizing MLTL formula progression in Isabelle/HOL

DOI10.1007/978-3-032-07021-0_21MaRDI QIDQ6856402zbMATH OpenFDO

Authors Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Yvonne Rozier

Publication date 19 February 2026

Full work available at URL https://doi.org/10.1007/978-3-032-07021-0_21

zbMATH Keywords

formula progressionmission-time linear temporal logic (MLTL)modal logicruntime verificationtheorem proving

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites work

• An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
• Bounded linear-time temporal logic: a proof-theoretic investigation
• Embedding online runtime verification for fault disambiguation on Robonaut2
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• From Church and Prior to PSL
• Isabelle/HOL. A proof assistant for higher-order logic
• Linear temporal logic symbolic model checking
• Maximum satisfiability of mission-time linear temporal logic
• Model predictive runtime verification for cyber-physical systems with real-time deadlines
• Multi-head Monitoring of Metric Dynamic Logic
• Revisiting MITL to fix decision procedures
• Satisfiability checking for mission-time LTL
• Some Recent Results in Metric Temporal Logic
• The benefits of relaxing punctuality
• The foundation of a generic theorem prover
• Verification: Theory and practice. Essays dedicated to Zohar Manna on the occasion of his 64th birthday.
• VeriMon: a formally verified monitoring tool

This page was built for publication: Formalizing MLTL formula progression in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6856402)