Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata
Rohan Acharya, Marcin Jurdziński, Aditya Prakash
TL;DR
The paper tackles the problem of determinising history-deterministic Büchi automata in polynomial time. It introduces a novel lookahead framework, showing that the 1-token game suffices and is equivalent to k-lookahead games, and proves that this characterisation yields a polynomial-time determinisation with a quadratic blow-up via sprint self-simulation techniques. By reducing game-based characterisations to universal automata, the authors establish SD Büchi criteria and leverage Joker games to obtain efficient HD Büchi recognition, while demonstrating that Joker games do not extend to parity automata. The results significantly advance the understanding of HD automata by providing a conceptually simpler and practically efficient determinisation method and by clarifying the limitations of lookahead-based tools on parity. Collectively, these contributions enhance synthesis and verification workflows by enabling efficient handling of history-deterministic properties and automata-based decision procedures.
Abstract
Our main technical contribution is a polynomial-time determinisation procedure for history-deterministic Büchi automata, which settles an open question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead game, which is a variant of Bagnol and Kuperberg's token game, in which Adam is given a fixed lookahead. We prove that the lookahead game is equivalent to the 1-token game. This allows us to show that the 1-token game characterises history-determinism for semantically-deterministic Büchi automata, which paves the way to our polynomial-time determinisation procedure.