Checking History-Determinism is NP-hard for Parity Automata

TL;DR

This paper proves that checking history-determinism in parity automata is NP-hard, improving previous bounds, and explores related problems with varying computational complexities, including quasi-polynomial solutions.

Contribution

It establishes NP-hardness of checking history-determinism in parity automata and adapts techniques to related problems, refining complexity bounds.

Findings

Checking simulation between nondeterministic parity automata is NP-hard.

Deciding history-determinism for a parity automaton is NP-hard.

Language containment problem can be decided in quasi-polynomial time.

Abstract

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.