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.

A nondeterministic automaton is semantically deterministic (SD) if different nondeterministic choices in the automaton lead to equivalent states. Semantic determinism is interesting as it is a natural relaxation of determinism, and as some applications of deterministic automata in formal methods can actually use automata with some level of nondeterminism, tightly related to semantic determinism. In the context of finite words, semantic determinism coincides with determinism, in the sense that every pruning of an SD automaton to a deterministic one results in an equivalent automaton. We study SD automata on infinite words, focusing on Büchi, co-Büchi, and weak automata. We show that there, while semantic determinism does not increase the expressive power, the combinatorial and computational properties of SD automata are very different from these of deterministic automata. In particular, SD Büchi and co-Büchi automata are exponentially more succinct than deterministic ones (in fact, also exponentially more succinct than history-deterministic automata), their complementation involves an exponential blow up, and decision procedures for them like universality and minimization are PSPACE-complete. For weak automata, we show that while an SD weak automaton need not be pruned to an equivalent deterministic one, it can be determinized to an equivalent deterministic weak automaton with the same state space, implying also efficient complementation and decision procedures for SD weak automata.

While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) automata. The latter are nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. The minimization problem for deterministic B\"uchi and co-B\"uchi word automata is NP-complete. In particular, no canonical minimal deterministic automaton exists, and a language may have different minimal deterministic automata. We describe a polynomial minimization algorithm for GFG co-B\"uchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set $\alpha$ of designated transitions only finitely often. Our algorithm is based on a sequence of transformations we apply to the automaton, on top of which a minimal quotient automaton is defined. We use our minimization algorithm to show canonicity for transition-based GFG co-B\"uchi word automata: all minimal automata have isomorphic safe components (namely components obtained by restricting the transitions to these not in $\alpha$) and once we saturate the automata with $\alpha$-transitions, we get full isomorphism.

We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton A is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to A by removing some of its transitions. Then, A is good-for-games (GFG) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, A is semantically deterministic (SD) if different nondeterministic choices in 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 GFG 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.

While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games automata. The latter are nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. The minimization problem for nondeterministic and deterministic Büchi and co-Büchi word automata are PSPACE-complete and NP-complete, respectively. We describe a polynomial minimization algorithm for good-for-games co-Büchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set of designated transitions only finitely often. Our algorithm is based on a sequence of transformations we apply to the automaton, on top of which a minimal quotient automaton is defined.