A Buchi automaton is a regular automaton but reads infinite
words instead of finite words. A word is defined to be in the
language of the automaton iff a run of the automaton on it visits
inifinitly many times in the group of final states (or receiving
states).