ラビンオートマトン

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