Fast Obligation Translation and Synthesis
For formal verification and synthesis practitioners, this work offers a faster method for handling a fragment of LTL specifications.
The paper presents efficient translation of syntactic obligations to minimal deterministic weak ω-automata using MTBDDs and on-the-fly synthesis, achieving substantial runtime improvements in Spot.
Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak $ω$-automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs), and that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. Our implementation in Spot shows substantial runtime improvements in translation and synthesis.