Case Study: Verification of robot motions from a differential geometric perspective

Formalizing hybrid dynamical systems can be extremely complex due to their geometric behavior. For example, modeling robot motions in differential dynamic logic (dL) requires adding constraints to ensure that the positions are sound. In such cases, it can be useful to model the behavior not on the reals, but on a manifold. In the example of robots, this would be SE(3), the configuration space. If, additionally, the underlying manifold is a group, we call it a Lie group. For example, SE(3) is also a group—the group of rigid body motions. We are currently developing a generalization of dL that allows variables to have a manifold (or Lie group), tangent vector (or Lie algebra), or real type. The aim of this thesis is to formalize the dynamics of a robot (or a drone) on the Lie group SE(3). A concrete example can be chosen freely, but it should highlight the advantages of verifying the dynamics on SE(3) rather than purely on the reals. This thesis may be suitable for mathematics and computer science students. It is required that you are either familiar with basic differential geometry and dynamic logic, or are willing to acquire the necessary knowledge.

For more information, please reach out to vivien.ebert@kit.edu.