History-Deterministic Parity Automata: Games, Complexity, and the 2-Token Theorem

TL;DR

This paper proves the 2-token theorem, showing that checking history-determinism for parity automata with fixed parity index is in PTIME, and introduces a polynomial-time determinisation procedure for history-deterministic B"uchi automata.

Contribution

It proves the 2-token theorem for parity automata, confirming the 2-token game characterizes history-determinism, and provides a polynomial-time determinisation method for history-deterministic B"uchi automata.

Findings

The 2-token game characterizes history-determinism for parity automata.

Checking history-determinism with fixed parity index is in PTIME.

Polynomial-time determinisation for history-deterministic B"uchi automata.

Abstract

History-deterministic automata are a restricted class of nondeterministic automata where the nondeterminism while reading an input can be resolved successfully based on the prefix read so far. History-deterministic automata are exponentially more succinct than deterministic automata, while still retaining some of the algorithmic properties of deterministic automata, especially in the context of reactive synthesis. This thesis focuses on the problem of checking history-determinism for parity automata. Our main result is the 2-token theorem, due to which we obtain that checking history-determinism for parity automata with a fixed parity index can be checked in PTIME. This improves 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\"uchi automaton is history-deterministic, it suffices to find the winner of the 2-token game on it. They conjectured that this 2-token game based characterisation of history-determinism extends to parity automata. We prove Bagnol and Kuperberg's conjecture that the winner of the 2-token game characterises history-determinism on parity automata. We also give a polynomial time determinisation procedure for history-deterministic B\"uchi automata, thus solving an open problem of Kuperberg and Skrzypczak from 2015. This result is a consequence of our proof of the 2-token theorem. Finally, we also show NP-hardness for the problem of checking history-determinism for parity automata when the parity index is not fixed. This is an improvement from the lower bound of solving parity games shown by Kuperberg and Skrzypczak in 2015.