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\"uchi, co-B\"uchi, 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.
翻译:我们研究了非确定性的一种层次结构中的三个层次:一个非确定性自动机 $\mathcal{A}$ 若可通过剪枝确定化(DBP),则意味着我们可以通过移除其部分转移来获得一个等价于 $\mathcal{A}$ 的确定型自动机。其次,$\mathcal{A}$ 是历史确定的(HD),如果其非确定性选择能够以仅依赖于历史的方式得到解析。最后,$\mathcal{A}$ 是语义确定的(SD),如果 $\mathcal{A}$ 中不同的非确定性选择会导致等价的状态。形式化方法中自动机的某些应用需要确定型自动机,但实际上可以利用具有某种程度非确定性的自动机。例如,DBP自动机在在线算法分析中非常有用,而HD自动机在综合与控制中具有重要作用。对于有限词上的自动机,这三个层次是一致的。我们研究了Büchi、co-Büchi以及无穷词上的弱自动机的层次结构。我们证明该层次结构是严格的,研究了其中不同层次的表现力,以及判断一个语言是否属于给定层次的复杂度。最后,我们描述了一种基于概率的层次分析,该分析将非确定性层次与语言中随机运行被接受的概率联系起来,并将后者与可用于推理概率系统的非确定性自动机关联起来。