Event
Formal Methods for Nonlinear Control: A Robustness Perspective
Virtual Informal Systems Seminar (VISS) Centre for Intelligent Machines (CIM) and Groupe d'Etudes et de Recherche en Analyse des Decisions (GERAD)
Speaker: Jun Liu, Associate Professor, Applied Mathematics, University of Waterloo
Abstract: Formal methods for control aim to synthesize controllers for continuous dynamical systems to meet high-level specifications. Finite abstractions, also known as symbolic models, have provided useful means for algorithmically synthesizing hybrid controllers with respect to rigorous specifications (e.g., safety, reachability, or more generally a temporal logic formula). A central theoretical question surrounding abstraction-based control is whether one can decide, through finite abstractions and discrete synthesis, the existence of a controller for a nonlinear system to satisfy a given specification. This question may also have practical implications towards addressing the inherent scalability issues of abstraction-based approaches.
In this talk, we discuss some recent results towards answering this question. We first introduce a method to synthesize robust controllers for temporal logic formulas using finite abstractions. We then use this notion of robustness to show that, if a system robustly satisfies a given specification, then it is possible to use discrete abstractions to synthesize a robust controller. Following this, we present a specification-guided framework to improve the computational performance of abstraction-based methods, while providing the same theoretical guarantees. We conclude by arguing that the intrinsic robustness and controllability of the underlying dynamical system can and should be exploited to address the scalability issues caused by discretization of continuous dynamics and to mitigate the combinatorial explosion imposed by logic specifications.
Biography: Jun Liu is an Associate Professor in Applied Mathematics at the University of Waterloo. He received the Ph.D. degree in Applied Mathematics from the University of Waterloo in 2011. From 2011 to 2012, he held an NSERC Postdoctoral Fellowship in Control and Dynamical Systems at Caltech. From 2012 to 2015, he was a Lecturer in Control and Systems Engineering at the University of Sheffield. His 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 Tier 2 Canada Research Chair from the Government of Canada in 2017, an Ontario Early Researcher Award in 2018, and an Early Career Award from the Canadian Applied and Industrial Mathematics Society and Pacific Institute for the Mathematical Sciences (CAIMS/PIMS) in 2020. He was a co-recipient of the Nonlinear Analysis: Hybrid Systems Paper Prize at the 2017 IFAC World Congress.
Abstract: Formal methods for control aim to synthesize controllers for continuous dynamical systems to meet high-level specifications. Finite abstractions, also known as symbolic models, have provided useful means for algorithmically synthesizing hybrid controllers with respect to rigorous specifications (e.g., safety, reachability, or more generally a temporal logic formula). A central theoretical question surrounding abstraction-based control is whether one can decide, through finite abstractions and discrete synthesis, the existence of a controller for a nonlinear system to satisfy a given specification. This question may also have practical implications towards addressing the inherent scalability issues of abstraction-based approaches.
In this talk, we discuss some recent results towards answering this question. We first introduce a method to synthesize robust controllers for temporal logic formulas using finite abstractions. We then use this notion of robustness to show that, if a system robustly satisfies a given specification, then it is possible to use discrete abstractions to synthesize a robust controller. Following this, we present a specification-guided framework to improve the computational performance of abstraction-based methods, while providing the same theoretical guarantees. We conclude by arguing that the intrinsic robustness and controllability of the underlying dynamical system can and should be exploited to address the scalability issues caused by discretization of continuous dynamics and to mitigate the combinatorial explosion imposed by logic specifications.
Biography: Jun Liu is an Associate Professor in Applied Mathematics at the University of Waterloo. He received the Ph.D. degree in Applied Mathematics from the University of Waterloo in 2011. From 2011 to 2012, he held an NSERC Postdoctoral Fellowship in Control and Dynamical Systems at Caltech. From 2012 to 2015, he was a Lecturer in Control and Systems Engineering at the University of Sheffield. His 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 Tier 2 Canada Research Chair from the Government of Canada in 2017, an Ontario Early Researcher Award in 2018, and an Early Career Award from the Canadian Applied and Industrial Mathematics Society and Pacific Institute for the Mathematical Sciences (CAIMS/PIMS) in 2020. He was a co-recipient of the Nonlinear Analysis: Hybrid Systems Paper Prize at the 2017 IFAC World Congress.
