Madhavan Mukund
Tutorial talk, Sixth National Seminar on Theoretical Computer Science, Banasthali Vidyapith, Banasthali, Rajasthan, August 1996.
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 of finite-state systems.