Variations of Nagumo's Theorem

Given a dynamical system (i.e., the equations of motions of a cyber-physical system that describe how it can move through space), an invariant set is a region of space with the property that any system that starts within that set, remains in that region forever. This property is very useful when trying to stabilize autonomous systems, e.g., if an autonomous vehicle needs to follow a trajectory despite disturbances arising from the wind etc. In this context, the Nagumo theorem is a famous result that provides an equivalent characterization of invariant sets, which in certain situations can be expressed as an optimization problem that can be solved numerically. This is the case for ellipsoids and V-polytopes, but recent advances have extended this idea to zonotopes, with some limitations.

The purpose of this study is to generalize this method even more, through a rigorous formalization of Nagumo’s theorem in differential dynamic logic, which would enable a characterization of open and noncompact invariants, something that was out of reach of the original formulation of Nagumo’s theorem.

This topic involves a combination of optimization theory and deductive verification, specifically differential dynamic logic. Applicants should have some proficiency with first-order logic, and some basic knowledge about ordinary differential equations (ODEs).

For more information, please reach out to adrian.kulmburg@kit.edu.