Email Gateway (Mar 04 2025 at 20:40): Email Gateway (Mar 04 2025 at 20:40):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Another AFP entry to expand the recently started MLTL series:
Language Partitioning for Mission-time Linear Temporal Logic
by Zili Wang, Katherine Kosaian, and Alec Rosentrater
Building on the existing formalization of Mission-time Linear Temporal Logic (MLTL), we formalize the notions of language decomposition and language partition for MLTL. More specifically, we formalize an algorithm to compute a language partition for MLTL and formally prove its correctness. Our algorithm is executable, and we export it to Haskell via Isabelle/HOL's code generator.
https://www.isa-afp.org/entries/Mission_Time_LTL_Language_Partition.html
Enjoy!
Last updated: Mar 09 2025 at 12:28 UTC