Data_Sheet_3_Using the past for resolving the future.PDF

Nondeterminism models an ability to see the future: An automaton with an infinite look ahead can successfully resolve its nondeterministic choices. An automaton is history deterministic (HD) if it can successfully resolve its nondeterministic choices in a way that only depends on the past. Formally, an HD automaton has a strategy that maps each finite word to the transition to be taken after the word is read and following this strategy results in accepting all the words in the language of the automaton. Beyond being theoretically interesting and intriguing, HD automata can replace deterministic automata in several applications, most notably reactive synthesis, and they attract a lot of interest in the research community. The survey describes the development of HD ω-regular automata, relates history determinism to other types of bounded nondeterminism, studies the determinization of HD automata and their succinctness with respect to deterministic ones, and discusses variants, extensions, and open problems around HD automata.

不确定性刻画了一种预知未来的能力：具备无限前瞻能力的自动机可成功消解其不确定性选择。若某自动机能够仅依赖过往历史即可成功消解其不确定性选择，则称其为历史确定性自动机（history deterministic，HD）。严格而言，HD自动机存在一种策略，可将每个有限字串映射至读取该字串后应执行的状态转移；遵循该策略可接受该自动机语言中的所有字串。HD自动机不仅兼具理论研究价值与学术趣味性，还可在诸多应用场景中替代确定性自动机，其中尤以反应式综合（reactive synthesis）领域最为典型，因此该类自动机在学术界广受关注。本综述梳理了HD ω正则自动机（ω-regular automata）的发展脉络，将历史确定性与其他类型的有界不确定性相关联，研究了HD自动机的确定化方法及其相较于确定性自动机的描述简洁性，并探讨了HD自动机的变体、扩展方向以及相关开放问题。