A Hierarchy of Nondeterminism

TL;DR

This paper develops and analyzes a three-tier hierarchy of nondeterminism for ω-automata: determinizable by pruning ($DBP$), history deterministic ($HD$), and semantically deterministic ($SD$). It treats Büchi, co-Büchi, and weak automata, establishing strictness of the hierarchy in general and detailing expressive-power relations among levels, as well as the complexities of deciding a given automaton’s level. It introduces almost-determinization by pruning (almost-$DBP$) and shows that for Büchi and weak automata semantic determinism implies almost-$DBP$, while co-Büchi requires HD; it also proves SD NCWs may fail to be almost-$DBP$ whereas all HD NCWs are. The work connects nondeterminism to probabilistic reasoning through MDPs, defining good-for-MDPs (GFM) and showing how GFMness relates to the hierarchy, including that all GFM automata are almost-$DBP$ and that SD implies GFM only in the Büchi case, with richer behavior for other acceptance conditions. Overall, the paper deepens understanding of when nondeterminism can be tamed, offering complexity bounds, construction techniques (e.g., determinization by subset-like constructions that preserve weakness), and insights for applications in verification, synthesis, and probabilistic modeling.

Abstract

We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton $\mathcal{A}$ is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to $\mathcal{A}$ by removing some of its transitions. Then, $\mathcal{A}$ is history deterministic (HD) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, $\mathcal{A}$ is semantically deterministic (SD) if different nondeterministic choices in $\mathcal{A}$ lead to equivalent states. Some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism. For example, DBP automata are useful in the analysis of online algorithms, and HD automata are useful in synthesis and control. For automata on finite words, the three levels in the hierarchy coincide. We study the hierarchy for Büchi, co-Büchi, and weak automata on infinite words. We show that the hierarchy is strict, study the expressive power of the different levels in it, as well as the complexity of deciding the membership of a language in a given level. Finally, we describe a probability-based analysis of the hierarchy, which relates the level of nondeterminism with the probability that a random run on a word in the language is accepting. We relate the latter to nondeterministic automata that can be used when reasoning about probabilistic systems.

Figures (7)

• Figure 1: An SD-NWW that is not HD.
• Figure 2: The structure of the NWW constructed in \ref{['sd pspace']}.
• Figure 3: The transitions to and from the states $q_k^0$ and $q_k^1$ in ${\mathcal{A}}_\varphi$.
• Figure 4: An NWW that is not almost-DBP.
• Figure 5: An SD-NCW that is not almost-DBP.

Theorems & Definitions (50)

• Theorem 3.1
• proof
• Theorem 3.2
• proof
• Theorem 4.1
• proof
• Theorem 4.2
• proof
• Proposition 4.3
• proof