CMU-CS-12-105
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-12-105

Differential Game Logic for Hybrid Games

André Platzer

March 2012

CMU-CS-12-105.pdf

An updated version of this report is available as
Computer Science Department Technical Report CMU-CS-13-100.pdf

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


Keywords: Dynamic logic, game logic, hybrid games, hybrid dynamical systems, proof calculus

We introduce differential game logic (dGL) for specifying and verifying properties of hybrid games, i.e., determined, sequential/dynamic, non-cooperative, zero-sum games of perfect information on hybrid systems that combine discrete and continuous dynamics. Unlike hybrid systems,hybrid games allow choices in the system dynamics to be resolved by different players with different objectives. The logic dGL can be used to study properties of the resulting adversarial behavior. It unifies differential dynamic logic for hybrid systems with game logic. We define a regular modal semantics for dGL, present a proof calculus for dGL, and prove soundness. We identify separating axioms, i.e., the axioms that distinguish dGL and its game aspects from logics for hybrid systems. We also define an operational game semantics, prove equivalence, and prove determinacy.

25 pages



Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu