Fast Obligation Translation and Synthesis

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 $\omega$-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.