一句话:研究无限字上自动机非确定性的三层分级,证明其严格性并分析表达力、判定复杂度与概率刻画。
本文研究非确定性的一种层级:可剪枝确定化(DBP)、历史确定性(HD)和语义确定性(SD)。对有限字自动机,三者等价;对无限字上的 Büchi、co-Büchi 与 weak 自动机,作者证明该层级严格,并刻画各层语言的表达力,分析判定给定语言属于哪一层的复杂度。此外,文章提出基于概率的分析,将非确定性层级与“在语言中某词上随机运行接受的概率”联系起来,并关联到可用于概率系统推理的非确定性自动机。该工作为形式方法中需要确定性的应用(如在线算法分析、合成与控制)提供了更细的非确定性自动机选择依据。
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.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{abs-2209-09866,
title = {A Hierarchy of Nondeterminism},
author = {Bader Abu Radi and Orna Kupferman and Ofer Leshkowitz},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:13)2025}
}