Formal stabilization of a coupled ODE-PDE switched system

Partial Differential Equations (PDEs) are a ubiquitous model that describes a wide range of dynamical systems. While stabilization of systems involving PDEs is an important problem, little work has been done on formal verification and synthesis for such systems. In this paper, we explain how a coupled ODE-PDE control problem can be formally stabilized using a tiling based control synthesis algorithm associated to set based reachability, which is usually used on finite dimensional problems. To formally prove the stabilization of the PDE, the original infinite dimensional problem is transformed into a finite dimensional one using, among other tools, model order reduction. The strength of our approach relies on the fact that we never explicitly discretize the PDE state using e.g. a finite element approximation, and consequently, we provide stability guarantees directly on the infinite dimensional state.