Constructive Hybrid Games

Abstract

Hybrid games are models which combine discrete, continuous, and adversarial dynamics. Game logic enables proving (classical) existence of winning strategies. We introduce constructive differential game logic (CdGL) for hybrid games, where proofs that a player can win the game correspond to computable winning strategies. This is the logical foundation for synthesis of correct control and monitoring code for safety-critical cyber-physical systems. Our contributions include novel static and dynamic semantics as well as soundness and consistency.

arXiv comment60 pages, preprint, under review

References in corpus (7)

• Differential Equation Invariance Axiomatization
• Differential Game Logic
• Differential Hybrid Games
• Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism
• An Axiomatic Approach to Liveness for Differential Equations
• Uniform Substitution for Differential Game Logic
• Constructive Game Logic

Cited by in corpus (1)

• Structured Proofs for Adversarial Cyber-Physical Systems