CMU-CS-13-100
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-13-100

A Complete Axiomatization of Differential Game Logic
for Hybrid Games

André Platzer

January 2013

This report is an updated version of Computer Science Department
Technical Report CMU-CS-12-105.

An updated version (July 2013) is also available as Computer Science Department
Technical Report CMU-CS-13-100R.pdf

Also appears as: Differential Game Logic
http://dx.doi.org/10.1145/2817824, 2015

CMU-CS-13-100.pdf


Keywords: Game logic, hybrid dynamical systems, hybrid games, axiomatization

We introduce differential game logic (dGL) for specifying and verifying properties of hybrid games, i.e. games on hybrid systems combining discrete and continuous 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. We present a simple sound and complete axiomatization of dGL relative to the fixpoint logic of differential equations. We prove hybrid games to be determined and their winning regions to require higher closure ordinals and we identify separating axioms, i.e. axioms that distinguish hybrid games from hybrid systems.

52 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu