Differential Game Logic for Hybrid Games

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 2012
Accession Number
ADA561153

Entities

People

  • AndrĂ© Platzer

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Calculus
  • Computer Science
  • Computers
  • Differential Equations
  • Dynamics
  • Equations
  • Game Theory
  • Hybrid Systems
  • Logic
  • Mathematics
  • Numbers
  • Semantics
  • Sequences
  • Social Sciences
  • Theorems
  • Topology
  • Zero-Sum Games

Fields of Study

  • Computer science

Readers

  • Game Theory.
  • Mathematical Modeling and Probability Theory.