パリティゲーム

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

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

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

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

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

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

パリティゲームが履歴なしの決定性を持っているため、パリティゲームを解く問題は次のような単純げなグラフ理論の問題と同値である: *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{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}
別の言い方をすれば、初期集合 U から開始して、「プレイヤー0の手番となるノードで、 U に一歩で到達できるノード」と「プレイヤー1の手番となるノードで、プレイヤー1がどのように選択しても U に入ってしまうノード」をUに追加していく。これを繰り返して止まったときの*U*が*Attr*0(*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</math> を得る。するとやはりこのゲームの必勝性を再帰的に解くことができ、各プレイヤーの勝利領域 <math>W*_i, W*_{1-i}</math> がわかる。このとき <math>W_i = W*_i かつ 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に関して対称ではない。

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

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

== 参考文献 ==
<references />
* 

== 読書案内 ==
* E. Grädel, W. Thomas, T. Wilke (Eds.) : *Automata, Logics, and Infinite Games*, Springer LNCS 2500 (2003), 
* W. Zielonka : *Infinite games on finitely coloured graphs with applications to automata on infinite tree'', TCS, 200(1-2):135-183, 1998

## 外部リンク
パリティゲームのソルバー:
* PGSolver Collection