Chains of co-Büchi automata (COCOA) have recently been introduced as a new canonical representation of omega-regular languages. The co-Büchi automata in a chain assign each omega-word its natural color, which depends only on the language itself and not on the chosen automaton representation. Automata in such a chain can be minimized in polynomial time and are good-for-games, making this representation attractive for verification and reactive synthesis. However, in these applications, specifications are usually given in linear temporal logic (LTL). To make COCOA useful, an LTL specification must first be translated into the chain of automata. The only translation currently known proceeds via deterministic parity automata (LTL$\,{\to}\,$DPA$\,{\to}\,$COCOA), where the first step ignores natural colors and requires involved constructions due to Safra or Esparza et al. This raises the question of whether, by exploiting the definition of the natural color of words, one can avoid such constructions and obtain a direct translation from LTL to COCOA. In this paper, we present a simple yet optimal translation from LTL to COCOA, as well as a variant that translates LTL into DPA. The translation represents a new path from LTL to DPA and exploits the definition of natural colors. It relies on standard operations on weak alternating automata, the Miyano-Hayashi breakpoint construction, the subset construction, and simple graph algorithms. Starting from weak alternating automata, the procedure also applies to specifications in linear dynamic logic. The procedure runs in asymptotically optimal doubly exponential time and produces automata of asymptotically optimal size.

Abstract 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ü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 approaches and retains the efficiency of GR(1) synthesis for specifications in GR(1) form and those with few non-GR(1) specification parts.