Fast Obligation Translation and Synthesis

Abstract

Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak $\ddot{I}‰$-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.