On unambiguous finite automata

11^th April 2024, 11:00 Ashton Lecture Theatre
Prof. Stefan Kiefer
Department of Computer Science, University of Oxford

Abstract

Finite automata are fundamental for automated verification. A nondeterministic finite automaton is called unambiguous if every accepted word has only one accepting run. Thus, unambiguous automata are in between deterministic and nondeterministic automata. They are naturally connected to linear algebra and combinatorics. The infinite-word version of unambiguous automata, unambiguous Büchi automata, can be used to model check Markov chains. These algorithms are both mathematically elegant and practically efficient for the verification of probabilistic systems. Based on new connections to communication complexity, there has been recent progress around state minimisation and the complexity of language operations on unambiguous automata.