History-Deterministic Büchi Automata are Succinct
Resolves a decade-old open problem in formal language theory for automata theorists.
The authors construct a history-deterministic Büchi automaton with 65 states that is strictly more succinct than any equivalent deterministic Büchi automaton, solving an open problem in automata theory.
We describe a history-deterministic Büchi automaton that has strictly less states than every language-equivalent deterministic Büchi automaton. This solves a problem that had been open since the introduction of history-determinism and actively investigated for over a decade. Our example automaton has 65 states, and proving its succinctness requires the combination of theoretical insights together with the aid of computers.