Mission-Time LTL (MLTL) Formula Validation via Regular Expressions
Date
2023-11-06
Authors
Elwing, Jenna
Gamboa-Guzman, Laura
Sorkin, Jeremy
Travesset, Chiara
Wang, Zili
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Springer, Cham
Abstract
Mission-time Linear Temporal Logic (MLTL) represents the most practical fragment of Metric Temporal Logic; MLTL resembles the popular logic Linear Temporal Logic (LTL) with finite closed-interval integer bounds on the temporal operators. Increasingly, many tools reason over MLTL specifications, yet these tools are useful only when system designers can validate the input specifications. We design an automated characterization of the structure of the computations that satisfy a given MLTL formula using regular expressions. We prove soundness and completeness of our structure. We also give an algorithm for automated MLTL formula validation and analyze its complexity both theoretically and experimentally. Additionally, we generate a test suite using control flow diagrams to robustly test our implementation and release an open-source tool with a user-friendly graphical interface. The result of our contributions are improvements to existing algorithms for MLTL analysis, and are applicable to many other tools for automated, efficient MLTL formula validation. Our updated tool may be found at https://temporallogic.org/research/WEST.
Series Number
Journal Issue
Is Version Of
Versions
Series
Academic or Administrative Unit
Type
Presentation
Comments
This is a manuscript of a proceeding published as Elwing, Jenna, Laura Gamboa-Guzman, Jeremy Sorkin, Chiara Travesset, Zili Wang, and Kristin Yvonne Rozier. "Mission-time ltl (mltl) formula validation via regular expressions." In International Conference on Integrated Formal Methods, pp. 279-301. Cham: Springer Nature Switzerland, 2023.
doi: https://doi.org/10.1007/978-3-031-47705-8_15.