Название: Formal Methods for Control of Nonlinear Systems
Автор: Yinan Li, Jun Liu
Издательство: CRC Press
Год: 2023
Страниц: 272
Язык: английский
Формат: pdf (true)
Размер: 14.97 MB

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.

The main aim of this book is to present formal methods for control of nonlinear dynamical systems with theoretical guarantees. We consider both continuous-time and discrete-time dynamical systems whose states evolve in continuous state spaces. Such models are paramount to control and robotics applications. The specifications we consider are general ω-regular properties that concern the infinite time-horizon behaviors of dynamical systems, which include relatively simple but useful properties of safety, invariance, reachability, reach-avoid (reachability with safety), as well as more complex specifications described by linear temporal logic (LTL). We embrace the fact that, in general, it is impossible to exactly determine if an ω-regular property is satisfiable by a nonlinear control system. Indeed, even reachability is undecidable for low-dimensional continuous or simple hybrid system models. Instead, we seek to answer the question whether a robust controller can be found to enforce the property in the presence of small perturbations to the dynamical system under control, provided that certain robust controllers do exist. We call such algorithms robustly complete.

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.