Case Study: Verification of nonzero-sum hybrid games

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.

The aim of this thesis is to develop a case study by modeling the case as nonzero-sum hybrid game in dGLsc and then verifying its safety. The topic for the case study can be chosen freely. A possible case could be to verify that two autonomous cars that meet at an intersection, can cross it without colliding. In this example, the two players are the two cars. The game involves the cars to decide whether they want to drive now, or wait, in order to let the other car pass, and then drive. They both share the goal that they do not want to collide while also wanting to reach their respective other side of the road (which is different for each player). Depending on the complexity of the case study, this can be either a bachelor’s or a master’s thesis.

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