ラビンオートマトン（Rabin Automaton）は、無限長の文字列を扱う有限オートマトンの一種。その形式は としたとき、 および は Büchi automaton と同様に定義される。 は遷移関数であり、 はペア の集合で、 である。 である の実行において、 からの一部の状態を無限回訪れる間に からの全状態を有限回訪れるようなインデックス があるとき、 は入力単語 を受容する。
参考文献 Automata on Infinite Objects, Handbook of Theoretical Computer Science (Vol. B), 1991. Wolfgang Thomas による調査 Automata on Infinite Words Paritosh K. Pandya によるチュートリアル
en:Rabin automaton