無限木オートマトン
数学的構造

コンピュータサイエンスと数理論理学において、無限木オートマトン（無限木オートマトン）とは、無限木構造を扱う状態機械の一種である。トップダウン型有限木オートマトンを無限木に拡張したもの、あるいは無限語オートマトンを無限木に拡張したものと見ることができる。

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

意味

無限木オートマトン（Infinite Tree Automaton）は-labeled Tree上で動作します。わずかに異なる定義が多数存在しますが、ここではその一つを紹介します。（非決定性）無限木オートマトンとは、以下の要素を持つ タプルです。 Σ {\displaystyle \Sigma } あ ＝ （ Σ 、 D 、 質問 、 q 0 、 δ 、 F ） {\displaystyle A=(\Sigma,D,Q,q_{0},\delta,F)}

  • Σ {\displaystyle \Sigma } はアルファベットです。このアルファベットは入力ツリーのノードにラベルを付けるために使用されます。
  • D ⊂ 北 {\displaystyle D\subset \mathbb {N} } は、入力木において許容される分岐次数の有限集合です。例えば、 の場合、入力木は二分木でなければなりません。また、 の場合、各ノードは1、2、または3個の子を持ちます。 D ＝ { 2 } {\displaystyle D=\{2\}} D ＝ { 1 、 2 、 3 } {\displaystyle D=\{1,2,3\}}
  • 質問 {\displaystyle Q} は有限の状態集合であり、初期状態です。 q 0 {\displaystyle q_{0}}
  • δ : 質問 × Σ × D → 2 質問 ∗ {\displaystyle \delta :Q\times \Sigma \times D\rightarrow 2^{Q^{*}}} は、オートマトンの状態、入力文字、次数を状態の -組のセットにマッピングする遷移関係です。 q ∈ 質問 {\displaystyle q\in Q} σ ∈ Σ {\displaystyle \sigma \in \Sigma } d ∈ D {\displaystyle d\in D} d {\displaystyle d}
  • F ⊆ 質問 ω {\displaystyle F\subseteq Q^{\omega}} 受け入れ条件です。

無限木オートマトンが決定論的であるとは、すべての、、に対して、遷移関係に 1 つの-組が存在する場合です。 q ∈ 質問 {\displaystyle q\in Q} σ ∈ Σ {\displaystyle \sigma \in \Sigma } d ∈ D {\displaystyle d\in D} δ （ q 、 σ 、 d ） {\displaystyle \delta (q,\sigma ,d)} d {\displaystyle d}

走る

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

  • r （ ϵ ） ＝ q 0 {\displaystyle r(\epsilon)=q_{0}} 。
  • となる任意の に対して、 が存在し、任意の に対して、および が成り立ちます。 t ∈ T r {\displaystyle t\in T_{r}} r （ t ） ＝ q {\displaystyle r(t)=q} （ q 1 、 。 。 。 、 q d （ t ） ） ∈ δ （ q 、 V （ t ） 、 d （ t ） ） {\displaystyle (q_{1},...,q_{d(t)})\in \delta (q,V(t),d(t))} 0 < 私 ≤ d （ t ） {\displaystyle 0<i\leq d(t)} t 。 私 ∈ T r {\displaystyle ti\in T_{r}} r （ t 。 私 ） ＝ q 私 {\displaystyle r(ti)=q_{i}}

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

受諾条件

実行 において、無限パスは状態列によってラベル付けされます。この状態列は、状態 上の無限語を形成します。これらの無限語がすべて受理条件 に属する場合、実行は を受理します。興味深い受理条件には、Büchi、R​​abin、Streett、Muller、およびparity があります。入力ラベル付き木 に対して受理実行が存在する場合、入力木はオートマトンによって受理されます。受理されたすべての ラベル付き木の集合は木言語と呼ばれ、木オートマトン によって認識されます。 （ T r 、 r ） {\displaystyle (T_{r},r)} F {\displaystyle F} Σ {\displaystyle \Sigma } （ T 、 V ） {\displaystyle (T,V)} Σ {\displaystyle \Sigma } L （ あ ） {\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 ω-オートマトンが他のオートマトンと同じ表現力を持つ 無限ワード上のオートマトンとは対照的です。 { 1つの 、 b } {\displaystyle \{a,b\}} 1つの {\displaystyle a} 1つの {\displaystyle a}

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

参考文献

  1. ^ ラビン、MO：「無限木上の2次理論とオートマトンの決定可能性」、アメリカ数学会誌、第141巻、1～35頁、1969年。
  2. ^ ラビン、MO：弱定義可能関係と特殊オートマトン、数理論理学と集合論の基礎、pp.1-23、1970年。
  3. ^ Ong, Luke, Automata, Logic and Games (PDF)、p. 92 (定理6.1)

文学

  • 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.
「https://en.wikipedia.org/w/index.php?title=Infinite-tree_automaton&oldid=1283538283」から取得