Fully Generalized Reactivity(1) Synthesis
CoRR(2024)
摘要
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 live- ness 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 intro- duced canonical representation of omega-regular
languages based on a chain of good-for-games co-Büchi 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 ap- proaches and
retains the efficiency of GR(1) synthesis for specifications in GR(1) form and
those with few non-GR(1) specification parts.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要