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-defmable. We show that GFG automata still enjoy exponential succinctness for LTL-defmable languages. We introduce a class of properties called "eventually safe" together with a specification language EvTL for this class. We finally give an algorithm to produce a Good-for-Games automaton from any EvTL formula, thereby allowing synthesis for eventually safe properties.
展开▼
