💻 computer science

Three-player Differential Game Logic

This paper introduces dGL3, a three-player differential game logic with a sound and relatively complete proof calculus designed to verify non-zero-sum hybrid games where players with individual goals can form coalitions, thereby overcoming the overly conservative limitations of zero-sum assumptions in scenarios involving shared safety objectives.

Original authors: Julia Butte, André Platzer

Published 2026-07-27

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Julia Butte, André Platzer

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a world where the machines around us—self-driving cars, robots, and smart trains—are not just following a script, but are actually playing a high-stakes game. This is the realm of Cyber-Physical Systems (CPS), where digital code meets the physical world. For a long time, scientists have been great at modeling these systems when everyone is on the same team, like a single robot arm moving perfectly. They've also gotten pretty good at modeling "two-player" games, like a self-driving car trying to avoid a pedestrian who might step out unexpectedly. In these two-player scenarios, it's a simple tug-of-war: one side wins if the other loses.

But what happens when you add a third player? Suddenly, the game changes completely. In a three-player scenario, the players can whisper to each other, form secret alliances, or decide to work together just for a moment before going their separate ways. This is the tricky part that has stumped researchers: how do you mathematically prove that a system is safe when three different agents with different goals can team up in any combination? If you assume they are always enemies (a "zero-sum" game), you might miss the fact that two of them could actually help each other, leading to overly cautious and useless safety rules. If you assume they are always friends, you might miss a dangerous betrayal. The question is: can we build a logical framework that handles this messy, shifting web of alliances and still prove the system won't crash?

This paper introduces a new mathematical tool called dGL3 (three-player Differential Game Logic) designed specifically to solve this puzzle. The authors, Julia Butte and André Platzer, have created a set of rules and a language that allows computers to verify the safety of these complex, three-way interactions. They show that even though three players can form coalitions (teams) in ways that two players cannot, the logic needed to understand them isn't actually a brand-new, unmanageable monster. Instead, they prove that you can translate any three-player game into a two-player game without losing any information.

Think of it like a game of chess where, instead of just White and Black, you have three teams. In a normal game, White and Black are enemies. But in this new game, White and Black might decide to team up against Red for a few moves, or Red might team up with White. The authors developed a "translator" that takes this chaotic three-way game and rewrites it as a standard two-player game. They proved that this translation is perfect: if you can solve the two-player version, you have solved the three-player version. This is a huge deal because it means we don't need to invent entirely new, impossible math to handle three players; we can just use the powerful tools we already have for two players, but with a clever twist.

The paper doesn't just claim this works; it provides a complete "proof calculus," which is like a step-by-step instruction manual for a computer to check these games. They demonstrated that this manual is sound (it never gives a false "safe" verdict) and relatively complete (it can prove anything that is actually true, provided the underlying math is strong enough). To show it in action, they used a scenario with a car driver, a motorcycle rider, and a gas station attendant. The car and the bike both need gas, but the attendant only has enough for one. The logic successfully figured out that the car driver can only win if they team up with the attendant, and it proved that the motorcycle rider and the car driver can never win together because their goals clash.

By breaking down the complex dynamics of three players into manageable logic, this research opens the door to verifying much more realistic and complex systems. It acknowledges that in the real world, agents (like autonomous vehicles) might cooperate or compete depending on the situation, and dGL3 gives us the mathematical lens to see through that complexity and ensure safety. The authors suggest that this approach could eventually be expanded to handle even more players, but for now, they have firmly established that three-player hybrid games are logically solvable, turning a seemingly impossible challenge into a manageable puzzle.

Technical Summary: Three-Player Differential Game Logic (dGL3)

Problem Statement

Cyber-physical systems (CPS) such as autonomous vehicles, robots, and trains increasingly operate in multi-agent environments where distinct agents possess different goals. While single-agent hybrid systems and two-player hybrid games (zero-sum or non-zero-sum) have been extensively studied, a fundamental gap exists in modeling three-player hybrid games.

The core challenge arises when three distinct CPS agents interact. Unlike two-player scenarios where coalitions effectively reduce the system to a single-player hybrid system, three-player interactions introduce a genuinely new dynamic: the ability for players to form dynamic coalitions at will. In a three-player setting, any subset of players (excluding the empty set) can form a coalition to pursue the intersection of their goals, while the remaining player(s) act adversarially. Existing logics, such as Differential Game Logic (dGL) for two players or Alternating-time Temporal Logic (ATL) for fixed coalitions, cannot adequately verify these non-zero-sum, non-hybrid, or hybrid scenarios where coalition formation is fluid and goals are individual. Specifically, zero-sum assumptions in two-player models lead to overly conservative results by neglecting the potential for coordination among players.

Methodology

The paper introduces dGL3, a logic designed to verify hybrid games involving three players with discrete jumps and differential equation dynamics. The methodology encompasses the following components:

1. Syntax and Semantics

Syntax: dGL3 extends first-order logic with real arithmetic and introduces two types of formulas: state formulas (interpreted over states) and game formulas (interpreted over tuples of states and coalitions).
- Coalitions: Represented as non-empty subsets of players $\{1, 2, 3\}$ .
- Modalities:
  - $\Diamond_C : \pi$ and $\Box_C : \pi$ : Existential and universal quantification over a set of coalitions $C$ .
  - $\langle[\alpha]\rangle(\pi)$ : A game modality where $\alpha$ is a hybrid game and $\pi$ describes the goals.
  - $\Xi(P_1, P_2, P_3)$ : A goal constructor that aggregates individual player goals into a coalition goal via conjunction.
- Hybrid Games: Operations include assignment, continuous evolution (controlled by specific players $i$ ), tests, choices, sequential composition, and repetition, all indexed by the controlling player.
Semantics: The semantics maps formulas to sets of states (for state formulas) or sets of state-coalition tuples (for game formulas).
- A coalition $c$ wins a game $\alpha$ starting from state $\omega$ if they can reach a state satisfying their aggregated goal.
- Winning Regions: Defined recursively. For a coalition $c$ controlling a game, they can choose the path. For coalitions not controlling the game, they must be prepared for the worst-case scenario (the controlling player acting adversarially).
- Fixed Points: Repetition games ( $\alpha^*_i$ ) are handled via greatest fixed points for controlling coalitions (who can choose to stop) and least fixed points for non-controlling coalitions (who must ensure safety regardless of loop duration).

2. Proof Calculus

A sound and relatively complete proof calculus is constructed for dGL3.

Axioms: The calculus includes axioms for decomposing game constructs (assignment, choice, sequence, repetition, continuous evolution) based on whether the coalition $c$ $c$ associated with the modality contains the controlling player $i$ $i$ .
- If $i \in c$ , the coalition controls the choice/evolution.
- If $i \notin c$ , the coalition faces the worst-case outcome of the controlling player's choice.
Derived Rules: Rules for sets of coalitions are derived from single-coalition rules, allowing for practical verification without exhaustive case distinctions.
Monotonicity: A monotonicity rule ensures that increasing the goal set expands the winning region.

3. Equivalence and Completeness

A central methodological contribution is the proof that three-player hybrid games reduce logically to two-player hybrid games.

Translation: The paper defines a translation function ( $\flat$ ) that maps any dGL3 formula to an equivalent dGL formula. This is achieved by grouping the coalition members into "Angel" and the remaining players into "Demon."
Relative Completeness: Since dGL is known to be relatively complete, and dGL3 is shown to be equivalent to dGL via syntactic translation, the dGL3 calculus is proven to be relatively complete with respect to any differentially expressive logic.

Key Results

Logical Equivalence: The paper proves the surprising result that the logic of three-player hybrid games is logically equivalent to the logic of two-player hybrid games:
$\text{two-player hybrid games} \equiv_{\text{logic}} \text{three-player hybrid games}$
This equivalence holds despite the added complexity of dynamic coalition formation in the three-player setting.
Soundness: The proof calculus for dGL3 is proven sound; any formula provable in the calculus is valid in all states.
Relative Completeness: The calculus is relatively complete. Any valid dGL3 formula can be proven using the calculus and axioms of a differentially expressive logic.
Monotonicity: The winning region function for hybrid games is proven to be monotone, ensuring the existence of the fixed points required for the semantics of repetition games.

Significance and Claims

The paper claims that dGL3 is the first logic capable of verifying non-zero-sum hybrid games with three players where coalitions can form dynamically.

Addressing the "Three-Player Challenge": The authors emphasize that while coalitions in two-player games trivially reduce the system to a single-player system, three-player games retain genuine multi-agent complexity even when only two players form a coalition. dGL3 addresses this specific challenge.
Avoiding Over-Conservatism: By explicitly modeling non-zero-sum goals and coalition possibilities, dGL3 avoids the overly conservative results produced by zero-sum assumptions, which ignore the potential for coordination among players.
Versatility: The logic is shown to be versatile enough to handle the "coalitional power" of three players, establishing that the reasoning principles of two-player games are sufficient to tame three-player dynamics.
Future Scope: The authors note that the fundamental challenges of $n$ -player games are already present in the three-player case, suggesting that dGL3 provides a foundation for extending verification to $n$ -player scenarios.

The paper illustrates these capabilities through a canonical example involving a car driver, a motorcycle rider, and a gas station attendant, demonstrating how coalition formation (e.g., the driver teaming up with the attendant) allows for winning strategies that would be impossible or unprovable under strict zero-sum or fixed-coalition assumptions.