無限木オートマトン

コンピュータサイエンスと数理論理学において、無限木オートマトンとは、無限木構造を扱う状態機械である。これは、トップダウン有限木オートマトンを無限木に拡張したもの、または無限ワードオートマトンを無限木に拡張したものとみなすことができる。

無限木上で動作する有限オートマトンを最初に使用したのは、マイケル・ラビン^[1]で、2つの後継者を持つモナド2階理論であるS2Sの決定可能性を証明するためでした。さらに、木オートマトンと論理理論は密接に関連しており、論理における決定問題をオートマトンに対する決定問題に還元できることが観察されています。

無限木オートマトン は- ラベル付き木上で動作します。わずかに異なる定義が多数存在しますが、ここでは 1 つを示します。(非決定性)無限木オートマトンは、次のコンポーネントを持つタプルです。 ${\displaystyle \Sigma }$${\displaystyle A=(\Sigma,D,Q,q_{0},\delta,F)}$

• ${\displaystyle \Sigma }$はアルファベットです。このアルファベットは入力ツリーのノードにラベルを付けるために使用されます。
• ${\displaystyle D\subset \mathbb {N} }$は、入力ツリーで許容される分岐度の有限集合です。たとえば、 の場合、入力ツリーはバイナリ ツリーである必要があります。また、 の場合、各ノードには 1、2、または 3 個の子があります。${\displaystyle D=\{2\}}$${\displaystyle D=\{1,2,3\}}$
• ${\displaystyle Q}$は有限の状態集合であり、初期値です。${\displaystyle q_{0}}$
• ${\displaystyle \delta :Q\times \Sigma \times D\rightarrow 2^{Q^{*}}}$は、オートマトンの状態、入力文字、および次数を状態の -組の集合にマッピングする遷移関係です。${\displaystyle q\in Q}$${\displaystyle \sigma \in \Sigma }$${\displaystyle d\in D}$${\displaystyle d}$
• ${\displaystyle F\subseteq Q^{\omega}}$受け入れ条件です。

無限木オートマトンが決定論的であるとは、任意の、 、 に対して、遷移関係に 1 つの -組がちょうど存在する場合です。 ${\displaystyle q\in Q}$${\displaystyle \sigma \in \Sigma }$${\displaystyle d\in D}$${\displaystyle \delta (q,\sigma ,d)}$${\displaystyle d}$

直感的には、入力木に対する木オートマトンの実行は、オートマトン遷移関係を満たす方法で、木ノードにオートマトン状態を割り当てます。もう少し正式には、-ラベル付き木に対する木オートマトンの実行は、次のように-ラベル付き木です。オートマトンが入力木のノードに到達し、現在状態 にあるとします。ノードに のラベルを付け、 をその分岐次数とします。次に、オートマトンがセットからタプルを選択し、自分自身をコピーして処理を進めます。各 について、オートマトンのコピーの 1 つがノード に進み、状態を に変更します。これにより、 -ラベル付き木である実行が生成されます。正式には、入力木に対する 実行は次の 2 つの条件を満たします。${\displaystyle A}$${\displaystyle \Sigma }$${\displaystyle (T,V)}$${\displaystyle Q}$${\displaystyle (T_{r},r)}$${\displaystyle t}$${\displaystyle q}$${\displaystyle t}$${\displaystyle \sigma \in \Sigma }$${\displaystyle d(t)}$${\displaystyle (q_{1},...,q_{d(t)})}$${\displaystyle \delta (q,\sigma ,d(t))}$${\displaystyle d(t)}$${\displaystyle 0<i\leq d(t)}$${\displaystyle ti}$${\displaystyle q_{i}}$${\displaystyle Q}$${\displaystyle (T_{r},r)}$

• ${\displaystyle r(\epsilon )=q_{0}}$。
• となる任意の に対して、 が存在し、任意の に対して、および となる。${\displaystyle t\in T_{r}}$${\displaystyle r(t)=q}$${\displaystyle (q_{1},...,q_{d(t)})\in \delta (q,V(t),d(t))}$${\displaystyle 0<i\leq d(t)}$${\displaystyle ti\in T_{r}}$${\displaystyle r(ti)=q_{i}}$

オートマトンが非決定的である場合、同じ入力ツリーに対して複数の異なる実行が行われる可能性があります。決定的オートマトンの場合、実行は一意です。

実行 では、無限パスは状態のシーケンスによってラベル付けされます。この状態のシーケンスは、状態に関する無限ワードを形成します。これらすべての無限ワードが受理条件 に属する場合、実行 は を受け入れます。興味深い受理条件には、 Büchi、R​​abin、Streett、Muller、およびparity があります。入力ラベル付きツリー に対して、受け入れ実行が存在する場合、入力ツリーはオートマトンによって受け入れられます。受け入れられたすべての ラベル付きツリーの集合はツリー言語と呼ばれ、ツリーオートマトン によって認識されます。 ${\displaystyle (T_{r},r)}$${\displaystyle F}$${\displaystyle \Sigma }$${\displaystyle (T,V)}$${\displaystyle \Sigma }$${\displaystyle {\mathcal {L}}(A)}$${\displaystyle A}$

非決定性 Muller、Rabin、Streett、およびパリティ木オートマトンは同じ木言語の集合を認識するため、同じ表現力を持っています。しかし、非決定性 Büchi 木オートマトンの方が厳密には弱いです。つまり、Rabin 木オートマトンによって認識できる木言語が存在しますが、どの Büchi 木オートマトンでも認識することはできません。^[2]（たとえば、すべてのパスに が有限個しかない - ラベル付き木の集合を認識する Büchi 木オートマトンはありません。たとえば^[3]を参照）。さらに、決定性木オートマトン（Muller、Rabin、Streett、パリティ、Büchi、ループ）は、厳密にはその非決定性版よりも表現力が劣ります。たとえば、ルートの左または右の子が でマークされている二分木の言語を認識する決定性木オートマトンはありません。これは、非決定性Büchi ω-オートマトンが他のオートマトンと同じ表現力を持つ 無限ワード上のオートマトンとは対照的です。${\displaystyle \{a,b\}}$${\displaystyle a}$${\displaystyle a}$

非決定性 Muller/Rabin/Streett/パリティ ツリー オートマトン言語は、和集合、積集合、射影、相補集合に対して閉じています。

• Wolfgang Thomas (1990)。「無限オブジェクト上のオートマトン」。Jan van Leeuwen (編) 著。形式モデルとセマンティクス。理論計算機科学ハンドブック。第 B 巻。Elsevier。pp. 133–191。特に、パート II 「無限木上のオートマトン」、165-185 ページ。
• A. Saoudi および P. Bonizzoni (1992)。「無限ツリー上のオートマトンと合理的制御」。Maurice Nivatおよび Andreas Podelski (編)。ツリーオートマトンと言語。コンピュータサイエンスと人工知能の研究。第 10 巻。アムステルダム: 北ホラント。pp. 189–200。