Characterizing the Polynomial-Time Minimizable $ω$-Automata

TL;DR

This work completes the landscape for polynomial-time minimization of automata over infinite words by showing that deterministic co-Büchi automata with transition-based acceptance and history-deterministic Büchi automata with transition-based acceptance are NP-hard to minimize. The authors establish this via a Hamiltonian-path–based reduction, first building a minimal HD-tNCW from a graph and then reducing to a polynomial-size deterministic co-Büchi automaton using an alphabet-size reduction. A crucial step encodes the graph with an exponential alphabet and then compresses it to a polynomial-size encoding that preserves language equivalence, enabling NP-hardness results to hold in the polynomial-input regime. The paper also demonstrates NP-completeness for the minimization of transition-based automata across several acceptance classes, highlighting the significant impact of transition-based acceptance on minimization complexity and informing future ω-automata representations for reactive systems.

Abstract

A central question in the theory of automata is which classes of automata can be minimized in polynomial time. We close the remaining gaps for deterministic and history-deterministic automata over infinite words by proving that deterministic co-Büchi automata with transition-based acceptance are NP-hard to minimize, as are history-deterministic Büchi automata with transition-based acceptance.

Figures (1)

• Figure 1: The tNCW $e({\cal A}^{G^{v_1}})$.

Theorems & Definitions (35)

• Example 1
• Definition 2
• Theorem 3
• Theorem 4
• Proposition 5: Direction 1 of Theorem \ref{['corr thm']}
• Proposition 6: Direction 2 of Theorem \ref{['corr thm']}
• Proposition 7
• Theorem 8
• Proposition 9
• Lemma 10