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.
Author(s): Yinan Li, Jun Liu
Publisher: CRC Press/Chapman & Hall
Year: 2022
Language: English
Pages: 270
City: Boca Raton
Cover
Half Title
Title Page
Copyright Page
Dedication
Contents
Preface
About the Authors
List of Symbols
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.4.1. Translating LTL to Büchi Automata
3.5. Formulation of Control Problems
3.5.1. Control of Nondeterministic Transition Systems
3.5.2. Control of Discrete-Time Dynamical Systems
3.5.3. Control of Continuous-Time Dynamical Systems
3.6. Discrete Synthesis
3.6.1. Safety
3.6.2. Reachability
3.6.3. ω-Regular Properties
3.7. Summary
4. Interval Computation
4.1. Interval Analysis
4.1.1. Inclusion Functions
4.1.2. Mean-Value and Taylor Inclusion Functions
4.1.3. Inclusion Functions based on Mixed Monotonicity
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.3.1. A Priori Enclosure
4.3.2. Over-Approximations by Lipschitz Growth Bound
4.3.3. Over-Approximations by Mixed Monotonicity
4.3.4. Over-Approximations by Validated Integration
4.3.5. Examples
4.4. Interval Under-approximations of Controlled Predecessors of Discrete-Time Systems
4.5. Interval Under-approximations of Controlled Predecessors of Continuous-Time System
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.4.1. Soundness and Robust Completeness
5.5. Summary
5.5.1. A Brief Account of Formal Methods for Control
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.6.1. Winning Set Characterization on the Continuous State Space
6.6.2. Completeness via Robustness
6.6.3. Sound Control Synthesis for Full LTL
6.6.4. Specification Pre-Processing
6.7. Extension to Continuous-Time Dynamical Systems
6.8. Complexity Analysis
6.8.1. Control Synthesis with Simple Specifications
6.8.2. Control Synthesis with DBA Specifications
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.4.1. Parallel Parking
7.4.2. Motion Planning
7.5. Online Obstacle Avoidance
7.5.1. Offline Control Synthesis
7.5.2. Online Replanning
7.5.3. Simulation
7.6. Robotic Manipulator
7.7. Bipedal Locomotion
7.7.1. Hybrid System Model of Bipedal Locomotion
7.7.2. Hierarchical Reactive Planning Strategy
7.7.3. Robust Switching Between Locomotion Modes
7.7.4. Simulation
7.8. Summary
A. Basic Theory of Ordinary Differential Equations
A.1. Initial Value Problem and Carathéodory Solutions
A.2. Existence and Uniqueness Theorem
A.3. Global Existence
A.4. Differential Inequalities and a Comparison Theorem
B. Interval Analysis
B.1. Proof of Convergence for Taylor Inclusions (Proposition 4.6)
B.1.1. Proof of Proposition 4.6
C. Basic Set Theory
C.1. Set Convergence
C.2. Heine-Borel Theorem
C.3. Minkowski Sum and Minkowski Difference
C.4. Proof of Proposition 6.2
C.5. Proof of Proposition 6.3
C.6. Proof of Proposition 6.4
D. Mappings of Locomotion Modes
Bibliography
Index
