About WEST

The WEST tool provides an automated way to generate regular expressions describing the set of all satisfying traces to Mission-time Linear Temporal Logic (MLTL) formulas. The graphic interface allows users to analyze MLTL formulas by randomly generating satisfying and unsatisfying traces, see how changing the truth value of variables at different steps affects the formula, import and export traces from files, and more.

Please see our GitHub to install the WEST tool. We have also formally verified the algorithms in Isabelle/HOL, and our formalization can be found on the Archive of Formal Proofs. We also have a software artifact available on Zenodo.

Publications

1. Jenna Elwing, Laura Gamboa Guzman, Jeremy Sorkins, Chiara Travesset, Zili Wang, Kristin Rozier. Mission-time LTL (MLTL) Formula Validation Via Regular Expressions, International Conference on integrated Formal Methods (iFM), 2023 Proceedings, doi.org/10.1007/978-3-031-47705-8_15.
   
2. Zili Wang, Laura P. Gamboa Guzman+, Kristin Y. Rozier. WEST: Interactive Validation of Mission-time Linear Temporal Logic (MLTL), to appear in Science of Computer Programming, 2025.
   
3. Zili Wang, Katherine Kosaian, Kristin Rozier. Formally Verifying a Transformation from MLTL Formulas to Regular Expressions, to appear in the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2025, preprint available.

Watch a video demonstration of the WEST tool in action!

Please contact Zili Wang or the team at the Laboratory for Temporal Logic for any questions regarding WEST.