Implementation of semi-competitive hybrid games for KeYmaera X

Cyber-phyiscal systems (CPS) like trains, planes, autonomous cars or robots need verification to ensure their safety. Especially relevant are situations involving two CPSs, as these situations occur frequently in real-world. The challenging aspects here are the possible interactions between the CPSs that arise from their intentions or goals. The logic dGLsc which has been developed in our group, deals with these situations by regarding them as games and the involved CPSs as players, each with an individual goal they try to reach. In order to achieve their goal, the two players may collaborate with each other when helpful and may compete when necessary. Therefore, dGLsc is able to naturally model interactions involving two CPSs by taking both of their goals into account, enabling an accurate verification of the situation.

To verify even large formulas in dGLsc, it is helpful to have a theorem prover that can partially automatically prove formulas and supports manual manipulation of formulas. Therefore, in this thesis, reasoning with dGLsc should be implemented in the existing theorem prover KeYmaera X. Optionally, the uniform substitution calculus for dGLsc which serves as the basis for implementation, can also be derived in the thesis.

For more information, please reach out to julia.butte@kit.edu.