Semi-competitive Differential Game Logic

This paper introduces semi-competitive differential game logic dGL$_{sc}$, which enables verification of safety-critical applications that involve interactions between two agents. In dGL$_{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 dGL$_{sc}$ have individual goals that may overlap, leading to nonzero-sum games. This makes dGL$_{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, dGL$_{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 dGL$_{sc}$. The relationship between dGL$_{sc}$ and zero-sum differential game logic dGL is discussed and the purpose of dGL$_{sc}$ illustrated in a canonical example.