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.

翻译：句法义务是LTL公式的一个片段，可转化为确定性弱$ω$-自动机（DWA）。我们证明，句法义务可以高效地转换为用多终端二叉决策图（MTBDD）表示的最小DWA，并且此类规格的综合问题可以直接在MTBDD表示上即时求解。我们在Spot工具中的实现表明，翻译和综合的运行时间得到了显著提升。