ビュヒ・オートマトン

決定性ビューチオートマトンというクラスは、すべてのオメガ正則言語を包含するには不十分である。特に、言語を認識する決定性ビューチオートマトンはない。${\displaystyle (0\cup 1)^{*}0^{\omega }}$⁠ は、1 が有限回しか出現しない単語を正確に含んでいます。このような決定性ビューチオートマトンが存在しないことは、背理法によって証明できます。${\textstyle A}$は、 を認識する決定性ビューチオートマトンです。${\displaystyle (0\cup 1)^{*}0^{\omega }}$最終状態が設定されました${\textstyle \mathbf {F} }$。${\textstyle A}$受け入れる${\textstyle 0^{\omega }}$。 それで、${\textstyle A}$州を訪れる予定${\textstyle \mathbf {F} }$有限接頭辞を読んだ後${\textstyle 0^{\omega }}$の後に言う${\textstyle i_{0}}$th 文字。${\textstyle A}$ωワードも受け入れる${\textstyle 0^{i_{0}}10^{\omega }}$したがって、一部の人にとって${\textstyle i_{1}}$接頭辞の後${\textstyle 0^{i_{0}}10^{i_{1}}}$オートマタはいくつかの州を訪れる${\textstyle \mathbf {F} }$この構成を続けると、ωワードは${\textstyle 0^{i_{0}}10^{i_{1}}10^{i_{2}}\dots }$生成されると、${\textstyle A}$州を訪れる${\textstyle \mathbf {F} }$無限に頻繁に、そしてその言葉は⁠にはない${\displaystyle (0\cup 1)^{*}0^{\omega }.}$矛盾。

決定性ビューチオートマトンによって認識可能な言語のクラスは、次の補題によって特徴付けられる。

補題：ω言語は、ある正規言語の極限言語である場合に、決定性ビューチオートマトンによって認識可能である。

証明：任意の決定性ビューチオートマトン${\textstyle A}$決定性有限オートマトンと見なすことができる${\textstyle A'}$またその逆も同様で、どちらのタイプのオートマトンも同じコンポーネントの5タプルとして定義されているため、受理条件の解釈だけが異なります。${\textstyle L(A)}$は制限言語です${\textstyle L(A')}$ωワードは、${\textstyle A}$強制するなら${\textstyle A}$最終状態を無限回訪問する。したがって、このωワードの無限個の有限接頭辞は、${\textstyle A'}$したがって、${\textstyle L(A)}$は制限言語です${\textstyle L(A')}$。

受理条件における複数の状態集合は、オートマトン構成によって1つの状態集合に変換することができ、これは「計数構成」として知られています。${\textstyle A=(Q,\Sigma ,\Delta ,q_{0},\{F_{1},\ldots ,F_{n}\})}$GBAでは、${\textstyle F_{1},\ldots ,F_{n}}$が受理状態の集合である場合、等価なビューチオートマトンは次のようになります。${\textstyle A'=(Q',\Sigma ,\Delta ',q'_{0},F')}$、 どこ

• ${\textstyle Q'=Q\times \{1,\ldots ,n\}}$
• ${\textstyle q'_{0}=(q_{0},1)}$
• ${\textstyle \Delta '=\{((q,i),a,(q',j))\mid (q,a,q')\in \Delta {\text{ and if }}q\in F_{i}{\text{ then }}j=((i+1){\bmod {n}}){\text{ else }}j=i\}}$
• ${\textstyle F'=F_{1}\times \{1\}}$

線形時相論理式から一般化ビューチオートマトンへの変換をここに示します。また、一般化ビューチオートマトンからビューチオートマトンへの変換は上記に示しました。

与えられたミュラーオートマトンを、以下のオートマトン構成によって等価なビューヒオートマトンに変換することができる。${\textstyle A=(Q,\Sigma ,\Delta ,Q_{0},\{F_{0},\ldots ,F_{n}\})}$はミュラーオートマトンであり、${\textstyle F_{0},\ldots ,F_{n}}$は受理状態の集合である。同等のビューチオートマトンは次の通りである。${\textstyle A'=(Q',\Sigma ,\Delta ',Q_{0},F')}$、 どこ

• ${\textstyle Q'=Q\cup \bigcup _{i=0}^{n}\{i\}\times F_{i}\times 2^{F_{i}}}$
• ${\textstyle \Delta '=\Delta \cup \Delta _{1}\cup \Delta _{2}}$、 どこ
  • ${\textstyle \Delta _{1}=\{(q,a,(i,q',\emptyset ))\mid (q,a,q')\in \Delta {\text{ and }}q'\in F_{i}\}}$
  • ${\textstyle \Delta _{2}=\{((i,q,R),a,(i,q',R'))\mid (q,a,q')\in \Delta {\text{ and }}q,q'\in F_{i}{\text{ and if }}R=F_{i}{\text{ then }}R'=\emptyset {\text{ otherwise }}R'=R\cup \{q\}\}}$
• ${\textstyle F'=\bigcup _{i=0}^{n}\{i\}\times F_{i}\times \{F_{i}\}}$

${\textstyle A'}$元の状態セットを保持します${\textstyle A}$そしてそれらにさらに状態を追加する。ビューヒオートマトン${\textstyle A'}$ミュラーオートマトンをシミュレートする${\textstyle A}$以下のように：入力ワードの開始時に、${\textstyle A'}$実行に続く${\textstyle A}$初期状態は同じで、${\textstyle \Delta '}$含まれる${\textstyle \Delta }$入力単語内の非決定論的に選択された位置で、${\textstyle A'}$遷移によって新たに追加された状態へジャンプすることを決定する${\textstyle \Delta _{1}}$。次に、${\textstyle \Delta _{2}}$すべての州を訪れてみてください${\textstyle F_{i}}$そして成長し続ける${\textstyle R}$。 一度${\textstyle R}$等しくなる${\textstyle F_{i}}$すると空集合にリセットされ、${\textstyle \Delta _{2}}$すべての州を訪れてみてください${\textstyle F_{i}}$何度も何度も州が。だから、もし州が${\textstyle R=F_{i}}$無限に頻繁に訪問される${\textstyle A'}$対応する入力を受け入れ、${\textstyle A}$この構成は、マクノートンの定理の証明の最初の部分とよく似ています。

与えられたクリプキ構造は次のように定義される。${\textstyle M=\langle Q,I,R,L,AP\rangle }$どこ${\textstyle Q}$は状態の集合であり、${\textstyle I}$は初期状態の集合であり、${\textstyle R}$は、2 つの状態間の関係であり、エッジとしても解釈されます。${\textstyle L}$は州のラベルであり、${\textstyle AP}$は、原子命題の集合であり、${\textstyle L}$。

ビュヒ・オートマトンは以下の特徴を持つ。

${\displaystyle Q_{\text{final}}=Q\cup \{{\text{init}}\}}$

${\displaystyle \Sigma =2^{AP}}$

${\displaystyle I=\{{\text{init}}\}}$

${\displaystyle F=Q\cup \{{\text{init}}\}}$

${\displaystyle \delta =q{\overrightarrow {a}}p}$もし${\textstyle (q,p)}$に属する${\textstyle R}$そして${\textstyle L(p)=a}$

そして${\textstyle {\text{init}}{\overrightarrow {a}}q}$もし${\textstyle q}$に属する${\textstyle I}$そして${\textstyle L(q)=a}$。

ただし、クリプキ構造とビューチオートマトンでは解釈に違いがあることに注意が必要です。前者は各状態におけるすべての状態変数の極性を明示的に指定するのに対し、後者は現在の変数セットが真であるか偽であるかを宣言するだけです。モデルに存在する可能性のある他の変数については何も言及しません。

Büchiは^{[ 1 ]}で、論理形式で二重指数補数構成法を提示した。ここでは、オートマトン理論で用いられる現代的な記法で彼の構成法を示す。${\textstyle A=(Q,\Sigma ,\Delta ,Q_{0},\mathbf {F} )}$をビューチオートマトンとする。${\textstyle \sim _{A}}$要素間の同値関係である${\textstyle \Sigma ^{+}}$各${\textstyle v,w\in \Sigma ^{+}}$、 ${\textstyle v\sim _{A}w}$すべての${\textstyle p,q\in Q}$、 ${\textstyle A}$走る${\textstyle p}$に${\textstyle q}$以上${\textstyle v}$これは以下の場合に限り可能です${\textstyle w}$ さらに ${\textstyle A}$ランニング${\textstyle \mathbf {F} }$から${\textstyle p}$に${\textstyle q}$以上${\textstyle v}$これは以下の場合に限り可能です${\textstyle w}$各クラスの${\textstyle \sim _{A}}$マップを定義します${\textstyle f\colon Q\to 2^{Q}\times 2^{Q}}$ 次のようにして：各状態について${\textstyle p\in Q}$、 我々は持っています${\textstyle (Q_{1},Q_{2})=f(p)}$、 どこ ${\textstyle Q_{1}=\{q\in Q\mid w{\text{ can move automaton }}A{\text{ from }}p{\text{ to }}q\}}$そして${\textstyle Q_{2}=\{q\in Q\mid w{\text{ can move automaton }}A{\text{ from }}p{\text{ to }}q{\text{ via a state in }}\mathbf {F} \}}$。 ご了承ください${\textstyle Q_{2}\subseteq Q_{1}}$。 もし${\textstyle f}$この方法で定義可能なマップである場合、定義する（一意の）クラスを表記します。${\textstyle f}$による${\textstyle L_{f}}$。

以下の３つの定理は、補集合の構成を提供する。${\textstyle A}$同値類を 使用して${\textstyle \sim _{A}}$。

定理１：${\textstyle \sim _{A}}$有限個の同値クラスがあり、各クラスは正規言語である。 証明: 有限個の同値クラスがあり、各クラスは正規言語である。${\textstyle f\colon Q\to 2^{Q}\times 2^{Q}}$関係${\textstyle \sim _{A}}$有限個の同値類を持つ。次に、${\textstyle L_{f}}$は正規言語です。${\textstyle p,q\in Q}$そして${\textstyle i\in \{0,1\}}$、 させて${\textstyle A_{i,p,q}=(\{0,1\}\times Q,\;\Sigma ,\;\Delta _{1}\cup \Delta _{2},\;\{(0,p)\},\;\{(i,q)\})}$非決定性有限オートマトン である。 ${\textstyle \Delta _{1}=\{((0,q_{1}),(0,q_{2}))\mid (q_{1},q_{2})\in \Delta \}\cup \{((1,q_{1}),(1,q_{2}))\mid (q_{1},q_{2})\in \Delta \}}$、 そして ${\textstyle \Delta _{2}=\{((0,q_{1}),(1,q_{2}))\mid q_{1}\in \mathbf {F} \land (q_{1},q_{2})\in \Delta \}}$。 させて${\textstyle Q'\subseteq Q}$。 させて${\textstyle \alpha _{p,Q'}=\bigcap \{L(A_{1,p,q})\mid q\in Q'\}}$これは移動可能な単語のセットです${\textstyle A}$から${\textstyle p}$すべての州へ${\textstyle Q'}$ ある州を通じて${\textstyle \mathbf {F} }$。 させて${\textstyle \beta _{p,Q'}=\bigcap \{L(A_{0,p,q})-L(A_{1,p,q})-\{\varepsilon \}\mid q\in Q'\}}$これは、移動可能な空でない単語の集合です。${\textstyle A}$から${\textstyle p}$すべての州へ${\textstyle Q'}$ また、どの州も通過しない実行はありません。${\textstyle \mathbf {F} }$。 させて${\textstyle \gamma _{p,Q'}=\bigcap \{\Sigma ^{+}-L(A_{0,p,q})\mid q\in Q'\}}$これは、移動できない空でない単語の集合です。${\textstyle A}$から${\textstyle p}$いずれかの州へ${\textstyle Q'}$正規言語は有限の共通部分と相対補元に関して閉じているので、${\textstyle \alpha _{p,Q'}}$、${\textstyle \beta _{p,Q'}}$、 そして${\textstyle \gamma _{p,Q'}}$は規則的です。定義により、 ${\textstyle L_{f}=\bigcap \{\alpha _{p,Q_{2}}\cap \beta _{p,Q_{1}-Q_{2}}\cap \gamma _{p,Q-Q_{1}}\mid (Q_{1},Q_{2})=f(p)\land p\in Q\}}$。

定理2：各${\textstyle w\in \Sigma ^{\omega }}$、 がある${\textstyle \sim _{A}}$クラス${\textstyle L_{f}}$そして${\textstyle L_{g}}$そのため ${\textstyle w\in L_{f}(L_{g})^{\omega }}$証明：この 定理を証明するために無限ラムゼーの定理 を用います。${\textstyle w=a_{0}a_{1}\ldots }$そして${\textstyle w(i,j)=a_{i}\ldots a_{j-1}}$自然数の集合を考えてみましょう。${\textstyle \mathbb {N} }$の同値類を${\textstyle \sim _{A}}$部分集合の色である${\textstyle \mathbb {N} }$ サイズ2。色は次のように割り当てます。${\textstyle i<j}$色を${\textstyle \{i,j\}}$は、${\textstyle w(i,j)}$無限ラムゼー定理により、無限集合を見つけることができます。${\textstyle X\subseteq \mathbb {N} }$ 各部分集合が${\textstyle X}$サイズ2のものは、同じ色です。${\textstyle 0<i_{0}<i_{1}<i_{2}\ldots \in X}$。 させて${\textstyle f}$同値類の定義マップであり、 ${\textstyle w(0,i_{0})\in L_{f}}$。 させて${\textstyle g}$各に対して、同値類の定義マップである。${\textstyle j>0}$、${\textstyle w(i_{j-1},i_{j})\in L_{g}}$。 それから${\textstyle w\in L_{f}(L_{g})^{\omega }}$。

定理3：${\textstyle L_{f}}$そして${\textstyle L_{g}}$同値類である${\textstyle \sim _{A}}$。 それから${\textstyle L_{f}(L_{g})^{\omega }}$は、${\textstyle L(A)}$または、${\textstyle L(A)}$証明：単語 があると仮定します${\textstyle w\in L(A)\cap L_{f}(L_{g})^{\omega }}$そうでなければ、定理は自明に成り立つ。${\textstyle r}$受け入れる連続${\textstyle A}$入力オーバー${\textstyle w}$各単語が${\textstyle w'\in L_{f}(L_{g})^{\omega }}$ も${\textstyle L(A)}$つまり、ランが存在する${\textstyle r'}$の${\textstyle A}$入力オーバー${\textstyle w'}$状態${\textstyle \mathbf {F} }$発生する${\textstyle r'}$無限に頻繁に。${\textstyle w\in L_{f}(L_{g})^{\omega }}$、 させて${\textstyle w_{0}w_{1}w_{2}\ldots =w}$そのため${\textstyle w_{0}\in L_{f}}$そしてそれぞれについて${\textstyle i>0}$、${\textstyle w_{i}\in L_{g}}$。 させて${\textstyle s_{i}}$州になる${\textstyle r}$摂取後${\textstyle w_{0}\ldots w_{i}}$。 させて${\textstyle I}$インデックスの集合は、${\textstyle i\in I}$実行セグメントが${\textstyle r}$ から${\textstyle s_{i}}$に${\textstyle s_{i+1}}$状態を含む${\textstyle \mathbf {F} }$。 ${\textstyle I}$無限集合でなければならない。同様に、単語を分割することができる。${\textstyle w'}$。 させて${\textstyle w'_{0}w'_{1}w'_{2}\ldots =w'}$そのため${\textstyle w'_{0}\in L_{f}}$そしてそれぞれについて${\textstyle i>0}$、${\textstyle w'_{i}\in L_{g}}$. 私たちは構築します${\textstyle r'}$帰納的に次のようにする。${\textstyle r'}$同じである${\textstyle r}$定義によれば${\textstyle L_{f}}$単語のランセグメントを選択できます${\textstyle w'_{0}}$到達するために${\textstyle s_{0}}$帰納法の仮説により、${\textstyle w'_{0}\ldots w'_{i}}$到達する${\textstyle s_{i}}$定義によれば${\textstyle L_{g}}$単語セグメントに沿ってランを拡張できます${\textstyle w'_{i+1}}$拡張が到達する${\textstyle s_{i+1}}$そして州を訪れる${\textstyle \mathbf {F} }$もし${\textstyle i\in I}$.${\textstyle r'}$このプロセスから得られるものは、状態を含む無限に多くの実行セグメントを持つことになる。${\textstyle \mathbf {F} }$、 以来${\textstyle I}$無限である。したがって、${\textstyle r'}$受け入れるランニングであり、${\textstyle w'\in L(A)}$。

上記の定理により、${\textstyle \Sigma ^{\omega }-L(A)}$形式のω正則言語 の有限和として${\textstyle L_{f}(L_{g})^{\omega }}$、 どこ${\textstyle L_{f}}$そして${\textstyle L_{g}}$は同値類である${\textstyle \sim _{A}}$。 したがって、${\textstyle \Sigma ^{\omega }-L(A)}$はω正則言語です。この言語をビューチオートマトンに変換できます。この構成は、サイズに関して二重指数関数的です。${\textstyle A}$。