Madhavan Mukund
Modern Applications of Automata Theory, Deepak D'Souza and Priti Shankar (eds), World Scientific (2012), 45–78.
This article 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 of finite-state systems.