Eventually Safe Languages

Good-for-Games (GFG) automata constitute a sound alternative to determinism as a way to model specifications in the Church synthesis problem. Typically, inputs for the synthesis problem are in the form of LTL formulas. However, the only known examples where GFG automata present an exponential gap in succinctness compared to deterministic ones are not LTL-definable. We show that GFG automata still enjoy exponential succinctness for LTL-definable languages. We introduce a class of properties called "eventually safe" together with a specification language E nu TL for this class. We finally give an algorithm to produce a Good-for-Games automaton from any E nu TL formula, thereby allowing synthesis for eventually safe properties.