Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications

Suguman Bansal, Yong Li, Lucas M. Tabajara +1

LTLf synthesis is the automated construction of a reactive system from a high-level description, expressed in LTLf, of its finite-horizon behavior. So far, the conversion of LTLf f…