Finite-State Automata on Infinite Inputs
Madhavan Mukund · Co-Published with Indian Institute of Science (IISc), Bangalore, India eBooks · 2012
This paper is a self-contained introduction to the theory of finite-state automata on infinite words. The study of automata on infinite inputs was initiated by Büchi in order to settle certain decision problems arising in logic. Subsequently, there has been a lot of fundamental work in this area, resulting in a rich and elegant mathematical theory. In recent years, there has been renewed interest in these automata because of the fundamental role they play in the automatic verification Büchi initiated the study of finite-state automata working on infinite inputs in [Bü60]. He was interested in showing that the monadic second order logic of infinite sequences (S1S) was decidable. Büchi discovered a deep and elegant connection between sets of models of formulas in this logic and ω-regular languages, the class of languages over infinite words