Formal Controller Synthesis for Dynamical Systems: Decidability and Scalability

In this talk, I will discuss formal controller synthesis for three different classes of dynamical systems. First, I will address our contributions to improving the scalability of abstraction-based controller design methods for dynamical systems with continuous state spaces and bounded uncertainty. These contributions include: (1) a data-driven scheme for relaxing the requirement of having analytical model, (2) a neural abstraction method to lower memory requirements of both synthesis and deployment, and (3) a scalable method for solving reach-avoid problems for multi-agent systems. Second, I will briefly describe our contributions to time-bounded model checking for continuous-time Markov decision processes, specifically: (1) a conditional decidability result, and (2) a systematic method for improving the scalability of numerical approximation methods. Finally, I will briefly discuss our results related to the decidability of reachability-related problems for linear dynamical systems, which include: (1) a hardness result for point-to-point reachability of linear dynamical systems with hyper-rectangular control sets, and (2) decidability of pseudo-reachability for hyperplane target sets.