Logic for Hybrid Games

Differential Game Logic

Differential game logic (dGL) is a logic for specifying and verifying properties of hybrid games, i.e. games that combine discrete, continuous, and adversarial dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players with different objectives. The logic dGL can be used to study the existence of winning strategies for such hybrid games, i.e. ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e. from each state, one player has a winning strategy, yet computing their winning regions may take transfinitely many steps. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic. Separating axioms are identified that distinguish hybrid games from hybrid systems. Finally, dGL is proved to be strictly more expressive than the corresponding logic of hybrid systems by characterizing the expressiveness of both.

Keywords: differential game logic, game logic, hybrid games, axiomatization, expressiveness

Differential game logic
Differential game logic for hybrid games is implemented in the KeYmaera X theorem prover.

Differential Hybrid Games

This paper introduces differential hybrid games, which combine differential games with hybrid games. In both kinds of games, two players interact with continuous dynamics. The difference is that hybrid games also provide all the features of hybrid systems and discrete games, but only deterministic differential equations. Differential games, instead, provide differential equations with input by both players, but not the luxury of hybrid games, such as mode switches and discrete or alternating interaction. This paper augments differential game logic with modalities for the combined dynamics of differential hybrid games. It shows how hybrid games subsume differential games and introduces differential game invariants and differential game variants for proving properties of differential games inductively.

Keywords: differential games, hybrid games, differential game game logic, differential game invariants, partial differential equations, viscosity solutions, real algebraic geometry



  1. André Platzer.
    Differential hybrid games.
    ACM Trans. Comput. Log. To appear. © The author
    [bib | pdf | arXiv | abstract]

  2. André Platzer.
    Differential game logic.
    ACM Trans. Comput. Log. 17(1), pp. 1:1-1:52, 2015. © The author
    [bib | pdf | doi | arXiv | abstract]

  3. André Platzer.
    Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-105, March 2012.
    Also see new results.
    [bib | pdf | TOCL'15 | abstract]