WEST: Interactive Validation of Mission-time LTL (MLTL) Via Regular Expressions

This webpage contains further details and artifacts for reproducibility of the experiments in:

Elwing, J., Gamboa-Guzman, L., Sorkin, J., Travesset, C., Wang, Z., Rozier, K.Y. (2024). Mission-time LTL (MLTL) Formula Validation Via Regular Expressions. In: Herber, P., Wijs, A. (eds) iFM 2023. iFM 2023. Lecture Notes in Computer Science, vol 14300. Springer, Cham. https://doi.org/10.1007/978-3-031-47705-8_15.
Wang, Z., Gamboa-Guzman, L., Rozier, K.Y. (2024) WEST: Interactive Validation of Mission-time Linear Temporal Logic (MLTL). To appear in Science of Computer Programming.

Demo Video - Youtube (Nov. 2023)

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 the 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.