omega-Automata, like finite automata, are labeled directed graphs, except that an omega-automaton is interpreted as an acceptor of infinite strings rather than finite strings. These automata form an important ingredient in the modern foundations of computer-aided verification and model checking, primarily because they are well suited for reasoning about systems that should, in principle, run for ever.

There is an elegant mathematical theory associated with these objects whose origins date back to at least the early 60's with the work of B"uchi and others. This theory has seen truly explosive growth as a result of the connection to formal verification, but despite all this development there remain a few intriguing unanswered questions about omega-automata, particularly regarding efficient algorithms for manipulating them.

I will survey some pieces of the basic theory of omega-automata, present some cute results related to them, and describe some of the intriguing open questions.