Data_Sheet_7_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自动机不仅兼具理论研究价值与学术趣味性，还可在诸多应用场景中替代确定性自动机，其中最具代表性的应用方向为反应式综合，因此该类自动机受到了国际研究界的广泛关注。本综述梳理了HD ω正则自动机的发展脉络，阐释了历史确定性与其他类型有界非确定性的关联，研究了HD自动机的确定化方法及其相较于确定性自动机的表达简洁性，并探讨了HD自动机的相关变体、扩展方向以及公开问题。