Finite Automata and the Infinite: A Journey Through 50 Years of Research

21^st January 2015, 11:00 Ashton Lecture Theater
Prof Wolfgang Thomas
Logic and Theory of Discrete Systems
RWTH Aachen
Germany

Abstract

Finite automata have been a central tool in making infinite structures of computer science accessible for algorithmic methods. There are two basic kinds of “infinity”: Infinite system behavior (as seen in non-terminating system runs) and infinite state spaces. In this talk we focus on the second aspect, the verification of infinite-state systems. We present essential stages of research, starting with Büchi’s study of prefix rewriting systems in 1964, continuing with Rabin’s tree theorem of 1969, and ending with more recent progress (based on results of Muchnik, Caucal, and others), which created an extremely rich landscape of infinite structures with good algorithmic properties.