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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Semi-competitive Differential Game Logic

  • Julia Butte,
  • André Platzer

摘要

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.