Semi-Competitive Differential Game Logic

Abstract

Abstract This paper introduces semi-competitive differential game logic $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , which enables verification of safety-critical applications that involve interactions between two agents. In $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , 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}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> have individual goals that may overlap, leading to nonzero-sum games. This makes $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> 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}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> 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}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> . The relationship between $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> and zero-sum differential game logic $$\textsf {dG}\mathcal {L}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:mi>L</mml:mi> </mml:mrow> </mml:math> is discussed and the purpose of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> illustrated in a canonical example.