Email Gateway (Aug 08 2025 at 18:17): Email Gateway (Aug 08 2025 at 18:17):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Another new entry expands the MLTL anthology. Specifically, this entry is about taking “derivatives” of MLTL formulas on a given trace:
Mission-time Linear Temporal Logic Formula Progression
by Katherine Kosaian and Zili Wang
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.
https://www.isa-afp.org/entries/Mission_Time_LTL_Formula_Progression.html
Enjoy!
Email Gateway (Aug 14 2025 at 10:36):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Erratum: one author has been omitted at entry submission time by mistake. The correct author list is:
Katherine Kosaian, Zili Wang, and Elizabeth Sloan
(This has been corrected now in the AFP. You may need to reload the page in your browser to see the changes.)
Best wishes,
Dmitriy
On 8 Aug 2025, at 20.16, Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk> wrote:
Dear all,
Another new entry expands the MLTL anthology. Specifically, this entry is about taking “derivatives” of MLTL formulas on a given trace:
Mission-time Linear Temporal Logic Formula Progression
by Katherine Kosaian and Zili Wang
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<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.
Enjoy!
Last updated: Aug 20 2025 at 20:23 UTC