This talk is based on joint work with Aditya Prakash and Thomas A. Henzinger Handling specifications given by nondeterministic automata for the problems of reactive synthesis or runtime verification require resolving nondeterministic choices without knowing the future of the input word. We define classes of automata over infinite words in which the nondeterminism can be resolved using a combination of memory and randomness on any input word, based solely on the prefix read so far.
We examine two adversarial settings for providing the input word to the 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 of the settings, we require the existence of almost-sure resolvers---resolvers that can ensure that for any word in the language of the underlying nondeterministic automaton, the run constructed by that resolver is almost-surely accepting.
The class of automata that are adversarially resolvable are equivalent to the well-studied class of history-deterministic automata. The latter case of stochastically resolvable automata defines a novel class. Restricting the class of resolvers in both settings to only memoryless stochastic resolvers further introduces two additional new classes of automata. We show that the new classes offer interesting trade-off between succinctness, expressivity, and computational complexity, providing a finer gradation between deterministic automata and non-deterministic automata.
Short Bio:
Thejaswini is a post-doctoral researcher at Institute of Science and Technology Austria, working with Tom Henzinger. She did her PhD at the University of Warwick and her M.Sc and B.Sc at Chennai Mathematical Institute. She is interested in solving problems motivated in the context of verification or synthesis using logic, games, and automata.
