Dr. Jun Liu

In many safety-critical cyber-physical systems, it is important to ensure that the system behaves as intended and meets desired specifications. Formal methods for control aim to synthesize controllers for dynamical systems to meet high-level specifications with provable satisfaction guarantees.

In the first part of this talk, we will discuss our recent work on formal control of nonlinear systems using temporal logic specifications. Both theoretical guarantees and practical implementations relevant to formal methods for nonlinear control will be addressed. The computational techniques will be illustrated with applications drawn from robotics and control. We will also discuss extensions of such frameworks to systems with stochastic dynamics.

In the second part of the talk, we will connect formal specifications with classical Lyapunov theory. We will introduce a notion of Lyapunov-barrier functions that can be used for verification and control with reach-avoid type specifications, serving as a building block for certifying more complex behaviors. Constructing Lyapunov functions has long been a known challenge in control. To address this challenge, we will present our recent work on learning and verifying neural Lyapunov certifications.

Biography:

Dr. 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 holds a Tier 2 Canada Research Chair in Hybrid Systems and Control since 2017 and was awarded 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.