Using the past for resolving the future

Abstract: 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 talk describes the development of HD $\omega$-regular automata, relates history determinism to other types of bounded nondeterminism, discuss the determinization of HD automata and their succinctness with respect to deterministic ones, and discusses variants, extensions, and open problems around HD automata.

formal languages and automata theory

Audience: researchers in the topic

( slides | video )

One FLAT World Seminar