パリティゲーム

パリティゲーム (parity games) は彩色された有向グラフ上でプレイされる理論上のゲームである。各ノードは優先度と呼ばれる(通常は有限種類の)自然数で彩色されている。このゲームはプレイヤー0とプレイヤー1の二名によってプレイされる。各プレイヤーは、ゲーム上に一個だけある駒をグラフの辺にそって動かす。手番は、その駒の現在地によって決められている。この操作を繰り返し(場合によっては無限回)行うことにより、プレイと呼ばれるパスが定まる。

有限長のプレイの場合、駒を動かせなくなったプレイヤーが敗者で、敗者でない側が勝者となる。無限長のプレイの勝者は、プレイ中に現れる優先度の値によって決定される。プレイ中に無限回現れた優先度のうち、最大の値が偶数ならばプレイヤー0の勝利、奇数ならばプレイヤー1の勝利となる。(偶奇が逆だったり、最大値のかわりに最小値を使う場合もある。) この偶奇性が「パリティ」の由来であろう。

パリティゲームはボレル階層の3層目に属する。したがってパリティゲームは決定的である。^[1]

n後者演算に関する二階の理論の決定可能性に関するラビンの証明では、パリティゲームに類似のゲームが暗黙的に使われ、該当ゲームの決定性も証明されている。^[2] ナスター-タルスキの定理を使えば、パリティゲームの決定性に対するより単純な証明を与えることもできる。^[3]

さらに、パリティゲームは履歴なしの決定性 (history-free determinacy, memoryless determinacy) をもつ。^[4]^[5] これは、あるパリティーゲームの初期位置で、どちらかのプレイヤーが必勝戦略を持つとき、履歴なしの必勝戦略、すなわち今までの駒の動きに関係なく、現在位置だけで次の行き先を決めるような戦略、が存在するというものである。

解法

計算機科学の未解決問題
パリティゲームは多項式時間で解けるか？

有限グラフ上のパリティゲームを解くとは、与えられた初期位置に対して、二人のプレイヤーのうちどちらが必勝戦略を持つか決定することである。この問題はNPかつCo-NP (より強く、UPかつco-UP) であることがわかっている。^[6] また、QP (準多項式時間) であることもわかっている^[7] この問題が多項式時間で解けるかどうかは未解決問題である。

パリティゲームが履歴なしの決定性を持っているため、パリティゲームを解く問題は次のような単純げなグラフ理論の問題と同値である: n頂点の有限有向2部グラフ $V=V_{0}\cup V_{1}$ までの自然数で彩色されたものが与えられる。このとき、 $V_{0}$ の頂点ごとにその頂点から出る辺を一つずつ選び、残りの出向辺を削除することで、得られた部分グラフの任意の閉路の最大優先度が偶数となるようにできるか？

パリティゲームを解く再帰的なアルゴリズム

パリティゲームを解くための再帰的なアルゴリズムが、Zielonkaにより説明されている。 $G=(V,V_{0},V_{1},E,\Omega )$ をパリティゲームとする。ここで、 $V_{0}$ と $V_{1}$ はそれぞれプレイヤー0とプレイヤー1の手番になるノードの集合、 $V=V_{0}\cup V_{1}$ はノード全体の集合、 $E\subseteq V\times V$ は辺の集合、 $\Omega :V\rightarrow \mathbb {N}$ は優先度を割り当てる関数とする。 Eはtotalであるとする。つまり、どのノードからも1本以上の辺が出ていると仮定する。

Zielonkaのアルゴリズムはアトラクタの概念に基づいている。 $U\subseteq V$ をノードの集合とし、 $i=0,1$ をプレイヤーの番号とする。Uのi-アトラクタ $Attr_{i}(U)$ とは、プレイヤー(1-i)の選択にかかわらず有限回でUに到達するようプレイヤーiが誘導できるようなノードの集合である。これは以下のような不動点計算により定義できる:

{\begin{aligned}Attr_{i}(U)^{0}&:=U\\Attr_{i}(U)^{j+1}&:=Attr_{i}(U)^{j}\cup \{v\in V_{i}\mid \exists (v,w)\in E:w\in Attr_{i}(U)^{j}\}\cup \{v\in V_{1-i}\mid \forall (v,w)\in E:w\in Attr_{i}(U)^{j}\}\\Attr_{i}(U)&:=\bigcup _{j=0}^{\infty }Attr_{i}(U)^{j}\end{aligned}}

別の言い方をすれば、初期集合 U から開始して、「プレイヤー0の手番となるノードで、 U に一歩で到達できるノード」と「プレイヤー1の手番となるノードで、プレイヤー1がどのように選択しても U に入ってしまうノード」をUに追加していく。これを繰り返して止まったときのUがAttr0(U)である。

Zielonkaのアルゴリズムは、優先度の値に関する再帰降下に基づいている。最大優先度が0のときは、どんな戦略であってもプレイヤー0が勝つのは明らかである。それ以外のときは、 p を最大優先度とし、 $i=p{\bmod {2}}$ をその優先度に紐付けられたプレイヤーの番号とする。また、 $U=\{v\mid \Omega (v)=p\}$ を優先度が p であるようなノード全体の集合、 $A=Attr_{i}(U)$ をプレイヤー i のアトラクタとおく。このとき、プレイヤー i はうまく戦略を選ぶことで、 A を無限回訪問するようなプレイでは必ずプレイヤー i が勝つようにできる。

$G'=G\setminus A$ を考える。このゲーム $G'$ は元のゲームより真に小さいから再帰的に解くことができ、それにより各プレイヤーの勝利領域 $W'_{i},W'_{1-i}$ がわかる。ここでもし $W'_{1-i}$ が空ならば、元のゲームGの対応する勝利領域 $W_{1-i}$ も空である。なぜならば、プレイヤー $1-i$ が $W_{i}$ から抜ける唯一の方法は A に行くことで、この場合もプレイヤー i の勝利が確定するからである。

いっぽう、もし $W'_{1-i}$ が空ではなかった場合、プレイヤー $1-i$ は少なくとも $W'_{1-i}$ では勝利することができる。なぜならば、プレイヤー i が $W'_{1-i}$ から A に逃げることはできない (さもなくば A がアトラクタであることに反する) からである。しかしそれ以外のノードでの必勝性は明らかではないので、プレイヤー $1-i$ のアトラクタ $B=Attr_{1-i}(W'_{1-i})$ を計算し、これを G から取り除いた、より小さいゲーム $G''=G\setminus B$ を得る。するとやはりこのゲームの必勝性を再帰的に解くことができ、各プレイヤーの勝利領域 $W''_{i},W''_{1-i}$ がわかる。このとき $W_{i}=W''_{i}$ かつ $W_{1-i}=W''_{1-i}\cup B$ であることがわかる。

このアルゴリズムは、擬似コードでは以下のように書ける:

 function  $solve(G)$ 
     p := G の最大優先度
     if  $p=0$ 
         return  $W_{0},W_{1}:=V,\{\}$ 
     else
         U :=  G のノードで優先度 p のもの全体
          $i:=p{\bmod {2}}$ 
          $A:=Attr_{i}(U)$ 
          $W_{0}',W_{1}':=solve(G\setminus A)$ 
         if  $W_{i}'=V$ 
              return  $W_{i},W_{1-i}:=V,\{\}$ 
          $B:=Attr_{1-i}(W_{1-i}')$ 
          $W_{0}'',W_{1}'':=solve(G\setminus B)$ 
         return  $W_{i},W_{1-i}:=W_{i}'',W_{1-i}''\cup B$

論理学やオートマトン理論との関係

パリティゲームは計算複雑性理論の観点からも興味深い一方、パリティゲーム問題を自動検証やコントローラ合成などのバックエンドと位置付けることもできる。たとえば、様相μ計算に対するモデル検査問題はパリティゲーム問題と同値であることが知られている。様相論理式の妥当性や充足可能性などを決定する問題もまた、パリティゲームに帰着することができる。

参考文献

^ D. A. Martin: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363–371 (1975)
^ Rabin, MO (1969). “Decidability of second-order theories and automata on infinite trees”. Transactions of the American Mathematical Society (American Mathematical Society) 141: 1–35. doi:10.2307/1995086. JSTOR 1995086.
^ E. A. Emerson and C. S. Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991), ISBN 0-8186-2445-0
^ A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)
^ Zielonka, W (1998). “Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees”. Theor. Comput. Sci. 200 (1–2): 135–183. doi:10.1016/S0304-3975(98)00009-7.
^ Marcin Jurdziński (1998), “Deciding the winner in parity games is in UP∩ co-UP”, Information Processing Letters (Elsevier) 68 (3): 119-124
^ Calude, Cristian S and Jain, Sanjay and Khoussainov, Bakhadyr and Li, Wei and Stephan, Frank, “Deciding parity games in quasipolynomial time”, STOC 2017

Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, Scott Weinstein (2007). Finite model theory and its applications. Springer. ISBN 978-3-540-00428-8

読書案内

E. Grädel, W. Thomas, T. Wilke (Eds.) : Automata, Logics, and Infinite Games, Springer LNCS 2500 (2003), ISBN 3-540-00388-6
W. Zielonka : Infinite games on finitely coloured graphs with applications to automata on infinite tree, TCS, 200(1-2):135-183, 1998

外部リンク

パリティゲームのソルバー:

PGSolver Collection

[1] D. A. Martin: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363–371 (1975)

[2] Rabin, MO (1969). “Decidability of second-order theories and automata on infinite trees”. Transactions of the American Mathematical Society (American Mathematical Society) 141: 1–35. doi:10.2307/1995086. JSTOR 1995086.

[EJ-3] E. A. Emerson and C. S. Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991), ISBN 0-8186-2445-0

[4] A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)

[ZL-5] Zielonka, W (1998). “Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees”. Theor. Comput. Sci. 200 (1–2): 135–183. doi:10.1016/S0304-3975(98)00009-7.

[6] Marcin Jurdziński (1998), “Deciding the winner in parity games is in UP∩ co-UP”, Information Processing Letters (Elsevier) 68 (3): 119-124

[7] Calude, Cristian S and Jain, Sanjay and Khoussainov, Bakhadyr and Li, Wei and Stephan, Frank, “Deciding parity games in quasipolynomial time”, STOC 2017

[1]

[2]

[3]

[4]

[5]

[6]

[7]

解法

パリティゲームを解く再帰的なアルゴリズム

関連するゲームとそれらの決定問題

論理学やオートマトン理論との関係

参考文献

読書案内

外部リンク