Explorable Parity Automata

TL;DR

This work introduces explorable automata as a natural extension of history-deterministic automata, where nondeterminism can be resolved by running a bounded number of parallel runs. It establishes that the explorability problem is ExpTime-complete for NFAs and for [0,2] parity automata, via a reduction to and from Bertrand’s population control problem and a capacity-based ExpTime algorithm. For infinite words, it defines ω-explorable automata and proves ExpTime-completeness for ω-explorability under safety and coBüchi conditions, with Büchi ω-explorability mirroring the full ω-regular language class. The expressivity analysis reveals a parity hierarchy collapse at [1,3], with explorable automata recognizing all ω-regular languages in the Büchi case, and shows that exploring with countably many tokens yields distinct outcomes (ω-explorability vs explorability). The paper also develops a detailed framework linking explorability to HDness, and extends the theory to ω-words via elaborated capacity games and targeted elimination constructions, highlighting the role of explorability as a meaningful intermediate notion between determinism and nondeterminism in automata theory.

Abstract

We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one. We show that recognizing HD parity automata of fixed index among explorable ones is in PTime, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is ExpTime-complete, in the case of finite words or parity automata up to index [0, 2]. Additionally, we define the notion of ω-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show ExpTime-completeness for ω-explorability of automata on infinite words for the safety and coBüchi acceptance conditions. We finally characterize the expressivity of (ω-)explorable automata with respect to the parity index hierarchy.

Figures (6)

• Figure 1: An explorable and a non-explorable automata
• Figure 2: An explorable automaton $\mathcal{B}_k$ requiring exponentially many tokens
• Figure 3: The parity hierarchy of languages recognized by the Deterministic/Explorable/Non-deterministic automata. Classes not included in the green collapse region always match their deterministic counterpart.
• Figure 4: Two safety automata. Left: $\omega$-explorable but not explorable. Right: not $\omega$-explorable.
• Figure 5: Transitions for $a_{t,p}$, where $t=(q,b,q',b',d)$, $p'$ is the position at direction $d$ from $p$, and $q"$, $p"$, and $t'$ are different from $q,p,t$ respectively.

Theorems & Definitions (66)

• Definition 2.1: $k$-explorability game
• Example 2.2
• Example 2.3
• Lemma 2.4
• proof
• Theorem 2.5: KM19
• Definition 2.6: Explorability problem
• Definition 2.7
• Lemma 2.8
• proof