Fast Obligation Translation and Synthesis
Alexandre Duret-Lutz, Giuseppe De Giacomo, Marcin Jurdzinski, Nir Piterman, Moshe Y. Vardi, Shufang Zhu

TL;DR
This paper introduces an efficient method for translating syntactic obligations into minimal deterministic weak automata using MTBDDs, enabling faster synthesis directly on this representation.
Contribution
It presents a novel approach for converting syntactic obligations into minimal DWA with MTBDDs and performs synthesis efficiently on this structure.
Findings
Substantial runtime improvements in translation and synthesis.
Efficient conversion to minimal DWA using MTBDDs.
Implementation in Spot demonstrates practical benefits.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
