パリティゲーム

パリティ ゲームは、色付きの有向グラフ上でプレイされます。各ノードは、優先度 (通常は有限個の自然数) によって色分けされています。2 人のプレーヤー (0 と 1) が、(共有されている単一の) トークンをグラフの端に沿って移動します。トークンが置かれたノードの所有者は、後続ノードを選択します (次の移動を行います)。プレーヤーはトークンの移動を続け、プレイと呼ばれる (無限の可能性のある)パスが作成されます。

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

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

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

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

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

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

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

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

${\displaystyle {\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 に属するすべてのノードを追加します。 ${\displaystyle Attr_{i}(U)^{j+1}}$${\displaystyle Attr_{i}(U)^{j}}$${\displaystyle Attr_{i}(U)^{j}}$

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

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

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

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

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

上記のゲームおよび関連するグラフ理論的問題を少し変更すると、ゲームを解くことがNP 困難になります。変更されたゲームにはラビンの受容条件があり、すべての頂点は単一の色ではなく色のセットによって色付けされます。したがって、色jがvの色セットに属する場合、頂点v は色jを持つと言います。無限プレイでプレイヤー 0 が勝つのは、プレイ中の頂点の無限数が色2iを持ち、有限数が色2i+1を持つようなi が存在する場合です。

パリティは、すべての頂点が単一の色を持つ特殊なケースです。具体的には、上記の二部グラフのシナリオでは、問題は、V ₀の各頂点から単一の出力エッジを選択する選択関数が存在するかどうかを判断することです。その結果、結果のサブグラフには、各サイクル (したがって、各強く接続されたコンポーネント) にi と色 2 iのノードが存在し、色 2 i  + 1 のノードが存在しないというプロパティがあります...

パリティ ゲームとは異なり、このゲームはプレイヤー 0 と 1 に関して対称ではなくなることに注意してください。

興味深い計算量理論上の地位にもかかわらず、パリティ ゲーム解決は、自動検証とコントローラ合成の問題に対するアルゴリズムのバックエンドとして見ることができます。たとえば、様相 μ 計算のモデル検査問題は、パリティ ゲーム解決と同等であることが知られています。また、様相論理の妥当性や充足可能性などの決定問題は、パリティ ゲーム解決に還元できます。

• 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 コレクション
• ブーーーー