Büchi presented in [18] a natural acceptance condition allowing nondeterministic finite-state automata to define languages
of infinite words: An automaton accepts an infinite word if there is a run that passes through a final state infinitely often.
Such an automaton is called a Büchi automaton. Complementation of Büchi automata is not obvious.