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以及无限词上的弱自动机对应的层级结构。证明该层级结构是严格的,考察其中不同层级的表达能力,以及判定语言是否属于给定层级的复杂度。最后,我们提出基于概率的层级分析,将非确定性程度与语言中随机运行接受词的概率相关联,并将后者与概率系统推理中可使用的非确定性自动机建立联系。