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