Büchi automaton

== English == === Etymology === Named after the Swiss mathematician Julius Richard Büchi, who invented this kind of automaton in 1962. === Noun === Büchi automaton (plural Büchi automatons or Büchi automata) (computing theory) A type of ω-automaton that extends a finite automaton to infinite inputs. It accepts an infinite input sequence if there exists a run of the automaton that visits (at least) one of the final states infinitely often.