Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Checking History-Determinism is NP-hard for Parity Automata

Aditya Prakash

TL;DR

This work establishes strong complexity barriers for history-determinism and related notions in nondeterministic parity automata. By a central reduction from $2$-D parity games, it proves $NP$-hardness for both simulation between parity automata and history-determinism, improving upon prior lower bounds tied to parity-game solving. It further shows that Eve can win the $1$-token and $2$-token games with corresponding hardness, and provides a quasi-polynomial time algorithm for language containment of a nondeterministic parity automaton into an HD parity automaton via a Muller-to-Parity conversion and a parity-game solve. The results delineate the landscape between $NP$-hardness and existing exponential-time upper bounds, and point to future work on the two-token conjecture and potential tighter complexity classifications for HD verification. Overall, the paper advances our understanding of the algorithmic limits and tractability for HD structures in parity automata and their verification/synthesis implications.

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.

Checking History-Determinism is NP-hard for Parity Automata

TL;DR

This work establishes strong complexity barriers for history-determinism and related notions in nondeterministic parity automata. By a central reduction from -D parity games, it proves -hardness for both simulation between parity automata and history-determinism, improving upon prior lower bounds tied to parity-game solving. It further shows that Eve can win the -token and -token games with corresponding hardness, and provides a quasi-polynomial time algorithm for language containment of a nondeterministic parity automaton into an HD parity automaton via a Muller-to-Parity conversion and a parity-game solve. The results delineate the landscape between -hardness and existing exponential-time upper bounds, and point to future work on the two-token conjecture and potential tighter complexity classifications for HD verification. Overall, the paper advances our understanding of the algorithmic limits and tractability for HD structures in parity automata and their verification/synthesis implications.

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.
Paper Structure (20 sections, 15 theorems, 3 equations, 4 figures)

This paper contains 20 sections, 15 theorems, 3 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Parity conditions
  4. Parity automata
  5. Game arenas
  6. Parity games
  7. Muller conditions and Zielonka trees
  8. 2-dimensional parity game
  9. Simulation
  10. History-determinism
  11. Token games
  12. Simulation is $\NP$-hard
  13. Checking History-Determinism is $\NP$-hard
  14. Good 2-D parity games
  15. $\NP$-hardness of checking history-determinism
  16. ...and 5 more sections

Key Result

lemma 1

Let $(C,\mathcal{F})$ be a Muller condition with the Zielonka tree $Z_{C,\mathcal{F}}$ that has $n$ leaves and height $h$. Then there is a deterministic parity automaton $\mathcal{D}_{C,\mathcal{F}}$ that can be constructed in polynomial time such that $\mathcal{D}_{C,\mathcal{F}}$ has $n$ states an

Figures (4)

  • Figure 1: A snippet of a game $\mathcal{G}$, and the corresponding automata $\mathcal{D}$ and $\mathcal{H}$ constructed in the reduction. The Adam vertices are represented by pentagons and Eve vertices by squares. The automaton $\mathcal{D}$ is deterministic, and $\mathcal{H}$ contains a copy of $\mathcal{D}$.
  • Figure 2: Zielonka trees $Z_0$ and $Z_1$
  • Figure 3: Zielonka tree $Z_{2k}$
  • Figure 4: Zielonka tree $Z_{2k+1}$

Theorems & Definitions (27)

  • remark 1
  • definition 1: Zielonka tree
  • lemma 1: CCF21
  • lemma 2
  • theorem 1: CHP07
  • remark 2
  • definition 2: Simulation game
  • definition 3: Letter game
  • definition 4: $k$-token game
  • lemma 3: BK18
  • ...and 17 more