AI 中文总结
研究三人微分博弈逻辑dGL3，用于验证含离散和微分方程动力学的混合博弈，考虑玩家联盟力量。给出其语法、语义及关键性质，引入可靠且相对完备的证明演算，并通过典型例子展示其使用。
AI 中文摘要
本文介绍了三人微分博弈逻辑dGL3，它能验证具有离散和微分方程动力学的混合博弈，博弈中有三个玩家，他们可能形成联盟，也可能不形成。每个玩家都有各自试图实现的目标，当玩家目标重叠时博弈变为非零和博弈。dGL3能验证涉及多个玩家的复杂情况，考虑到他们的联盟力量。dGL3擅长验证玩家共享安全目标但其他目标不同、可能协作也可能不协作的博弈。在此情况下，零和假设会因忽略玩家间协调潜力而导致过于保守的结果。本文给出了dGL3的语法和语义，并证明了其关键性质。引入了dGL3的可靠且相对完备的证明演算，并通过一个典型例子说明了dGL3的使用。
英文摘要
This paper introduces the three-player differential game logic dGL3, which enables the verification of hybrid games of discrete and differential equation dynamics with three players who may or may not form coalitions. Each player has an individual goal they try to fulfill, so the game becomes non-zero-sum when the goals of the players overlap. This is how dGL3 can verify complex situations involving multiple players, taking into account their coalitional power. dGL3 excels at verifying games where players share safety objectives but otherwise pursue different goals, so that they may or may not collaborate. In this case, zero-sum assumptions lead to overly conservative results by neglecting the potential of coordination amongst the players. In this paper, the syntax and semantics of dGL3 are presented and crucial properties of dGL3 are proved. A sound and relatively complete proof calculus for dGL3 is introduced and the use of dGL3 is illustrated in a canonical example.
Comments29 pages, 4 figures, version includes minor fixes of typos, etc
