Mission-time Linear Temporal Logic Formula Progression (Q7361264)
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_Formula_Progression
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Mission-time Linear Temporal Logic Formula Progression |
AFP entry Mission_Time_LTL_Formula_Progression |
Statements
28 July 2025
0 references
Katherine Kosaian
0 references
Zili Wang
0 references
Elizabeth Sloan
0 references
Mission-time Linear Temporal Logic Formula Progression (English)
0 references
We build on the Isabelle/HOL formalization of Mission-time Linear Temporal Logic (MLTL) to formalize a formula progression algorithm for MLTL formulas (https://dblp.org/rec/conf/rv/LiR18.html), a key algorithm in the FPROGG tool for generating MLTL benchmarks. The formula progression algorithm takes a MLTL formula and steps through a given trace to partially evaluate a logically equivalent simpler formula at each step, ultimately checking whether or not the trace satisfies the original formula. Our formalization is executable and we export it to code in SML.
0 references
