Playing Hybrid Games with KeYmaera

We propose a new logic, called differential dynamic game logic (dDGL), that adds several game constructs on top of differential dynamic logic (dL) so that it can be used for hybrid games. The logic dDGL is a conservative extension of dL, which we exploit for our implementation of dDGL in the theorem prover KeYmaera. We provide rules for extending the dL sequent proof calculus to handle the dDGL constructs by identifying analogs to operators of dL. We have implemented dDGL in an extension of KeYmaera and verified a case study in which a robot satisfies a joint safety and liveness objective in a factory automation scenario, in which the factory may perform interfering actions independently.

• Type: Journal
• Year: 2012
• Where: CADE
• Authors: Jan-David Quesel, André Platzer
• Keywords: CADE 2012, Conservative Extension, Dynamic Logic, Game Logic, Logical Reasoning