Muutke küpsiste eelistusi

E-raamat: Formal Methods for Control of Nonlinear Systems [Taylor & Francis e-raamat]

(University of Waterloo, Canada),
  • Formaat: 254 pages, 9 Tables, black and white; 46 Line drawings, black and white; 46 Illustrations, black and white
  • Ilmumisaeg: 15-Dec-2022
  • Kirjastus: Chapman & Hall/CRC
  • ISBN-13: 9780429270253
  • Taylor & Francis e-raamat
  • Hind: 143,10 €*
  • * hind, mis tagab piiramatu üheaegsete kasutajate arvuga ligipääsu piiramatuks ajaks
  • Tavahind: 204,43 €
  • Säästad 30%
  • Formaat: 254 pages, 9 Tables, black and white; 46 Line drawings, black and white; 46 Illustrations, black and white
  • Ilmumisaeg: 15-Dec-2022
  • Kirjastus: Chapman & Hall/CRC
  • ISBN-13: 9780429270253
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.
Preface xi
About the Authors xv
List of Symbols
xvii
1 Continuous-Time Dynamical Systems
1(20)
1.1 Continuous-Time Control System
1(1)
1.2 Existence of Local and Global Solutions
2(3)
1.3 Stability and Boundedness
5(7)
1.4 Safety and Reachability
12(5)
1.5 Control Lyapunov Functions
17(1)
1.6 Summary
18(3)
2 Discrete-Time Dynamical Systems
21(6)
2.1 Discrete-Time Control Systems
21(1)
2.2 Stability and Boundedness
21(3)
2.3 Safety and Reachability
24(1)
2.4 Summary
25(2)
3 Formal Specifications and Discrete Synthesis
27(26)
3.1 Transition Systems
27(2)
3.2 Linear-Time Properties
29(1)
3.3 Linear Temporal Logic
29(3)
3.4 w-Regular Properties
32(4)
3.4.1 Translating LTL to Biichi Automata
33(3)
3.5 Formulation of Control Problems
36(4)
3.5.1 Control of Nondeterministic Transition Systems
36(2)
3.5.2 Control of Discrete-Time Dynamical Systems
38(1)
3.5.3 Control of Continuous-Time Dynamical Systems
39(1)
3.6 Discrete Synthesis
40(11)
3.6.1 Safety
40(2)
3.6.2 Reachability
42(2)
3.6.3 w-Regular Properties
44(7)
3.7 Summary
51(2)
4 Interval Computation
53(38)
4.1 Interval Analysis
53(11)
4.1.1 Inclusion Functions
54(5)
4.1.2 Mean-Value and Taylor Inclusion Functions
59(1)
4.1.3 Inclusion Functions based on Mixed Monotonicity
60(4)
4.2 Interval Over-Approximations of One-Step Forward Reachable Sets of Discrete-Time Systems
64(2)
4.3 Interval Over-Approximations of One-Step Forward Reachable Sets of Continuous-Time Systems
66(12)
4.3.1 A Priori Enclosure
66(1)
4.3.2 Over-Approximations by Lipschitz Growth Bound
67(3)
4.3.3 Over-Approximations by Mixed Monotonicity
70(5)
4.3.4 Over-Approximations by Validated Integration
75(1)
4.3.5 Examples
75(3)
4.4 Interval Under-approximations of Controlled Predecessors of Discrete-Time Systems
78(6)
4.5 Interval Under-approximations of Controlled Predecessors of Continuous-Time System
84(4)
4.6 Summary
88(3)
5 Controller Synthesis via Finite Abstractions
91(14)
5.1 Control Abstractions
91(1)
5.2 Soundness
92(2)
5.3 Completeness via Robustness
94(4)
5.4 Extension to Continuous-Time Dynamical Systems
98(3)
5.4.1 Soundness and Robust Completeness
99(2)
5.5 Summary
101(4)
5.5.1 A Brief Account of Formal Methods for Control
102(3)
6 Specification-Guided Controller Synthesis via Direct Interval Computation
105(50)
6.1 Discrete-Time Dynamical Systems
105(1)
6.2 Properties of Controlled Predecessors
106(3)
6.3 Invariance Control
109(8)
6.4 Reachability Control
117(6)
6.5 Reach-and-Stay Control
123(6)
6.6 Temporal Logic Specifications
129(16)
6.6.1 Winning Set Characterization on the Continuous State Space
130(5)
6.6.2 Completeness via Robustness
135(6)
6.6.3 Sound Control Synthesis for Full LTL
141(1)
6.6.4 Specification Pre-Processing
142(3)
6.7 Extension to Continuous-Time Dynamical Systems
145(4)
6.8 Complexity Analysis
149(3)
6.8.1 Control Synthesis with Simple Specifications
150(1)
6.8.2 Control Synthesis with DBA Specifications
151(1)
6.9 Summary
152(3)
7 Applications and Case Studies
155(50)
7.1 DC-DC Boost Converter
155(3)
7.2 Estimation of Domains-of-Attraction
158(3)
7.3 Control of the Moore-Greitzer Engine
161(3)
7.4 Mobile Robot Motion Planning
164(6)
7.4.1 Parallel Parking
165(2)
7.4.2 Motion Planning
167(3)
7.5 Online Obstacle Avoidance
170(11)
7.5.1 Offline Control Synthesis
172(4)
7.5.2 Online Replanning
176(3)
7.5.3 Simulation
179(2)
7.6 Robotic Manipulator
181(3)
7.7 Bipedal Locomotion
184(18)
7.7.1 Hybrid System Model of Bipedal Locomotion
186(4)
7.7.2 Hierarchical Reactive Planning Strategy
190(4)
7.7.3 Robust Switching Between Locomotion Modes
194(4)
7.7.4 Simulation
198(4)
7.8 Summary
202(3)
A Basic Theory of Ordinary Differential Equations
205
A.1 Initial Value Problem and Caratheodory Solutions
205(1)
A.2 Existence and Uniqueness Theorem
206(7)
A.3 Global Existence
213(2)
A.4 Differential Inequalities and a Comparison Theorem
215(4)
B Interval Analysis
219(4)
B.1 Proof of Convergence for Taylor Inclusions (Proposition 4.6)
219(4)
B.1.1 Proof of Proposition 4.6
220(3)
C Basic Set Theory
223(6)
C.1 Set Convergence
223(1)
C.2 Heine-Borel Theorem
224(1)
C.3 Minkowski Sum and Minkowski Difference
224(1)
C.4 Proof of Proposition 6.2
225(1)
C.5 Proof of Proposition 6.3
226(1)
C.6 Proof of Proposition 6.4
227(2)
D Mappings of Locomotion Modes
229(2)
Bibliography 231(20)
Index 251
Jun Liu received the B.S. degree in applied mathematics from Shanghai Jiao-Tong University in 2002, the M.S. degree in mathematics from Peking University in 2005, and the Ph.D. degree in applied mathematics from the University of Waterloo in 2011. Following an NSERC Postdoctoral Fellowship in Control and Dynamical Systems at Caltech, he became a Lecturer in Control and Systems Engineering at the University of Sheffield in 2012. He joined the Faculty of Mathematics of the University of Waterloo in 2015, where he currently is an Associate Professor of Applied Mathematics and directs the Hybrid Systems Laboratory. Dr. Liu's 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 Marie-Curie Career Integration Grant from the European Commission in 2013, a Canada Research Chair from the Government of Canada in 2017 and 2022, an Early Researcher Award from the Ontario Ministry of Research, Innovation and Science in 2018, and an Early Career Award from the Canadian Applied and Industrial Mathematics Society and Pacific Institute for the Mathematical Sciences in 2020. His best paper awards include the Zhang Si-Ying Outstanding Youth Paper Award and the Nonlinear Analysis: Hybrid Systems Paper Prize. Dr. Liu is a senior member of IEEE, a member of SIAM, and a lifetime member of CAIMS. He has served on the editorial boards and program committees of several journals and conferences, including Automatica, Nonlinear Analysis: Hybrid Systems, Systems & Control Letters, the ACM International Conference on Hybrid Systems: Computation and Control (HSCC), the IEEE Conference on Decision and Control (CDC), and the American Control Conference (ACC).

Yinan Li is a senior autonomy developer at OTTO Motorsthe industrial division of Clearpath Robotics in Kitchener, Ontario, Canada. She works on navigation algorithms for industrial mobile robots, multi-robot traffic control and coordination. Before joining OTTO Motors, she was a post-doctoral fellow at Hybrid Systems Laboratory, shortly after she received her Ph.D. degree in applied mathematics from University of Waterloo in 2019. Her Ph.D. and post-doctoral research focused on formal control methods for nonlinear systems, and joint research with Georgia Institute of Technology and Clearpath Robotics were about applications of formal control methods in humanoid and mobile robots. She was awarded the 2020 Huawei prize for best research paper for her research in this area.