Formal Methods for Control of Nonlinear Systems

Formal methods is a field of computer science that emphasizes the use of rigorous mathematical techniques for verification and design of hardware and software systems. Analysis and design of nonlinear control design plays an important role across many disciplines of engineering and applied sciences, ranging from the control of an aircraft engine to the design of genetic circuits in synthetic biology. While linear control is a well-established subject, analysis and design of nonlinear control systems remains a challenging topic due to some of the fundamental difficulties caused by nonlinearity. Formal Methods for Control of Nonlinear Systems provides a unified computational approach to analysis and design of nonlinear systems. Features - Constructive approach to nonlinear control. - Rigorous specifications and validated computation. - Suitable for graduate students and researchers who are interested in learning how formal methods and validated computation can be combined together to tackle nonlinear control problems with complex specifications from an algorithmic perspective. - Combines mathematical rigor with practical applications.

Jun Liu received the B.S. degree in applied mathematics from Shanghai Jiao-Tong University in 2002, the M.S. degree in mathematics from Peking University in 2005, and the Ph.D. degree in applied mathematics from the University of Waterloo in 2011. Following an NSERC Postdoctoral Fellowship in Control and Dynamical Systems at Caltech, he became a Lecturer in Control and Systems Engineering at the University of Sheffield in 2012. He joined the Faculty of Mathematics of the University of Waterloo in 2015, where he currently is an Associate Professor of Applied Mathematics and directs the Hybrid Systems Laboratory. Dr. Liu's main research interests are in the theory and applications of hybrid systems and control, including rigorous computational methods for control design with applications in cyber-physical systems and robotics. He was awarded a Marie-Curie Career Integration Grant from the European Commission in 2013, a Canada Research Chair from the Government of Canada in 2017 and 2022, an Early Researcher Award from the Ontario Ministry of Research, Innovation and Science in 2018, and an Early Career Award from the Canadian Applied and Industrial Mathematics Society and Pacific Institute for the Mathematical Sciences in 2020. His best paper awards include the Zhang Si-Ying Outstanding Youth Paper Award and the Nonlinear Analysis: Hybrid Systems Paper Prize. Dr. Liu is a senior member of IEEE, a member of SIAM, and a lifetime member of CAIMS. He has served on the editorial boards and program committees of several journals and conferences, including Automatica, Nonlinear Analysis: Hybrid Systems, Systems & Control Letters, the ACM International Conference on Hybrid Systems: Computation and Control (HSCC), the IEEE Conference on Decision and Control (CDC), and the American Control Conference (ACC). Yinan Li is a senior autonomy developer at OTTO Motors-the industrial division of Clearpath Robotics- in Kitchener, Ontario, Canada. She works on navigation algorithms for industrial mobile robots, multi-robot traffic control and coordination. Before joining OTTO Motors, she was a post-doctoral fellow at Hybrid Systems Laboratory, shortly after she received her Ph.D. degree in applied mathematics from University of Waterloo in 2019. Her Ph.D. and post-doctoral research focused on formal control methods for nonlinear systems, and joint research with Georgia Institute of Technology and Clearpath Robotics were about applications of formal control methods in humanoid and mobile robots. She was awarded the 2020 Huawei prize for best research paper for her research in this area.

1. Continuous-Time Dynamical Systems. 1.1. Continuous-Time Control System. 1.2. Existence of Local and Global Solutions. 1.3. Stability and Boundedness. 1.4. Safety and Reachability. 1.5. Control Lyapunov Functions. 1.6. Summary. 2. Discrete-Time Dynamical Systems. 2.1. Discrete-Time Control Systems. 2.2. Stability and Boundedness. 2.3. Safety and Reachability. 2.4. Summary. 3. Formal Specifications and Discrete Synthesis. 3.1. Transition Systems. 3.2. Linear-Time Properties. 3.3. Linear Temporal Logic. 3.4. --Regular Properties. 3.5. Formulation of Control Problems. 3.6. Discrete Synthesis. 3.7. Summary. 4. Interval Computation. 4.1. Interval Analysis 4.2. Interval Over-Approximations of One-Step Forward Reachable Sets of Discrete-Time Systems. 4.3. Interval Over-Approximations of One-Step Forward Reachable Sets of Continuous-Time Systems. 4.4. Interval Under-approximations of Controlled Predecessors of Discrete-Time Systems. 4.5. Interval Under-approximations of Controlled Predecessors of Continuous-Time Systems. 4.6. Summary. 5. Controller Synthesis via Finite Abstractions. 5.1. Control Abstractions. 5.2. Soundness. 5.3. Completeness via Robustness. 5.4. Extension to Continuous-Time Dynamical Systems. 5.5. Summary. 6. Specification-Guided Controller Synthesis via Direct Interval Computation. 6.1. Discrete-Time Dynamical Systems. 6.2. Properties of Controlled Predecessors. 6.3. Invariance Control. 6.4. Reachability Control. 6.5. Reach-and-Stay Control. 6.6. Temporal Logic Specifications. 6.7. Extension to Continuous-Time Dynamical Systems. 6.8. Complexity Analysis. 6.9. Summary. 7. Applications and Case Studies. 7.1. DC-DC Boost Converter. 7.2. Estimation of Domains-of-Attraction. 7.3. Control of the Moore-Greitzer Engine. 7.4. Mobile Robot Motion Planning. 7.5. Online Obstacle Avoidance. 7.6. Robotic Manipulator. 7.7. Bipedal Locomotion. 7.8. Summary.