Case Study: The significance of choosing the right model

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. In some cases, there might be different manifolds that are suitable for formalization. For example, one could also use (dual) quaternions to formalize robot motions. This thesis should find an example (either the one mentioned or another) that highlights the significance of choosing the right model in terms of complexity. 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.