Checking History-Determinism is NP-hard for Parity Automata
For automata theorists, this establishes the computational hardness of a key verification problem for parity automata.
The paper proves that checking history-determinism for parity automata is NP-hard, improving on a previous lower bound, and also shows that deciding language containment for history-deterministic parity automata is solvable in quasi-polynomial time.
We show that the problem of checking if a given nondeterministic parity automaton simulates another given nondeterministic parity automaton is NP-hard. We then adapt the techniques used for this result to show that the problem of checking history-determinism for a given parity automaton is NP-hard. This is an improvement from Kuperberg and Skrzypczak's previous lower bound of solving parity games from 2015. We also show that deciding if Eve wins the one-token game or the two-token game of a given parity automaton is NP-hard. Finally, we show that the problem of deciding if the language of a nondeterministic parity automaton is contained in the language of a history-deterministic parity automaton can be solved in quasi-polynomial time.