About: ラビンオートマトン

ラビンオートマトン（Rabin Automaton）は、無限長の文字列を扱う有限オートマトンの一種。その形式は としたとき、 および は Büchi automaton と同様に定義される。 は遷移関数であり、 はペア の集合で、 である。 である の実行において、 からの一部の状態を無限回訪れる間に からの全状態を有限回訪れるようなインデックス があるとき、 は入力単語 を受容する。