Klientų aptarnavimas: +370 652 87781

Pagalba | Naujas vartotojas | Prisijungti

El. knyga: Formal Methods for Control of Nonlinear Systems

Jun Liu (University of Waterloo, Canada), Yinan Li

Formatas: 272 pages
Išleidimo metai: 15-Dec-2022
Leidėjas: Chapman & Hall/CRC
Kalba: eng
ISBN-13: 9781000831931

Kitos knygos pagal šią temą:

Formatas - PDF+DRM
Kaina: 64,99 €*
* ši kaina yra galutinė, t.y. papildomos nuolaidos nebus taikomos
Įdėti į krepšelį
Įtraukti į pageidavimų sąrašą
Ši e-knyga skirta tik asmeniniam naudojimui. El. knygos nėra grąžinamos.
Bibliotekoms

Formatas: 272 pages
Išleidimo metai: 15-Dec-2022
Leidėjas: Chapman & Hall/CRC
Kalba: eng
ISBN-13: 9781000831931

Kitos knygos pagal šią temą:

DRM apribojimai

Kopijuoti:

neleidžiama
Spausdinti:

neleidžiama
El. knygos naudojimas:

Skaitmeninių teisių valdymas (DRM)
Leidykla pateikė šią knygą šifruota forma, o tai reiškia, kad norint ją atrakinti ir perskaityti reikia įdiegti nemokamą programinę įrangą. Norint skaityti šią el. knygą, turite susikurti Adobe ID . Daugiau informacijos čia. El. knygą galima atsisiųsti į 6 įrenginius (vienas vartotojas su tuo pačiu Adobe ID).

Reikalinga programinė įranga
Norint skaityti šią el. knygą mobiliajame įrenginyje (telefone ar planšetiniame kompiuteryje), turite įdiegti šią nemokamą programėlę: PocketBook Reader (iOS / Android)

Norint skaityti šią el. knygą asmeniniame arba „Mac“ kompiuteryje, Jums reikalinga Adobe Digital Editions “ (tai nemokama programa, specialiai sukurta el. knygoms. Tai nėra tas pats, kas „Adobe Reader“, kurią tikriausiai jau turite savo kompiuteryje.)

Negalite skaityti šios el. knygos naudodami „Amazon Kindle“.

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

About the Authors

List of Symbols

xvii

1 Continuous-Time Dynamical Systems

(20)

1.1 Continuous-Time Control System

(1)

1.2 Existence of Local and Global Solutions

(3)

1.3 Stability and Boundedness

(7)

1.4 Safety and Reachability

(5)

1.5 Control Lyapunov Functions

(1)

1.6 Summary

(3)

2 Discrete-Time Dynamical Systems

(6)

2.1 Discrete-Time Control Systems

(1)

2.2 Stability and Boundedness

(3)

2.3 Safety and Reachability

(1)

2.4 Summary

(2)

3 Formal Specifications and Discrete Synthesis

(26)

3.1 Transition Systems

(2)

3.2 Linear-Time Properties

(1)

3.3 Linear Temporal Logic

(3)

3.4 w-Regular Properties

(4)

3.4.1 Translating LTL to Biichi Automata

(3)

3.5 Formulation of Control Problems

(4)

3.5.1 Control of Nondeterministic Transition Systems

(2)

3.5.2 Control of Discrete-Time Dynamical Systems

(1)

3.5.3 Control of Continuous-Time Dynamical Systems

(1)

3.6 Discrete Synthesis

(11)

3.6.1 Safety

(2)

3.6.2 Reachability

(2)

3.6.3 w-Regular Properties

(7)

3.7 Summary

(2)

4 Interval Computation

(38)

4.1 Interval Analysis

(11)

4.1.1 Inclusion Functions

(5)

4.1.2 Mean-Value and Taylor Inclusion Functions

(1)

4.1.3 Inclusion Functions based on Mixed Monotonicity

(4)

4.2 Interval Over-Approximations of One-Step Forward Reachable Sets of Discrete-Time Systems

(2)

4.3 Interval Over-Approximations of One-Step Forward Reachable Sets of Continuous-Time Systems

(12)

4.3.1 A Priori Enclosure

(1)

4.3.2 Over-Approximations by Lipschitz Growth Bound

(3)

4.3.3 Over-Approximations by Mixed Monotonicity

(5)

4.3.4 Over-Approximations by Validated Integration

(1)

4.3.5 Examples

(3)

4.4 Interval Under-approximations of Controlled Predecessors of Discrete-Time Systems

(6)

4.5 Interval Under-approximations of Controlled Predecessors of Continuous-Time System

(4)

4.6 Summary

(3)

5 Controller Synthesis via Finite Abstractions

(14)

5.1 Control Abstractions

(1)

5.2 Soundness

(2)

5.3 Completeness via Robustness

(4)

5.4 Extension to Continuous-Time Dynamical Systems

(3)

5.4.1 Soundness and Robust Completeness

(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.

Daugiau apie elektronines knygas