Speaker: André Platzer, KIT University Karlsruhe
Time: Wednesday 17 June 2026, 14:00am
Place: Room to be announced, ENS Paris-Saclay
Abstract: This talk highlights some of the most fascinating aspects of the logic of hybrid games, which constitute the foundation for developing multi-agent cyber-physical systems (CPS) such as robots, cars and aircraft, with the mathematical rigor that their safety-critical nature demands. Differential game logic (dGL) provides an integrated specification and verification language for hybrid games that combine discrete transitions and continuous evolution along differential equations with adversarial dynamics resolved by different players with different objectives. dGL can be used to study the existence of winning strategies for 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., one player has a winning strategy from each state, yet their winning regions may require transfinite closure ordinals. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic.
In addition to providing a strong theoretical foundation for CPS, differential game logic as implemented in the KeYmaera X prover has been instrumental in verifying the multi-aircraft dynamics of the Federal Aviation Administration's Airborne Collision Avoidance System ACAS X and constitutes the foundation for control envelope synthesis in hybrid systems.
References:
André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. DOI:10.1007/978-3-319-63588-0
André Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), pp. 1:1-1:52, 2015. DOI:10.1145/2817824
André Platzer. Differential hybrid games. ACM Trans. Comput. Log. 18(3), pp. 19:1-19:44, 2017. DOI:10.1145/3091123