Fully Generalized Reactivity(1) Synthesis
<|reference_start|>Fully Generalized Reactivity(1) Synthesis: Generalized Reactivity(1) (GR(1)) synthesis is a reactive synthesis approach in which the specification is split into two parts: a symbolic game graph, describing the safe transitions of a system, a liveness specification in a subset of Linear Temporal Logic (LTL) on top of it. Many specifications can naturally be written in this restricted form, and the restriction gives rise to a scalable synthesis procedure -- the reasons for the high popularity of the approach. For specifications even slightly beyond GR(1), however, the approach is inapplicable. This necessitates a transition to synthesizers for full LTL specifications, introducing a huge efficiency drop. This paper proposes a synthesis approach that smoothly bridges the efficiency gap from GR(1) to LTL by unifying synthesis for both classes of specifications. The approach leverages a recently introduced canonical representation of omega-regular languages based on a chain of good-for-games co-B\"uchi automata (COCOA). By constructing COCOA for the liveness part of a specification, we can then build a fixpoint formula that can be efficiently evaluated on the symbolic game graph. The COCOA-based synthesis approach outperforms standard approaches and retains the efficiency of GR(1) synthesis for specifications in GR(1) form and those with few non-GR(1) specification parts.<|reference_end|>
@article{ehlers2024fully,
    title={Fully Generalized Reactivity(1) Synthesis},
    author={R"udiger Ehlers and Ayrat Khalimov},
    journal={arXiv preprint arXiv:2402.02979},
    year={2024},
    archivePrefix={arXiv},
    eprint={2402.02979},
    primaryClass={cs.FL}
}