Mission-time Linear Temporal Logic to Regular Expressions (Q7361278)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Mission_Time_LTL_to_Regular_Expression
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Mission-time Linear Temporal Logic to Regular Expressions |
AFP entry Mission_Time_LTL_to_Regular_Expression |
Statements
24 January 2025
0 references
Zili Wang
0 references
Katherine Kosaian
0 references
Mission-time Linear Temporal Logic to Regular Expressions (English)
0 references
We formalize the WEST algorithm for translating from Mission-time Linear Temporal Logic Formulas to regular expressions and prove it correct, building upon the previous Mission_time_LTL entry in Isabelle/HOL. Additionally, we formalize an algorithm for checking the equivalence of a restricted subset of regular expressions. Both of these algorithms are executable, and the code export is used to validate the existing (previously unverified) WEST tool.
0 references
