Applying Koopman Methods for Nonlinear Reachability Analysis

In this thesis we investigate the possibilities for applying Koopman methods for reachability analysis. Reachability analysis is a verification process used to determine that a dynamical system starting in an initial set X0 cannot reach a certain set of dangerous states D within a time interval [0,T]. Koopman methods seem promising, because they predict nonlinear behaviour using linear techniques. However they have not been widely applied to reachability analysis.We describe three different Koopman methods: data-driven, Polyflow and Carleman. We use the Polyflow method combined with ideas from several other methods to create a new reachability tool: PolyReach. Next, we analyse the performance of PolyReach by comparing it with a state-of-the-art reachability algorithm Flow* on various nonlinear systems. Finally, we summarize the strengths and weaknesses of the PolyReach tool and discuss ideas for further improvement.Mechanical Engineering | Systems and Contro