パリティゲームのソースを表示

[[ファイル:Example_Parity_Game_Solved.png|右|サムネイル|300x300ピクセル|パリティゲームの例。 円形のノードはプレイヤー0に、正方形のノードはプレイヤー1に属する。 左側の青い領域はプレイヤー0の勝利領域で、右側の赤い領域はプレイヤー1の勝利領域である。]]
'''パリティゲーム (parity games)''' は彩色された[[有向グラフ]]上でプレイされる理論上のゲームである。各ノードは優先度と呼ばれる(通常は有限種類の)[[自然数]]で彩色されている。このゲームはプレイヤー0とプレイヤー1の二名によってプレイされる。各プレイヤーは、ゲーム上に一個だけある駒をグラフの辺にそって動かす。手番は、その駒の現在地によって決められている。この操作を繰り返し(場合によっては無限回)行うことにより、プレイと呼ばれる[[道 (グラフ理論)|パス]]が定まる。

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

パリティゲームは[[ボレル階層]]の3層目に属する。したがってパリティゲームは決定的である。<ref>D. A. Martin: Borel determinacy, The Annals of Mathematics, Vol 102 No. 2 pp. 363&#x2013;371 (1975)</ref>

''n''後者演算に関する二階の理論の[[決定可能性]]に関する[[マイケル・ラビン|ラビン]]の証明では、パリティゲームに類似のゲームが暗黙的に使われ、該当ゲームの決定性も証明されている。<ref>{{Cite journal|last=Rabin|first=MO|year=1969|title=Decidability of second-order theories and automata on infinite trees|journal=Transactions of the American Mathematical Society|volume=141|pages=1–35|publisher=American Mathematical Society|doi=10.2307/1995086|jstor=1995086}}</ref> [[ナスター-タルスキの定理]]を使えば、パリティゲームの決定性に対するより単純な証明を与えることもできる。<ref name="EJ">E. A. Emerson and C. S. Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368&#x2013;377 (1991), {{ISBN2|0-8186-2445-0}}</ref>

さらに、パリティゲームは履歴なしの決定性 (history-free determinacy, memoryless determinacy) をもつ。<ref>A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)</ref><ref name="ZL">{{Cite journal|last=Zielonka|first=W|year=1998|title=Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees|journal=Theor. Comput. Sci.|volume=200|issue=1&ndash;2|pages=135&ndash;183|doi=10.1016/S0304-3975(98)00009-7}}</ref> これは、あるパリティーゲームの初期位置で、どちらかのプレイヤーが必勝戦略を持つとき、履歴なしの必勝戦略、すなわち今までの駒の動きに関係なく、現在位置だけで次の行き先を決めるような戦略、が存在するというものである。

== 解法 ==
{{Unsolved|計算機科学|パリティゲームは多項式時間で解けるか？}}<span>有限グラフ上のパリティゲームを</span>'''解く'''とは、与えられた初期位置に対して、二人のプレイヤーのうちどちらが必勝戦略を持つか決定することである。この問題は[[NP]]かつ[[Co-NP]] (より強く、[[UP (計算複雑性理論)|UP]]かつco-UP) であることがわかっている。<ref>{{Citation|title=Deciding the winner in parity games is in UP∩ co-UP|authors=Marcin Jurdziński|date=1998|journal=Information Processing Letters|volume=68|issue=3|pages=119-124|publisher=Elsevier}}</ref> また、QP (準多項式時間) であることもわかっている<ref>{{Citation|title=Deciding parity games in quasipolynomial time|authors=Calude, Cristian S and Jain, Sanjay and Khoussainov, Bakhadyr and Li, Wei and Stephan, Frank|journal=STOC 2017}}</ref> この問題が[[P (計算複雑性理論)|多項式時間で解ける]]かどうかは未解決問題である。

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

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

Zielonkaのアルゴリズムはアトラクタの概念に基づいている。 <math>U \subseteq V</math> をノードの集合とし、 <math>i=0,1</math> をプレイヤーの番号とする。''Uの''i-アトラクタ <math>Attr_i(U)</math> とは、プレイヤー(1-''i'')の選択にかかわらず有限回でUに到達するようプレイヤーiが誘導できるようなノードの集合である。これは以下のような不動点計算により定義できる:
: <math>\begin{align}
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{align}</math>
別の言い方をすれば、初期集合 U から開始して、「プレイヤー0の手番となるノードで、 U に一歩で到達できるノード」と「プレイヤー1の手番となるノードで、プレイヤー1がどのように選択しても U に入ってしまうノード」をUに追加していく。これを繰り返して止まったときの''U''が''Attr''0(''U'')である。

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

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

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

このアルゴリズムは、[[擬似コード]]では以下のように書ける:
  '''function''' <math>solve(G)</math>
      p := G の最大優先度
      '''if''' <math>p = 0</math>
          '''return''' <math>W_0, W_1 := V, \{\}</math>
      '''else'''
          U :=  G のノードで優先度 p のもの全体
          <math>i := p \bmod 2</math>
          <math>A := Attr_i(U)</math>
          <math>W_0', W_1' := solve(G \setminus A)</math>
          '''if''' <math>W_i' = V</math>
               '''return''' <math>W_i , W_{1-i} := V, \{\}</math>
          <math>B := Attr_{1-i}(W_{1-i}')</math>
          <math>W_0'', W_1'' := solve(G \setminus B)</math>
          '''return''' <math>W_i , W_{1-i} := W_i'', W_{1-i}'' \cup B</math>

== 関連するゲームとそれらの決定問題 ==
ここまで述べてきたゲームや、同値なグラフ理論の問題に、ある少しの変更を加えることで、[[NP困難]]になる。 具体的には受理条件 (勝利条件) として[[ラビンオートマトン|ラビンの受理条件]]を採用するとNP困難になる。二部グラフ上の問題として説明すると、これは''V''<sub>0</sub>の各頂点から出向辺を1つずつ選ぶことで、どの閉路も(あるいは、どの強連結成分も)ある ''i''  について&nbsp;2''i'' で彩色された頂点を持つが、&nbsp;2''i''&nbsp;+&nbsp;1 で彩色された頂点を持たないようにできるか、という問題といえる。

パリティゲームとは異なり、ラビンの受理条件を採用したゲームはプレイヤー0とプレイヤー1に関して対称ではない。

== 論理学やオートマトン理論との関係 ==
[[ファイル:Applications_of_Parity_Games.png|右|サムネイル|400x400ピクセル|パリティゲーム問題の主な応用]]
パリティゲームは計算複雑性理論の観点からも興味深い一方、パリティゲーム問題を自動検証やコントローラ合成などのバックエンドと位置付けることもできる。 たとえば、[[様相μ計算]]に対するモデル検査問題はパリティゲーム問題と同値であることが知られている。様相論理式の妥当性や充足可能性などを決定する問題もまた、パリティゲームに帰着することができる。

== 参考文献 ==
<references />
* {{Cite book|last=Erich Grädel, Phokion G. Kolaitis, [[Leonid Libkin]], Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, Scott Weinstein|author=Erich Grädel, Phokion G. Kolaitis, [[Leonid Libkin]], Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, Scott Weinstein|title=Finite model theory and its applications|year=2007|publisher=Springer|ISBN=978-3-540-00428-8}}

== 読書案内 ==
* E. Grädel, W. Thomas, T. Wilke (Eds.) : ''Automata, Logics, and Infinite Games'', Springer LNCS 2500 (2003), {{ISBN2|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

== 外部リンク ==
パリティゲームのソルバー:
* [https://github.com/oliverfriedmann/pgsolver PGSolver Collection]

{{デフォルトソート:はりていげむ}}
[[Category:ゲーム]]