# Minimization and Canonization of GFG Transition-Based Automata

arXiv: https://arxiv.org/abs/2106.06745 · HTML: https://mlsanity.com/paper/2106.06745/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Jun 2021.

## Built on by (most cited first, 1 of 1)

- [Good-for-MDP State Reduction for Stochastic LTL Planning](https://mlsanity.com/paper/2511.09073/) (2025)

## Abstract (arXiv)

While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) 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 deterministic B"uchi and co-B"uchi word automata is NP-complete. In particular, no canonical minimal deterministic automaton exists, and a language may have different minimal deterministic automata. We describe a polynomial minimization algorithm for GFG co-B"uchi 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. We use our minimization algorithm to show canonicity for transition-based GFG co-B"uchi word automata: all minimal automata have isomorphic safe components (namely components obtained by restricting the transitions to these not in α) and once we saturate the automata with α-transitions, we get full isomorphism.