パリティゲーム

パリティゲーム (parity games) は彩色された有向グラフ上でプレイされる理論上のゲームである。各ノードは優先度と呼ばれる(通常は有限種類の)自然数で彩色されている。このゲームはプレイヤー0とプレイヤー1の二名によってプレイされる。各プレイヤーは、ゲーム上に一個だけある駒をグラフの辺にそって動かす。手番は、その駒の現在地によって決められている。この操作を繰り返し(場合によっては無限回)行うことにより、プレイと呼ばれるパスが定まる。
有限長のプレイの場合、駒を動かせなくなったプレイヤーが敗者で、敗者でない側が勝者となる。無限長のプレイの勝者は、プレイ中に現れる優先度の値によって決定される。プレイ中に無限回現れた優先度のうち、最大の値が偶数ならばプレイヤー0の勝利、奇数ならばプレイヤー1の勝利となる。(偶奇が逆だったり、最大値のかわりに最小値を使う場合もある。) この偶奇性が「パリティ」の由来であろう。
パリティゲームはボレル階層の3層目に属する。したがってパリティゲームは決定的である。
"n"後者演算に関する二階の理論の決定可能性に関するラビンの証明では、パリティゲームに類似のゲームが暗黙的に使われ、該当ゲームの決定性も証明されている。 ナスター-タルスキの定理を使えば、パリティゲームの決定性に対するより単純な証明を与えることもできる。
さらに、パリティゲームは履歴なしの決定性 (history-free determinacy, memoryless determinacy) をもつ。 これは、あるパリティーゲームの初期位置で、どちらかのプレイヤーが必勝戦略を持つとき、履歴なしの必勝戦略、すなわち今までの駒の動きに関係なく、現在位置だけで次の行き先を決めるような戦略、が存在するというものである。
解法.
有限グラフ上のパリティゲームを解くとは、与えられた初期位置に対して、二人のプレイヤーのうちどちらが必勝戦略を持つか決定することである。この問題はNPかつCo-NP (より強く、UPかつco-UP) であることがわかっている。 また、QP (準多項式時間) であることもわかっている この問題が多項式時間で解けるかどうかは未解決問題である。
パリティゲームが履歴なしの決定性を持っているため、パリティゲームを解く問題は次のような単純げなグラフ理論の問題と同値である: "n"頂点の有限有向2部グラフ formula_1までの自然数で彩色されたものが与えられる。このとき、formula_2の頂点ごとにその頂点から出る辺を一つずつ選び、残りの出向辺を削除することで、得られた部分グラフの任意の閉路の最大優先度が偶数となるようにできるか？
パリティゲームを解く再帰的なアルゴリズム.
パリティゲームを解くための再帰的なアルゴリズムが、Zielonkaにより説明されている。 formula_3をパリティゲームとする。ここで、formula_2とformula_5はそれぞれプレイヤー0とプレイヤー1の手番になるノードの集合、formula_1 はノード全体の集合、 formula_7 は辺の集合、 formula_8 は優先度を割り当てる関数とする。 "E"はtotalであるとする。つまり、どのノードからも1本以上の辺が出ていると仮定する。
Zielonkaのアルゴリズムはアトラクタの概念に基づいている。 formula_9 をノードの集合とし、 formula_10 をプレイヤーの番号とする。"Uの"i-アトラクタ formula_11 とは、プレイヤー(1-"i")の選択にかかわらず有限回でUに到達するようプレイヤーiが誘導できるようなノードの集合である。これは以下のような不動点計算により定義できる:
別の言い方をすれば、初期集合 U から開始して、「プレイヤー0の手番となるノードで、 U に一歩で到達できるノード」と「プレイヤー1の手番となるノードで、プレイヤー1がどのように選択しても U に入ってしまうノード」をUに追加していく。これを繰り返して止まったときの"U"が"Attr"0("U")である。
Zielonkaのアルゴリズムは、優先度の値に関する再帰降下に基づいている。最大優先度が0のときは、どんな戦略であってもプレイヤー0が勝つのは明らかである。それ以外のときは、 p を最大優先度とし、 formula_13 をその優先度に紐付けられたプレイヤーの番号とする。また、 formula_14 を優先度が p であるようなノード全体の集合、 formula_15 をプレイヤー i のアトラクタとおく。このとき、プレイヤー i はうまく戦略を選ぶことで、 A を無限回訪問するようなプレイでは必ずプレイヤー i が勝つようにできる。
formula_16 を考える。このゲーム formula_17 は元のゲームより真に小さいから再帰的に解くことができ、それにより各プレイヤーの勝利領域 formula_18 がわかる。ここでもし formula_19 が空ならば、元のゲーム"G"の対応する勝利領域formula_20 も空である。なぜならば、プレイヤー formula_21 が formula_22 から抜ける唯一の方法は A に行くことで、この場合もプレイヤー i の勝利が確定するからである。
いっぽう、もし formula_19 が空ではなかった場合、プレイヤー formula_21 は少なくとも formula_19 では勝利することができる。なぜならば、プレイヤー i が formula_19 から A に逃げることはできない (さもなくば A がアトラクタであることに反する) からである。しかしそれ以外のノードでの必勝性は明らかではないので、プレイヤー formula_21  のアトラクタ formula_28 を計算し、これを G から取り除いた、より小さいゲーム formula_29 を得る。するとやはりこのゲームの必勝性を再帰的に解くことができ、各プレイヤーの勝利領域 formula_30 がわかる。このとき formula_31 かつ formula_32 であることがわかる。
このアルゴリズムは、擬似コードでは以下のように書ける:
 function formula_33
 p := G の最大優先度
 if formula_34
 return formula_35
 else
 U := G のノードで優先度 p のもの全体
 formula_36
 formula_37
 formula_38
 if formula_39
 return formula_40
 formula_41
 formula_42
 return formula_43
関連するゲームとそれらの決定問題.
ここまで述べてきたゲームや、同値なグラフ理論の問題に、ある少しの変更を加えることで、NP困難になる。 具体的には受理条件 (勝利条件) としてラビンの受理条件を採用するとNP困難になる。二部グラフ上の問題として説明すると、これは"V"0の各頂点から出向辺を1つずつ選ぶことで、どの閉路も(あるいは、どの強連結成分も)ある "i" について 2"i" で彩色された頂点を持つが、 2"i" + 1 で彩色された頂点を持たないようにできるか、という問題といえる。
パリティゲームとは異なり、ラビンの受理条件を採用したゲームはプレイヤー0とプレイヤー1に関して対称ではない。
論理学やオートマトン理論との関係.
パリティゲームは計算複雑性理論の観点からも興味深い一方、パリティゲーム問題を自動検証やコントローラ合成などのバックエンドと位置付けることもできる。 たとえば、様相μ計算に対するモデル検査問題はパリティゲーム問題と同値であることが知られている。様相論理式の妥当性や充足可能性などを決定する問題もまた、パリティゲームに帰着することができる。
外部リンク.
パリティゲームのソルバー: