tozima's blog

主に自分のための、論文の読書記録

An Automaton Learning Approach to Solving Safety Games over Infinite Graphs

2016 TACAS

by Daniel Neider and Ufuk Topcu

有限状態オートマトンで表現された (safety) 無限ゲームをオートマトン学習で解くというもの。Winning set を記述するオートマトンを反例駆動で探す。なお本論文で扱っているゲームは通常の意味での games over pushdown graph よりも難しいことに注意。

概要

有限アルファベット \Sigma を固定して、ノード集合が \Sigma^* であるような safety game を考える。Safety game G = (V_0, V_1, E, I, F) はプレイヤー 0 と 1 の頂点 V_0, V_1 （ただし V_0 \cap V_1 = \emptyset）と辺 E \subseteq (V_0 \cup V_1) \times (V_0 \cup V_1) と初期頂点集合 I \subseteq (V_0 \cup V_1) と到達してはいけない頂点集合 F \subseteq (V_0 \cup V_1) で定まる。ゲームが regular であるということを、この論文では、 (V_0 \cup V_1) \subseteq \Sigma^* であって、部分集合 V_0, V_1, I, F がすべて正規言語であって、 E が（有限状態非決定性トランスデューサで表現できるという意味で）正規関係であることをいう。それぞれのオートマトン表現を入力とし、ゲームにプレイヤー 0 が勝てるか否か（そして勝てる場合には winning set）を出力する問題を考える。

本論文の手法は regular な winning set をオートマトン学習で予想するというものである。正規言語 W \subseteq (V_0 \cup V_1) が与えられたときに、それが winning set であるかどうかの判定は容易にできる。Winning set でない場合には、次の４種類の反例のうちいずれかを構成することができる。

  1. I \not\subseteq W であることの証拠となる v \in I \setminus W (positive counterexample)
  2. F \cap W \neq \emptyset であることの証拠となる v \in F \cap W (negative counterexample)
  3. （プレイヤー 0 の次の手の非存在） v \in W \cap V_0 から W 内への辺がないことの証拠である、組 (v, \{ u \mid (v, u) \in E \}) であって v \in V_0 \cap W かつ \{ u \mid (v, u) \in E \} \cap W = \emptyset であるもの (existential implicational counterexample)
  4. （プレイヤー 1 の合法手の考慮不足） W が v \in W \cap V_1 から到達可能な頂点で閉じていないことの証拠である、組 (v, \{ w \mid (v, w) \in E \}) であって v \in V_1 \cap W かつ \{ u \mid (u, w) \in E \} \setminus W \neq \emptyset であるもの (universal implicational counterexample)

winning set の学習は、上記反例を蓄積しつつ、これまでに与えられた反例たちと consistent なオートマトンのうち最小サイズのものを作ることで行われる。最小サイズのオートマトンの構成は propositional SAT への帰着する。具体的には「状態数 N のオートマトンで、これまでに与えられた反例たちと consistent なオートマトンが存在する」ことを表す命題論理式を作り、UNSAT だった場合には N をインクリメントすることを繰り返す。命題論理式は、素朴に「各状態が受理状態か」を表す命題変数 N 個と、「状態 i で記号 a を読んだ時に状態 j に遷移するか」を表す命題変数 N \times |\Sigma| \times N 個を使って自然に表現したものを使う。

私見

まずはゲームの表現力について。まずは下限から。論文では pushdown game などと比べられているが、本論文の "regular game" は通常の意味の "pushdown game" （＝ pushdown automaton の configuration graph 上のゲーム）よりも強いことに注意*1。実際、pushdown automaton の configuration 上の遷移関係 (\gamma, q) \stackrel{a}{\to} (\gamma', q') は regular relation であるので、pushdown automaton の configuration graph は本論文の意味で regular である。あとは一工夫して、スタック \gamma と状態 q と読むべき語 w の３つ組を頂点としたゲームグラフを考えて、初期ノード集合を (初期スタック、初期状態、任意の語) という形の組み合わせすべてとすると、pushdown automaton の受理言語が全体集合 \Sigma^* かという問題を、本論文のゲームに帰着できる。よって特に本論文のゲームは決定不能である*2。

つぎに上限だが、body に ∀ を許した CHC よりは弱いことが容易に分かる。したがって、 \mu-calculus + 文字列データの \mu\nu-fragment に帰着可能でもある。その意味で Beyene et al. POPL14 の game solving で扱っている問題（＝CHC + ∃-head + well-foundedness predicate）よりは、理論的には大幅に簡単である。

設定さえ正しく理解できれば、手法自体は素朴という印象であった。

*1:この点から、先行研究が使っている呼称 reachability games on automatic graphs の方が適切であろう。

*2:決定不能性は論文中でも触れられている。