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.