MC
6460
Candidate
Yinan Li | Applied Mathematics, University of Waterloo
Title
Robustly Complete Temporal Logic Control Synthesis for Nonlinear Systems
Abstract
Modern systems such as spacecrafts and autonomous vehicles are complex yet safety critical, which leads to the rising demand of the control methods that can deal with different dynamics and constraints while being provably correct. Formal methods are rigorous techniques originally used for developing and verifying finite-state systems with respect to specifications in formal languages. This thesis is concerned with using formal methods in control synthesis for nonlinear systems, which can guarantee the correctness of the resulting control strategies.
For nonlinear continuous-state dynamical systems, formal control synthesis relies on finite abstractions of the original system by discretizing the system state space and over approximating system transitions. Without further assumptions, control synthesis is usually not complete in the way that no control strategies can be found even if there exists one. To deal with this problem, this thesis proposes a formal control synthesis approach that is sound and robustly complete in the sense that correct control strategies can be found whenever the specifications can be realized for the system with additional disturbance.
Fundamental to the soundness and robust completeness is a fixed-point characterization of the winning set of the system with respect to a given specification, which is the set of initial conditions that can be controlled to satisfy the specification. Regarding discrete-time systems, we show that such characterizations not only apply to basic invariance, reachability and reach-and-stay specifications but also the class of LTL formulas that can be translated into deterministic B\"uchi automata (DBA).
Because of the general nonlinearity, exact computation of winning sets is currently almost impossible. In this work, the conditions for set approximations are derived so that control synthesis is robustly complete. To meet such conditions, the proposed approach adopts interval arithmetic and a subdivision scheme in winning set approximation. Under such a scheme, the system state space is adaptively partitioned without failing the precision requirement to satisfy the robust completeness conditions. The proposed method is also shown applicable to sampled-data systems by computing validated solutions over one sampling period based on high-order Taylor expansion.
Applications such as converter voltage regulation, parallel parking, and reactive locomotion planning problems are studied to show the effectiveness and efficiency of the proposed approach.