History-Deterministic B\"uchi Automata are Succinct

TL;DR

This paper presents a history-deterministic B"uchi automaton that is strictly more succinct than any equivalent deterministic B"uchi automaton, solving a longstanding open problem through theoretical and computational methods.

Contribution

It introduces the first example of a history-deterministic B"uchi automaton with fewer states than any equivalent deterministic automaton, resolving a decade-long open question.

Findings

Automaton has 65 states, demonstrating succinctness.

Proof combines theoretical insights with computational verification.

Addresses a longstanding open problem in automata theory.

Abstract

We describe a history-deterministic B\"uchi automaton that has strictly less states than every language-equivalent deterministic B\"uchi 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.