Semi-Competitive Differential Game Logic

Technical Summary: Semi-Competitive Differential Game Logic (dGLsc)

Problem Statement
The safety verification of Cyber-Physical Systems (CPS), particularly those involving interactions between multiple agents (e.g., autonomous vehicles, aircraft), presents significant challenges. Traditional approaches often model these interactions using Differential Game Logic (dGL), which assumes a zero-sum, adversarial relationship where one player's gain is the other's loss. While this yields safe results, it is often overly conservative. In many real-world scenarios, such as collision avoidance, agents share safety objectives (e.g., neither wants to crash) while pursuing distinct individual goals (e.g., reaching different destinations). A zero-sum assumption fails to capture the potential for cooperation in these "non-zero-sum" games, leading to verification failures for systems that are actually safe. Furthermore, existing non-zero-sum logics often struggle with continuous dynamics or require complex game trees that are intractable for hybrid systems with unbounded depth.

Methodology
The paper introduces Semi-Competitive Differential Game Logic (dGLsc), a formal logic designed to verify hybrid games where two players (Angel and Demon) possess individual, potentially overlapping goals. The core methodology relies on the concept of semi-competitiveness:

1. Behavioral Model: Players cooperate when it is helpful for both to achieve their respective goals but compete when necessary. Specifically, a player will never lose on purpose. If multiple winning options exist, a player chooses one that also helps the opponent win. If no option leads to a win for the player, they do not altruistically help the opponent.
2. Syntax: dGLsc extends the syntax of dGL by modifying the modalities. Instead of $\langle \alpha \rangle P$ (Angel wins $\alpha$ to reach $P$) and $[\alpha] Q$ (Demon wins $\alpha$ to reach $Q$), dGLsc uses $\langle \alpha \rangle (P, Q)$ and $[\alpha] (P, Q)$. These modalities explicitly encode both players' goals within the formula, allowing the logic to reason about the interaction of individual objectives.
3. Semantics: The semantics define winning regions $\varsigma_\alpha(X, Y)$ for Angel and $\delta_\alpha(X, Y)$ for Demon, where $X$ and $Y$ are the goal sets. Unlike dGL, these regions are not complementary. The semantics account for cooperation by including states where both players can win simultaneously. For example, in a continuous game, Demon's winning region includes states where Angel (who controls the evolution) stops the system at a point where both goals are met. The semantics for repetition games ($\alpha^*$) are defined via fixpoints that distinguish between competitive and cooperative scenarios, utilizing the least fixpoint for Angel and the greatest fixpoint for Demon to ensure uniqueness and monotonicity.
4. Proof Calculus: A sound and relatively complete proof calculus is presented. It includes axioms for each hybrid game operator (assignment, continuous evolution, test, choice, sequence, dual, repetition) tailored to the two-goal structure. Crucially, the calculus includes a Fixpoint Rule (FP) that characterizes repetition games as the union of two least fixpoints (one for competition, one for cooperation). The system also includes monotonicity rules and a determinacy axiom for cases where goals are complementary.

Key Contributions

• Formal Logic dGLsc: The introduction of a logic specifically for non-zero-sum hybrid games with continuous dynamics, enabling the verification of safety-critical systems where agents have overlapping but distinct goals.
• Semi-Competitive Semantics: A novel semantic framework where players act cooperatively if it aids their own success, resolving the tension between individual optimization and mutual safety without requiring explicit negotiation protocols.
• Theoretical Properties:
  • Monotonicity: Proven that increasing a player's goal set expands their winning region.
  • Equivalence to dGL: Demonstrated that when goals are complementary (opposing), dGLsc reduces to standard zero-sum dGL.
  • General Equivalence: Showed that any dGLsc winning region can be expressed as a disjunction of winning regions in a transformed dGL game (removing dual operators) and a standard dGL game, proving the logic's expressiveness.
• Proof Calculus: A sound and relatively complete calculus that avoids the need for manual coding of non-zero-sum concepts (which would be required if using standard dGL) and supports modular reasoning.

Results
The paper establishes the soundness of the proof calculus, ensuring that all provable formulas are valid. It further proves relative completeness, showing that any valid formula in dGLsc can be proven if the underlying first-order logic is differentially expressive. The paper illustrates the utility of dGLsc through a canonical example of two planes exchanging fuel stocks. In this scenario, standard dGL would fail to verify safety because the agents cannot control the variables critical to the other's goal. However, dGLsc successfully verifies the safety of the interaction because the semi-competitive semantics allow the agents to cooperate (e.g., Angel filling Demon's tank) to ensure both reach their respective targets.

Significance
The paper claims that dGLsc provides a natural and intuitive way to express and reason about non-zero-sum hybrid games, which are prevalent in multi-agent CPS but difficult to verify under conservative zero-sum assumptions. By formalizing semi-competitive behavior, the logic enables safety proofs for situations that are unsafe under zero-sum assumptions but safe in reality due to the potential for cooperation. The work bridges the gap between game-theoretic concepts of non-zero-sum equilibria and the formal verification of hybrid systems with continuous dynamics, offering a tool that is more precise than adversarial models while remaining computationally tractable compared to general game-theoretic approaches.