Semi-Competitive Differential Game Logic

Abstract

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