パリティゲーム

パリティゲームは、色付き有向グラフ上でプレイされます。グラフの各ノードは、優先度（通常は有限個の自然数）によって色付けされています。2人のプレイヤー（0と1）は、（共有の）トークンをグラフの端に沿って動かします。トークンが落ちたノードの所有者は、次のノードを選択します（次の動きを行います）。プレイヤーはトークンを動かし続け、結果として（おそらく無限の）パスが形成されます。これをプレイと呼びます。

有限プレイの勝者は、相手が動けなくなったプレイヤーです。無限プレイの勝者は、プレイ中に出現する優先順位によって決まります。通常、無限プレイにおいて、プレイ中に無限に出現する最大の優先順位が偶数であれば、プレイヤー0が勝ちます。そうでない場合は、プレイヤー1が勝ちます。これが、タイトルにある「パリティ」という言葉の由来です。

パリティゲームはボレル階層の第3レベルに位置し、その結果決定されます。^[1]

パリティゲームに関連するゲームは、ラビンによるn後継者のモナド的2階理論（n = 2のS2S ）の決定可能性の証明で暗黙的に使用され、そのようなゲームの決定性が証明されました。^[2]クナスター・タルスキの定理は、パリティゲームの決定性の比較的簡単な証明につながります。^[3]

さらに、パリティゲームは履歴に依存せずに決定されます。^[3]^[4]^[5]これは、プレイヤーが勝利戦略を持っている場合、そのプレイヤーの勝利戦略は、プレイの履歴ではなく、現在のボードの位置のみに依存することを意味します。

ゲームを解く

コンピュータサイエンスにおける未解決問題

パリティゲームは多項式時間で解くことができますか?

コンピュータサイエンスにおけるさらなる未解決問題

有限グラフ上で行われるパリティゲームを解くということは、与えられた開始位置において、2人のプレイヤーのうちどちらが勝利戦略を持っているかを決定することを意味します。この問題は、 NPおよびco-NP、より正確にはUPおよびco-UPにおいて、またQP（準多項式時間）においても解けることが示されています。 [ ⁶^{]この決定問題が}PTimeで解けるかどうかは未解決の問題です。

パリティゲームは履歴に依存しない決定性を持つため、与えられたパリティゲームを解くことは、次に示すような単純なグラフ理論の問題を解くことと等価である。n 個の頂点を持つ有限有向二部グラフと、1からmまでの色で色付けされたVが与えられたとき、の各頂点から単一の出力辺を選択する選択関数が存在する。この場合、結果として得られる部分グラフは、各サイクルにおいて最大出現色が偶数色であるという特性を持つ。 $V=V_{0}\cup V_{1}$ $V_{0}$

パリティゲームを解くための再帰アルゴリズム

Zielonkaは、パリティゲームを解く再帰アルゴリズムを概説しました。をパリティゲームとし、それぞれプレイヤー0とプレイヤー1に属するノードの集合、をすべてのノードの集合、をエッジの全集合、を優先順位割り当て関数とします。 $G=(V,V_{0},V_{1},E,\Omega )$ $V_{0}$ $V_{1}$ $V=V_{0}\cup V_{1}$ $E\subseteq V\times V$ $\Omega :V\rightarrow \mathbb {N}$

ジエロンカのアルゴリズムは、アトラクターの記法に基づいています。をノードの集合とし、をプレイヤーとします。Uの $i -アトラクターとは、$ $U$ を含むノードの集合のうち、 $i が$ 内のすべてのノードから $U$ への訪問を強制できる最小の集合です。これは $、$ 固定点計算によって定義できます。 $U\subseteq V$ $i=0,1$ $Attr_{i}(U)$ $Attr_{i}(U)$

{\begin{aligned}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{aligned}}

言い換えれば、初期セット $U$ から開始します。次に、各ステップ ( ) において、プレイヤー 0 に属するノードのうち、1 本のエッジで前のセット ( ) に到達できるノードと、プレイヤー 1 に属するノードのうち、プレイヤー 1 がどのエッジを選択しても前のセット ( ) に到達できるノードをすべて追加します。 $Attr_{i}(U)^{j+1}$ $Attr_{i}(U)^{j}$ $Attr_{i}(U)^{j}$

Zielonkaのアルゴリズムは、優先度の数に基づく再帰降下法に基づいています。最大の優先度が0の場合、プレイヤー0がゲーム全体に勝利することが（任意の戦略で）すぐにわかります。そうでない場合、最大の優先度を $p$ とし、優先度に関連付けられたプレイヤーをとします。優先度 $p$ を持つノードの集合をとし、対応するプレイヤー $i$ のアトラクターをとします。これにより、プレイヤー $iは、$ $Aを$ 無限回訪れるすべてのプレイにおいて、プレイヤー $i$ が勝利することを保証できます。 $i=p{\bmod {2}}$ $U=\{v\mid \Omega (v)=p\}$ $A=Attr_{i}(U)$

$A$ のすべてのノードと影響を受けるエッジが削除されたゲームを考えてみましょう。再帰によって小さなゲームを解き、勝利セットのペアを得ることができます。が空の場合、ゲーム $G$ も空です。なぜなら、プレイヤーは $A$ から脱出することしかできず、その結果プレイヤー $i$ が勝利するからです。 $G'=G\setminus A$ $G'$ $W'_{i},W'_{1-i}$ $W'_{1-i}$ $W_{1-i}$ $1-i$ $W_{i}'$

それ以外の場合、が空でない場合、プレイヤー $iはから$ $A$ へ逃げることができないため（ $A$ は $i$ -アトラクターであるため）、プレイヤーがで勝てるということだけが確実に分かります。したがって、アトラクターを計算し、 $G$ から削除して、より小さなゲームを得ます。これを再帰的に解くと、勝利セットのペアが得られます。したがって、とが成り立ちます。 $W'_{1-i}$ $1-i$ $W'_{1-i}$ $W'_{1-i}$ $B=Attr_{1-i}(W'_{1-i})$ $G''=G\setminus B$ $W''_{i},W''_{1-i}$ $W_{i}=W''_{i}$ $W_{1-i}=W''_{1-i}\cup B$

単純な疑似コードでは、アルゴリズムは次のように表現されます。

関数  $p$   :=  $Gの最大優先度$ if return else  $U$   :=  $G$ の優先度 $pのノード$ if return return $solve(G)$     $p=0$    $W_{0},W_{1}:=V,\{\}$     $i:=p{\bmod {2}}$   $A:=Attr_{i}(U)$   $W_{0}',W_{1}':=solve(G\setminus A)$    $W_{1-i}'=\{\}$    $W_{i},W_{1-i}:=V,\{\}$   $B:=Attr_{1-i}(W_{1-i}')$   $W_{0}'',W_{1}'':=solve(G\setminus B)$    $W_{i},W_{1-i}:=W_{i}'',W_{1-i}''\cup B$

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

パリティゲーム解法は、計算量理論における興味深い地位を占めているにもかかわらず、自動検証や制御器合成における問題に対するアルゴリズム的バックエンドとして捉えることができます。例えば、様相μ計算のモデル検査問題は、パリティゲーム解法と等価であることが知られています。また、様相論理の妥当性や充足可能性といった決定問題も、パリティゲーム解法に帰着することができます。

参考文献

^ DA Martin：ボレルの決定性、数学年報、第102巻第2号、pp.363-371（1975年）
^ Rabin, MO (1969). 「無限木上の2階理論とオートマトンにおける決定可能性」.アメリカ数学会誌. 141.アメリカ数学会誌: 1–35 . doi :10.2307/1995086. JSTOR 1995086.
^ ab EA EmersonとCS Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991), ISBN 0-8186-2445-0
^ A. モストフスキー：禁止された位置を持つゲーム、グダニスク大学、技術報告書78（1991）
^ Zielonka, W (1998). 「有限色グラフ上の無限ゲームと無限木上のオートマトンへの応用」. Theor. Comput. Sci . 200 ( 1– 2): 135– 183. doi : 10.1016/S0304-3975(98)00009-7 .
^ Marcin Jurdziński (1998)、「パリティゲームにおける勝者の決定はUP∩co-UPにある」（PDF）、Information Processing Letters、68（3）、Elsevier：119– 124、doi：10.1016/S0020-0190（98）00150-1
^ Calude, Cristian S; Jain, Sanjay; Khoussainov, Bakhadyr; Li, Wei; Stephan, Frank、「準多項式時間でのパリティゲームの決定」（PDF）、Stoc 2017

Erich Grädel, Phokion G. Kolaitis, Leonid Libkin , Maarten Marx, Joel Spencer , Moshe Y. Vardi , Yde Venema, Scott Weinstein (2007).有限モデル理論とその応用. Springer. ISBN 978-3-540-00428-8。{{cite book}}: CS1 maint: multiple names: authors list (link)

さらに読む

E. Grädel、W. Thomas、T. Wilke（編）：オートマタ、ロジック、無限ゲーム、Springer LNCS 2500（2003）、ISBN 3-540-00388-6
W. Zielonka :有限色グラフ上の無限ゲームと無限木オートマトンへの応用、TCS、200(1-2):135-183、1998

外部リンク

最先端のパリティゲーム解決ツールセットは次の 2 つです。

PGSolver コレクション
ブーブー

[1] DA Martin：ボレルの決定性、数学年報、第102巻第2号、pp.363-371（1975年）

[2] Rabin, MO (1969). 「無限木上の2階理論とオートマトンにおける決定可能性」.アメリカ数学会誌. 141.アメリカ数学会誌: 1–35 . doi :10.2307/1995086. JSTOR 1995086.

[EJ-3] EA EmersonとCS Jutla: Tree Automata, Mu-Calculus and Determinacy, IEEE Proc. Foundations of Computer Science, pp 368–377 (1991), ISBN 0-8186-2445-0

[4] A. モストフスキー：禁止された位置を持つゲーム、グダニスク大学、技術報告書78（1991）

[ZL-5] Zielonka, W (1998). 「有限色グラフ上の無限ゲームと無限木上のオートマトンへの応用」. Theor. Comput. Sci . 200 ( 1– 2): 135– 183. doi : 10.1016/S0304-3975(98)00009-7 .

[6] Marcin Jurdziński (1998)、「パリティゲームにおける勝者の決定はUP∩co-UPにある」（PDF）、Information Processing Letters、68（3）、Elsevier：119– 124、doi：10.1016/S0020-0190（98）00150-1

[7] Calude, Cristian S; Jain, Sanjay; Khoussainov, Bakhadyr; Li, Wei; Stephan, Frank、「準多項式時間でのパリティゲームの決定」（PDF）、Stoc 2017