パリティゲーム
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
パリティゲームを解くための再帰的なアルゴリズムが、Zielonkaにより説明されている。 G = ( V , V 0 , V 1 , E , Ω ) {\displaystyle G=(V,V_{0},V_{1},E,\Omega )} をパリティゲームとする。ここで、 V 0 {\displaystyle V_{0}} と V 1 {\displaystyle V_{1}} はそれぞれプレイヤー0とプレイヤー1の手番になるノードの集合、 V = V 0 ∪ V 1 {\displaystyle V=V_{0}\cup V_{1}} はノード全体の集合、 E ⊆ V × V {\displaystyle E\subseteq V\times V} は辺の集合、 Ω : V → N {\displaystyle \Omega :V\rightarrow \mathbb {N} } は優先度を割り当てる関数とする。 Eはtotalであるとする。つまり、どのノードからも1本以上の辺が出ていると仮定する。
Zielonkaのアルゴリズムはアトラクタの概念に基づいている。 U ⊆ V {\displaystyle U\subseteq V} をノードの集合とし、 i = 0 , 1 {\displaystyle i=0,1} をプレイヤーの番号とする。Uのi-アトラクタ A t t r i ( U ) {\displaystyle Attr_{i}(U)} とは、プレイヤー(1-i)の選択にかかわらず有限回でUに到達するようプレイヤーiが誘導できるようなノードの集合である。これは以下のような不動点計算により定義できる:
パリティゲーム (parity games) は彩色された有向グラフ上でプレイされる理論上のゲームである。各ノードは優先度と呼ばれる(通常は有限種類の)自然数で彩色されている。このゲームはプレイヤー0とプレイヤー1の二名によってプレイされる。各プレイヤーは、ゲーム上に一個だけある駒をグラフの辺にそって動かす。手番は、その駒の現在地によって決められている。この操作を繰り返し(場合によっては無限回)行うことにより、プレイと呼ばれるパスが定まる。
有限長のプレイの場合、駒を動かせなくなったプレイヤーが敗者で、敗者でない側が勝者となる。無限長のプレイの勝者は、プレイ中に現れる優先度の値によって決定される。プレイ中に無限回現れた優先度のうち、最大の値が偶数ならばプレイヤー0の勝利、奇数ならばプレイヤー1の勝利となる。(偶奇が逆だったり、最大値のかわりに最小値を使う場合もある。