パリティゲーム
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/06/16 06:46 UTC 版)
パリティゲーム (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部グラフ 
パリティゲームは計算複雑性理論の観点からも興味深い一方、パリティゲーム問題を自動検証やコントローラ合成などのバックエンドと位置付けることもできる。 たとえば、様相μ計算に対するモデル検査問題はパリティゲーム問題と同値であることが知られている。様相論理式の妥当性や充足可能性などを決定する問題もまた、パリティゲームに帰着することができる。
参考文献
- ^ 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
外部リンク
パリティゲームのソルバー:
- パリティゲームのページへのリンク
