Fully Generalized Reactivity (1) Synthesis

Recently Ehlers&Schewe proposed a canonical minimal representation foromega-regular languages [1]. The representation consists of a canonical chainof co-Büchi languages (COCOA): A1 ⊃ A2 ⊃. .. ⊃ An, where each Ai is expressibleby a good-for-games co-Büchi automaton, canonical and minimal by the work ofAbu Radi and Kupferman [2]. This work presents a first application of the newrepresentation, to the problem of reactive synthesis. In reactive synthesis wewant to automatically construct a transducer from a specification in e. g. linear temporal logic. The flow of our construction is: translate a given LTLinto a parity automaton and into COCOA using [1, 2], then we construct amu-calculus fixpoint formula which is evaluated on a game graph of thesynthesis problem. The resulting procedure generalizes the widely knownGeneralized Reactivity (1) synthesis approach to full LTL while inheriting itsefficiency advantages on the original specification class. This is a joint work with Rüdiger Ehlers (main contributor). [1]: Natural Colors of Infinite Words, by Rüdiger Ehlers and Sven Schewe[2]: Minimization and Canonization of GFG Transition-Based Automata, by Bader {Abu Radi} and Orna Kupferman Contributed talk given by Ayrat Khalimov

Authors

• Ayrat Khalimov

Keywords

No keywords are indexed for this paper.