Sciweavers

CADE
2012
Springer

Playing Hybrid Games with KeYmaera

12 years 2 months ago
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.
Jan-David Quesel, André Platzer
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where CADE
Authors Jan-David Quesel, André Platzer
Comments (0)