Book chapter
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings, pp.254-275
Lecture Notes in Computer Science, v. 15696, Springer
2025
DOI: 10.1007/978-3-031-90643-5_13
Abstract
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-critical contexts. As the results of formal verification are only as trustworthy as their input specifications, the WEST tool was created to facilitate writing MLTL specifications. Accordingly, it is vital to demonstrate that WEST itself works correctly. To that end, we verify the WEST algorithm, which converts MLTL formulas to (logically equivalent) regular expressions, in the theorem prover Isabelle/HOL. Our top-level result establishes the correctness of the regular expression transformation; we then generate a code export from our verified development and use this to experimentally validate the existing WEST tool. To facilitate this, we develop some verified support for checking the equivalence of two regular expressions.
Details
- Title: Subtitle
- Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
- Creators
- Zili Wang - Iowa State UniversityKatherine Kosaian - University of Iowa, Iowa City, IA, United StatesKristin Yvonne Rozier - Iowa State University
- Resource Type
- Book chapter
- Publication Details
- Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings, pp.254-275
- Publisher
- Springer; Cham
- Series
- Lecture Notes in Computer Science; v. 15696
- DOI
- 10.1007/978-3-031-90643-5_13
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Grant note
- National Science Foundation (http://data.elsevier.com/vocabulary/SciValFunders/100000001) CNS-1552934; CCRI-2016592; GRFP-2024364991 / National Science Foundation (http://data.elsevier.com/vocabulary/SciValFunders/100000001)
- Language
- English
- Date published
- 2025
- Academic Unit
- Computer Science
- Record Identifier
- 9984825636302771
Metrics
1 Record Views