Bell Labs, Murray Hill, NJ
omega-Automata
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.