Formally Verifying a Transformation from MLTL Formulas to Regular Expressions

Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier

Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification logics like STL and MTL, is often used to model and verify real world systems in safety-cri…