Automata Theory and Model Checking ================================== We study automata on infinite words and their applications in system specification and verification. We first introduce B\"uchi automata and survey their closure properties, expressive power, and determinization. We then introduce additional acceptance conditions and the model of alternating automata. We compare the different classes of automata in terms of expressive power and succinctness, and describe decision problems for them. Finally, we describe the automata-theoretic approach to system specification and verification.