Minimizing GFG Transition-Based Automata
=================================

While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic  or good-for-games automata. The latter are nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. 
The minimization problem for nondeterministic and deterministic B\"uchi and co-Buchi word automata are PSPACE-complete and NP-complete, respectively. We describe a polynomial minimization algorithm for good-for-games co-Buchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set of designated transitions only finitely often. Our algorithm is based on a sequence of transformations we apply to the automaton, on top of which a minimal quotient automaton is defined.