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.
Cite
@article{arxiv.2605.12372,
title = {Fast Obligation Translation and Synthesis},
author = {Alexandre Duret-Lutz and Giuseppe De Giacomo and Marcin Jurdzinski and Nir Piterman and Moshe Y. Vardi and Shufang Zhu},
journal= {arXiv preprint arXiv:2605.12372},
year = {2026}
}