Semi-competitive Differential Game Logic
摘要
This paper introduces semi-competitive differential game logic \(\textsf {dG}\mathcal {L}_{sc}\) , which enables verification of safety-critical applications that involve interactions between two agents. In \(\textsf {dG}\mathcal {L}_{sc}\) , these interactions are specified as games on hybrid systems with two players that may collaborate with each other when helpful and may compete when necessary. The players in the hybrid games of \(\textsf {dG}\mathcal {L}_{sc}\) have individual goals that may overlap, leading to nonzero-sum games. This makes \(\textsf {dG}\mathcal {L}_{sc}\) especially well-suited for verifying situations where players, e.g., share safety objectives but otherwise pursue different goals, so that zero-sum assumptions lead to overly conservative results. Additionally, \(\textsf {dG}\mathcal {L}_{sc}\) solves the subtlety that even though each player may benefit from knowledge of the other player’s goals, e.g., concerning shared safety objectives, unsafe situations might still occur if every player were to mutually assume the other player would act to avoid unsafety. The syntax and semantics, as well as a sound and relatively complete proof calculus are presented for \(\textsf {dG}\mathcal {L}_{sc}\) . The relationship between \(\textsf {dG}\mathcal {L}_{sc}\) and zero-sum differential game logic \(\textsf {dG}\mathcal {L}\) is discussed and the purpose of \(\textsf {dG}\mathcal {L}_{sc}\) illustrated in a canonical example.