Koopman-based Implicit Backward Reachable Sets for Unknown Nonlinear SystemsH. Balim, A. Aspeel, Z. Liu, and N. Ozay Koopman liftings have been successfully used to learn high dimensional linear approximations for autonomous systems for prediction purposes, or for control systems for leveraging linear control techniques to control nonlinear dynamics. In this paper, we show how learned Koopman approximations can be used for state-feedback correct-by-construction control. To this end, we introduce the Koopman over-approximation, a (possibly hybrid) lifted representation that has a simulation-like relation with the underlying dynamics. Then, we prove how successive application of controlled predecessor operation in the lifted space leads to an implicit backward reachable set for the actual dynamics. Finally, we demonstrate the approach on two nonlinear control examples with unknown dynamics. Why this is a challenging problem? Our main contributions include a relation between the original and lifted system, namely Koopman-overapproximations, and an appropriate lifted set representation, namely psi-implicit inner approximations, which together are shown to guarantee that inner-approximations of BRSs can be computed. There are several challenges in regards to set representations specific to backward reachability: 1) we need a representation in the lifted space that is amenable to linear computations (e.g., polyhedra), 2) we need to inner-approximate backward reachable sets (BRSs), which is crucial in backward reachability and for controller extraction, 3) naively lifting a polytopic set results in a lifted set that lives in a nonlinear low dimensional manifold, which is hard to manipulate, hard to inner-approximate with a nice object, and hard to reach with uncertain dynamics. Note that these challenges do not exist in using Koopman-liftings for stability (since there is no need to represent sets) or for forward reachability (as naive lifting can be easily over-approximated by nicer sets like polyhedra and forward reachability requires over-approximations), hence were not addressed in the literature before. Additionally, our use of local liftings to reduce conservativeness is motivated by our recent work where we show that continuous global liftings do not exist in general for nonlinear systems, in particular, when there are multiple omega limit sets, hence some hybridization is needed. |