ラビンオートマトン(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 によるチュートリアル