In automata theory, while determinisation provides a standard route to solving many common problems in automata theory, some weak forms of nondeterminism can be dealt with in some problems without costly determinisation. For example, the handling of specifications given by nondeterministic automata over infinite words for the problems of reactive synthesis or runtime verification requires resolving nondeterministic choices without knowing the future of the input word. We define and study classes of $\omega$-regular automata for which the nondeterminism can be resolved by a policy that uses a combination of memory and randomness on any input word, based solely on the prefix read so far. We examine two settings for providing the input word to an automaton. In the first setting, called adversarial resolvability, the input word is constructed letter-by-letter by an adversary, dependent on the resolver's previous decisions. In the second setting, called stochastic resolvability, the adversary pre-commits to an infinite word and reveals it letter-by-letter. In each setting, we require the existence of an almost-sure resolver, i.e., a policy that ensures that as long as the adversary provides a word in the language of the underlying nondeterministic automaton, the run constructed by the policy is accepting with probability 1. The class of automata that are adversarially resolvable is the well-studied class of history-deterministic automata. The case of stochastically resolvable automata, on the other hand, defines a novel class. Restricting the class of resolvers in both settings to stochastic policies without memory introduces two additional new classes of automata. We show that the new automaton classes offer interesting trade-offs between succinctness, expressivity, and computational complexity, providing a fine gradation between deterministic automata and nondeterministic automata.

翻译：在自动机理论中，确定性化提供了解决自动机理论中许多常见问题的标准途径，但某些弱形式的非确定性可以在无需昂贵确定性化的情况下处理某些问题。例如，在反应式综合或运行时验证问题中，处理由无限词上的非确定性自动机给出的规约时，需要在不知道输入词未来部分的情况下解决非确定性选择。我们定义并研究了一类$\omega$-正则自动机，对于这类自动机，其非确定性可以通过一种策略来解决，该策略在任何输入词上仅基于已读取的前缀，结合使用存储和随机性。我们考察了向自动机提供输入词的两种设置。在第一种称为对抗可解性的设置中，输入词由对手根据解析器先前的决策逐字母构造。在第二种称为随机可解性的设置中，对手预先承诺一个无限词并逐字母揭示它。在每种设置中，我们要求存在一个几乎必然解析器，即一种策略，确保只要对手提供的词在底层非确定性自动机的语言中，该策略所构造的运行以概率1被接受。对抗可解的自动机类是经过充分研究的历史确定性自动机类。另一方面，随机可解的自动机情况定义了一个新颖的类。将两种设置中的解析器类限制为无记忆的随机策略，引入了两个额外的新自动机类。我们证明这些新的自动机类在简洁性、表达能力和计算复杂性之间提供了有趣的权衡，从而在确定性自动机和非确定性自动机之间提供了精细的分级。