技術要約：3人非協力ゲーム論理 (dGL3)

問題提起

自動運転車、ロボット、列車などのサイバーフィジカルシステム（CPS）は、異なる目標を持つ複数のエージェントが存在するマルチエージェント環境において、ますます複雑な運用を強いられています。単一エージェントのハイブリッドシステムや、2人ハイブリッドゲーム（ゼロサムまたは非ゼロサム）については広く研究されてきましたが、3人ハイブリッドゲームをモデル化することには根本的なギャップが存在します。

核心となる課題は、3つの異なるCPSエージェントが相互作用する場合に発生します。2人プレイヤーのシナリオでは、連合（coalition）を形成することでシステムを実質的に単一プレイヤーのハイブリッドシステムへと還元できますが、3人プレイヤーの相互作用は、全く新しいダイナミクスをもたらします。それは、プレイヤーが任意のタイミングで動的な連合を形成できるという能力です。3人プレイヤーの設定では、プレイヤーのいずれかの部分集合（空集合を除く）が、自らの目標の共通項を追求するために連合を形成でき、残りのプレイヤー（またはプレイヤーたち）は敵対的に作用します。既存の論理、例えば2プレイヤー用の微分ゲーム論理（dGL）や、固定された連合を扱う交互時間時相論理（ATL）では、このような非ゼロサム、非ハイブリッド、あるいはハイブリッドなシナリオにおいて、連合形成が流動的であり、かつ目標が個別の状況を適切に検証することはできません。具体的には、2人モデルにおけるゼロサムの仮定は、プレイヤー間の協調の可能性を無視するため、過度に保守的な結果を導いてしまいます。

手法

本論文では、離散的なジャンプと微分方程式のダイナミクスを持つ、3人のプレイヤーが関与するハイブリッドゲームを検証するために設計された論理、dGL3を導入しています。その手法は以下の要素で構成されています。

1. 構文と意味論

• 構文: dGL3は、実数算術を備えた一階述語論理を拡張し、2種類の式を導入しています：状態式（状態に対して解釈される）およびゲーム式（状態と連合のタプルに対して解釈される）。

  • 連合: プレイヤー $\{1, 2, 3\}$ の非空部分集合として表現されます。
  • モダリティ:
    • $\Diamond_C : \pi$ および $\Box_C : \pi$: 連合の集合 $C$ に対する存在量化および全称量化。
    • $\langle[\alpha]\rangle(\pi)$: $\alpha$ がハイブリッドゲームであり、$\pi$ が目標を記述するゲームモダリティ。
    • $\Xi(P_1, P_2, P_3)$: 個々のプレイヤーの目標を連言（conjunction）を通じて連合の目標へと集約する目標構成子。
  • ハイブリッドゲーム: 代入、連続的な進化（特定のプレイヤー $i$ によって制御される）、テスト、選択、逐次合成、および反復が含まれ、これらはすべて制御プレイヤーによってインデックス付けされます。

• 意味論: 式を（状態の集合、または状態と連合のタプルの集合）へとマッピングします。

  • 連合 $c$ は、状態 $\omega$ から開始されるゲーム $\alpha$ において、彼らの集約された目標を満たす状態に到達できる場合に勝利します。
  • 勝利領域: 再帰的に定義されます。ゲームを制御する連合 $c$ は、その経路を選択できます。制御していない連合は、制御プレイヤーが敵対的に行動するという最悪のシナリオに備えなければなりません。
  • 不動点: 反復ゲーム ($\alpha^*_i$) は、制御する連合（停止を選択できる側）については最大不動点を通じて、制御されていない連合（ループの期間に関わらず安全性を確保しなければならない側）については最小不動点を通じて扱われます。

2. 証明計算

dGL3のための、健全かつ相対的に完全な証明計算が構築されています。

• 公理: 計算には、制御プレイヤー $i$ が連合 $c$ に含まれるかどうかに基づいて、ゲーム構成要素（代入、選択、逐次、反復、連続的進化）を分解するための公理が含まれます。
  • $i \in c$ の場合、連合はその選択や進化を制御します。
  • $i \notin c$ の場合、連合は制御プレイヤーの選択による最悪の結果に直面します。
• 派生ルール: 単一の連合に関するルールから集合のルールを派生させることで、網羅的なケース分類を行うことなく、実用的な検証を可能にします。
• 単調性: 単調性ルールにより、目標集合を増やすことで勝利領域が拡大することが保証されます。

3. 等価性と完全性

中心的な手法上の貢献は、3人ハイブリッドゲームは論理的に2人ハイブリッドゲームに還元できるという証明です。

• 翻訳: 本論文は、任意の dGL3 式を等価な dGL 式にマッピングする翻訳関数 ($\flat$) を定義しています。これは、連合のメンバーを「エンジェル（天使）」、残りのプレイヤーを「デーモン（悪魔）」としてグループ化することによって達成されます。
• 相対的完全性: dGL は相対的に完全であることが知られており、dGL3 が構文的翻訳を通じて dGL と等価であることが示されているため、dGL3 の計算は、任意の微分表現可能な論理に対して相対的に完全であることが証明されます。

主要な結果

1. 論理的等価性: 本論文は、3人ハイブリッドゲームの論理は、2人ハイブリッドゲームの論理と論理的に等価であるという驚くべき結果を証明しています：
   $$\text{2人ハイブリッドゲーム} \equiv_{\text{logic}} \text{3人ハイブリッドゲーム}$$
   この等価性は、3人プレイヤーの設定における動的な連合形成の複雑さにもかかわらず成立します。
2. 健全性: dGL3 の証明計算は健全であると証明されています。すなわち、計算量において証明可能な式は、すべての状態で妥当です。
3. 相対的完全性: 計算は相対的に完全です。妥当な dGL3 式は、計算と微分表現可能な論理の公理を用いて証明可能です。
4. 単調性: ハイブリッドゲームの勝利領域関数は単調であることが証明されており、これにより反復ゲームのセマンティクスに必要な不動点の存在が保証されます。

意義と主張

本論文は、dGL3 が、動的な連合形成が可能な、3人のプレイヤーが関与する非ゼロサム・ハイブリッドゲームを検証できる最初の論理であると主張しています。

• 「3人プレイヤーの課題」への対処: 著者らは、2人プレイヤーのゲームにおける連合はシステムを自明に1人プレイヤーのシステムへと還元するのに対し、3人プレイヤーのゲームは、たとえ2人が連合を形成したとしても、真のマルチエージェントの複雑さを保持していることを強調しています。dGL3 はこの特定の課題に対処しています。
• 過度な保守性の回避: 非ゼロサムの目標と連合の可能性を明示的にモデル化することにより、プレイヤー間の協調の可能性を無視してしまうゼロサムの仮定が生み出す、過度に保守的な結果を回避します。
• 汎用性: この論理は、3人のプレイヤーの「連合としての力」を扱うのに十分な汎用性があることを示しており、2人プレイヤーの推論原理が3人プレイヤーのダイナミクスを制御するのに十分であることを確立しています。
• 今後の展望: 著者らは、$n$ 人プレイヤーの根本的な課題はすでに3人プレイヤーのケースに現れていると指摘しており、dGL3 が $n$ 人プレイヤーのシナリオへの検証を拡張するための基礎を提供することを示唆しています。

論文では、車のドライバー、オートバイのライダー、ガソリンスタンドの店員を含む典型的な例を用いてこれらの能力を説明しており、どのように連合形成（例：ドライバーが店員と組むこと）が、厳格なゼロサムまたは固定された連合の仮定の下では不可能、あるいは証明不可能な勝利戦略を可能にするかを実証しています。