ω-オートマトン

理論計算機科学の一分野であるオートマトン理論において、ωオートマトン（またはストリームオートマトン）は、有限の文字列ではなく無限の文字列を入力として実行する有限オートマトンの一種です。ω オートマトンには停止がないため、単に一連の受け入れ状態があるだけでなく、さまざまな受け入れ条件があります。

ω オートマトン は、ハードウェア、オペレーティング システム、制御システムなど、終了することが想定されていないシステムの動作を指定するのに役立ちます。このようなシステムでは、「すべての要求に対して、最終的には確認応答が続く」などのプロパティ、またはその否定である「確認応答が続かない要求がある」などを指定する必要がある場合があります。前者は無限語のプロパティです。有限シーケンスでは、このプロパティを満たすとは言えません。

ω-オートマトンには、それぞれ決定的または非決定的な、ビュッヒ オートマトン、ラビン オートマトン、ストリート オートマトン、パリティ オートマトン、ミュラー オートマトンなどのクラスがあります。これらの ω-オートマトン クラスは、受理条件の点のみが異なります。決定的ビュッヒ オートマトン以外は、すべて正規の ω-言語を正確に認識します。決定的ビュッヒ オートマトンだけは、他のすべてのオートマトンよりも厳密に弱いです。これらのタイプのオートマトンはすべて同じω-言語のセットを認識しますが、特定の ω-言語の表現の簡潔さが異なります。

正式には、決定論的ωオートマトンは次の要素から構成される タプルA  = ( Q ,Σ,δ, Q ₀ , Acc )です。

• Q は有限集合です。 Qの要素はAの状態と呼ばれます。
• Σ はAのアルファベットと呼ばれる有限集合です。
• δ:  Q  × Σ →  Q はAの遷移関数と呼ばれる関数です。
• Q _{0 は}Qの要素であり、初期状態と呼ばれます。
• Acc は受入れ条件であり、正式にはQ ^ωのサブセットです。

Aの入力はアルファベット Σ 上の無限文字列、つまり無限シーケンス α = ( a ₁ , a ₂ , a ₃ ,...) です。このような入力に対するAの実行は、次のように定義される状態の無限シーケンス ρ = ( r ₀ , r ₁ , r ₂ ,...) です。

• r ₀ = q ₀です。
• r ₁ = δ( r ₀ , a ₁ )である。
• r ₂ = δ( r ₁ , a ₂ )である。

...

• つまり、すべてのiについて、r _i = δ( r _{i -1} , a _i )です。

ω-オートマトンの主な目的は、すべての入力のセットのサブセット、つまり受け入れられる入力のセットを定義することです。通常の有限オートマトンの場合、すべての実行は状態r _nで終了し、 r _{n が}受け入れ状態である場合にのみ入力が受け入れられますが、ω-オートマトンの場合、受け入れられる入力のセットの定義はより複雑です。ここでは、実行 ρ 全体を見る必要があります。対応する実行がAccにある場合、入力は受け入れられます。受け入れられる入力 ω ワードのセットは、オートマトンによって認識された ω 言語と呼ばれ、L(A) と表されます。

AccをQ ^ωのサブセットとして定義することは純粋に形式的なものであり、通常そのようなセットは無限であるため、実践には適していません。さまざまな種類の ω オートマトン (Büchi、R​​abin など) の違いは、 Q ^ωの特定のサブセットAcc を有限セットとしてエンコードする方法、したがってどのサブセットにエンコードできるかにあります。

正式には、非決定性ωオートマトンは次の要素から構成される タプルA  = ( Q ,Σ,Δ, Q ₀ , Acc )です。

• Q は有限集合です。 Qの要素はAの状態と呼ばれます。
• Σ はAのアルファベットと呼ばれる有限集合です。
• Δ はQ  × Σ ×  Qのサブセットであり、 Aの遷移関係と呼ばれます。
• Q _{0 は}Qのサブセットであり、初期状態セットと呼ばれます。
• Acc は受け入れ条件であり、 Q ^ωのサブセットです。

遷移関数 δ を持つ決定論的 ω オートマトンとは異なり、非決定論的バージョンには遷移関係 Δ があります。 Δ は、  Q  × Σからべき集合P ( Q ) への関数 : Q  × Σ →  P ( Q ) と見なすことができることに注意してください。 したがって、状態q _nとシンボルa _{n が}与えられた場合、次の状態q _{n +1}は必ずしも一意に決定されるわけではなく、むしろ次の状態の集合が存在します。

入力 α = ( a ₁ , a ₂ , a _{3 ,...) に対する}Aの実行は、次の条件を満たす状態の 無限シーケンス ρ = ( r ₀ , r ₁ , r _{2 ,...) です。}

• r _{0 は}Q ₀の要素です。
• r _{1 はΔ(} r ₀ , a ₁ )の要素である。
• r _{2 はΔ(} r ₁ , a ₂ )の要素である。

...

• つまり、すべての_i : r i_はΔ( r _{i -1} , ai )の要素です。

非決定性 ω-オートマトンでは、与えられた入力に対して多くの異なる実行が許可されるか、まったく許可されない場合があります。 実行可能な実行のうち少なくとも 1 つが受け入れ可能であれば、入力は受け入れられます。 実行が受け入れ可能かどうかは、決定性 ω-オートマトンの場合と同様に、 Accのみに依存します。 Δ を δ のグラフと見なすことで、すべての決定性 ω-オートマトンを非決定性 ω-オートマトンと見なすことができます。 決定性 ω-オートマトンの実行と受け入れの定義は、非決定性の場合の特殊なケースです。

受容条件は、ω ワードの無限集合である可能性があります。ただし、ほとんどの場合、有限に表現可能な受容条件が研究されています。以下に、さまざまな一般的な受容条件を示します。

リストについて説明する前に、次の点に留意しましょう。無限に実行されるシステムの場合、特定の動作が無限に繰り返されるかどうかが関心の対象になることがよくあります。たとえば、ネットワーク カードが無限に多くの ping 要求を受信した場合、一部の要求には応答できない可能性がありますが、受信した ping 要求の無限のサブセットには応答する必要があります。このことから、次の定義が生まれます。任意の実行 ρ について、Inf(ρ) を ρ で無限に発生する状態の集合とします。特定の状態が無限に頻繁に訪れるというこの概念は、次の受け入れ条件を定義するのに役立ちます。

• Büchiオートマトンとは、 Qの何らかのサブセットFに対して次の受理条件を使用するω-オートマトンAです。

ビュッヒ条件

Aは、Inf(ρ) ∩Fが空ではない実行ρを正確に受け入れます 。つまり、ρには無限に発生する受け入れ状態が存在します。

• あラビンオートマトンとは、状態集合の_{ペア(B i}、G _i )の集合Ωに対して、以下の受入れ条件を使用するωオートマトンA

ラビン条件

Aは、Ω内にペア(B _i ,G _{i )が存在し、B i}  ∩ Inf(ρ)が空であり、G _i  ∩ Inf(ρ)が空ではないような実行ρだけを受け入れます。

• ストリートオートマトンとは、状態集合のペア(B _i、G _i )の集合Ωに対して、次の受理条件を使用するωオートマトンAである。

ストリートコンディション

Aは、Ω内のすべてのペア(B _i、G _i )について、B _i  ∩ Inf(ρ)が空であるか、G _i ∩ Inf(ρ)が空ではないような実行ρを正確に 受け入れます。

• パリティオートマトンとは、ある自然数 kに対して状態集合がQ  = {0,1,2,..., k } であるオートマトンAであり、次の受理条件を満たすものです。

パリティ条件

Aは、Inf(ρ)の最小の数が偶数である場合にのみρを受け入れます。

• ミュラーオートマトンとは、 P ( Q )( Qの冪集合)のサブセットFに対して、次の受理条件を使用するωオートマトンAである。

ミュラー条件

Aは、Inf(ρ)がFの要素となる実行ρだけを受け入れます 。

すべての Büchi オートマトンを Muller オートマトンと見なすことができます。 Fを、 Fの少なくとも 1 つの要素を含む Qのすべてのサブセットで構成されるF 'に置き換えるだけで十分です。同様に、すべての Rabin、Streett、またはパリティ オートマトンも Muller オートマトンと見なすことができます。

アルファベット Σ = {0,1} 上の 次の ω 言語Lは、非決定性 Büchi オートマトンによって認識できます。Lは、1 が有限回しか出現しない Σ ^ωのすべての ω ワードで構成されます。Lを認識する非決定性 Büchi オートマトンには、q ₀ (初期状態) とq _{1 の}2 つの状態のみが必要です。Δ は、3 つの組 ( q ₀ ,0, q ₀ )、 ( q ₀ ,1, q ₀ )、 ( q ₀ ,0, q ₁ )、および ( q ₁ ,0, q ₁ ) で構成されます。F  = { q _{1 }} 。1が有限回しか出現しない任意の入力 α に対して、読み取る 1 がある限り状態q _{0に留まり、その後状態}q ₁に移行する実行が存在します。この実行は成功です。 1 が無限にある場合、実行できるのは 1 つだけです。つまり、常に状態q ₀に留まる実行です。(マシンがq _{0を離れて}q ₁に到達すると、戻ることはできません。別の 1 が読み取られた場合、後続の状態はありません。)

上記の言語は、非決定的なオートマトンよりも 表現力が劣る決定的なBüchi オートマトンでは認識できないことに注意してください。

^{有限アルファベット Σ 上の ω 言語は、 Σ 上の ω 単語の集合、つまり Σ ω}のサブセットです。 Σ 上の ω 言語は、それがAによって受け入れられるすべての ω 単語の集合である場合、 ω オートマトンA (同じアルファベットを持つ)によって認識されると言われます。 ω オートマトンクラスの表現力は、クラス内の一部のオートマトンによって認識できるすべての ω 言語のクラスによって測定されます。

非決定性ビュッヒ、パリティ、ラビン、ストリート、ミュラーのオートマトンはすべて、まったく同じクラスのω-言語を認識します。^[1] これらは、正規言語のω-クリーネ閉包、または正規ω-言語として知られています。異なる証明を使用して、決定性パリティ、ラビン、ストリート、ミュラーのオートマトンがすべて正規ω-言語を認識することも示されます。このことから、正規ω-言語のクラスは補集合に対して閉じていることがわかります。ただし、上記の例は、決定性ビュッヒオートマトンのクラスが厳密に弱いことを示しています。

非決定性 Muller、Rabin、Streett、パリティ、Büchi オートマトンは同じ表現力を持っているため、相互に翻訳できます。次の略語を使用します。たとえば、NB は非決定性 Büchi ω オートマトンを表し、DP は決定性パリティ ω オートマトンを表します。次の式が成り立ちます。 ${\displaystyle \{N,D\}\times \{M,R,S,P,B\}}$

• 明らかに、任意の決定論的オートマトンを非決定論的オートマトンとして見ることができます。
• ${\displaystyle NB\rightarrow NR/NS/NP}$状態空間での爆発はありません。
• ${\displaystyle NR\rightarrow NB}$状態空間における多項式爆発、すなわち結果として得られるNBの状態数は であり、ここで はNBの状態数、 はラビン受容対の数である（例えば、^{[2] を}参照）。${\displaystyle 2nm+1}$${\displaystyle n}$${\displaystyle m}$
• ${\displaystyle NS/NM/NP\rightarrow NB}$状態空間で指数関数的に増加します。
• ${\displaystyle NB\rightarrow DR/DP}$状態空間で指数関数的に爆発する。この決定論的結果にはサフラの構成が使われている。

翻訳の包括的な概要は、参照されたウェブソースで見つけることができます。^[3]

ω-オートマトンを使用して、後継者の下での自然数の モナド2階(MSO)理論であるS1Sの決定可能性を証明することができます。無限木オートマトンでは、ω-オートマトンを無限木に拡張し、2つの後継者を持つMSO理論であるS2Sの決定可能性を証明するために使用できます。また、これは、制限された(固定された制限が与えられた)木幅を持つグラフのMSO理論に拡張できます。

• Farwer、Berndt (2002)、「ω-Automata」、Grädel、Erich。トーマス、ヴォルフガング。 Wilke, Thomas (編)、『Automata, Logics, and Infinite Games』、Lecture Notes in Computer Science、Springer、pp.  3–21、ISBN 978-3-540-00388-5。
• ペラン、ドミニク、ピン、ジャン=エリック (2004)、Infinite Words: Automata, Semigroups, Logic and Games、エルゼビア、ISBN 978-0-12-532111-2
• Thomas, Wolfgang (1990)、「無限オブジェクト上のオートマトン」、van Leeuwen, Jan (編)、理論計算機科学ハンドブック、第 B 巻、MIT 出版、pp.  133– 191、ISBN 978-0-262-22039-2
• Bakhadyr Khoussainov、Anil Nerode ( 2012年 12 月 6 日)。オートマトン理論とその応用。Springer Science & Business Media。ISBN 978-1-4612-0171-7。