The 2-Token Theorem: Recognising History-Deterministic Parity Automata Efficiently

History-determinism is a restricted notion of nondeterminism in automata, where the nondeterminism can be successfully resolved based solely on the prefix read so far. Historydeterministic automata still allow for exponential succinctness in automata over infinite words compared to deterministic automata (Kuperberg and Skrzypczak, 2015) , allow for canonical forms unlike deterministic automata (Abu Radi and Kupferman, 2019 and 2020; Ehlers and Schewe, 2022) , and retain some of the algorithmic properties of deterministic automata, for example for reactive synthesis (Henzinger and Piterman, 2006; Ehlers and Khalimov, 2024). Despite the topic of history-determinism having received a lot of attention over the last decade, the complexity of deciding whether a parity automaton is history-deterministic has, up till now, remained open. We show that history-determinism for a parity automaton with a fixed parity index can be checked in PTIME, thus improving upon the naive EXPTIME upper bound of Henzinger and Piterman that has stood since 2006. More precisely, we show that the so-called 2-token game, which can be solved in PTIME for parity automata with a fixed parity index, characterises history-determinism for parity automata. This game was introduced by Bagnol and Kuperberg in 2018, who showed that to decide if a Büchi automaton is history-determinism, it suffices to find the winner of the 2-token game on it. They conjectured that this 2-token game based characterisation extends to parity automata. Boker, Kuperberg, Lehtinen, and Skrzypcak showed in 2020 that this conjecture holds for coBüchi automata as well. We prove Bagnol and Kuperberg's conjecture that the winner of the 2-token game characterises history-determinism on parity automata. As consequences of our result, we also get the 2-token game based characterisation for history-determinism in alternating parity automata and ω-regular automata with any acceptance condition, thus yielding efficient algorithms for deciding their history-determinism. Additionally, we also obtain an efficient algorithm for deciding the good-enough-synthesis (Almagor and Kupferman, 2020) for specifications given by a deterministic parity automata.