ラビンオートマトン

ラビンオートマトン（Rabin Automaton）は、無限長の文字列を扱う有限オートマトンの一種。その形式は ${\mathcal {A}}=(Q,~\Sigma ,~q_{0},~\delta ,~\Omega )$ としたとき、 $Q,~q_{0}$ および $\Sigma$ は Büchi automaton と同様に定義される。 $\delta :Q\times \Sigma \rightarrow Q$ は遷移関数であり、 $\Omega$ はペア $(E_{j},~F_{j})$ の集合で、 $E_{j},F_{j}\subset Q$ である。 $\rho \in Q^{\omega }$ である ${\mathcal {A}}$ の実行において、 $F_{i}$ からの一部の状態を無限回訪れる間に $E_{i}$ からの全状態を有限回訪れるようなインデックス $i$ があるとき、 ${\mathcal {A}}$ は入力単語 $\alpha$ を受容する。