Verifying Nonlinear Systems Using Koopman Operator Linearization

Koopman operator linearization approximates a nonlinear system of differential equations as a higher-dimensional linear system. This is attractive since many types of analysis, including formal verification using reachability analysis, are significantly more tractable for linear systems.

However, three key challenges remain with the approach, which will be covered during the talk: (i) There are (infinitely?) many hyperparameters when performing Koopman operator linearization. Can we do it automatically and accurately? (ii) Although linear systems are easier to analyze, the initial set of states for a Koopman-linearized system is defined using a complex nonlinear mapping. Can this modified verification problem still be solved efficiently? (iii) What good is it to verify an approximation? What can be done to increase confidence in the correctness of the verification result?