Formal Methods for Discrete-Time Dynamical Systems

Description

This book bridges fundamental gaps between control theory and formal methods. Although it focuses on discrete-time linear and piecewise affine systems, it also provides general frameworks for abstraction, analysis, and control of more general models. The book is self-contained, and while some mathematical knowledge is necessary, readers are not expected to have a background in formal methods or control theory. It rigorously defines concepts from formal methods, such as transition systems, temporal logics, model checking and synthesis. It then links these to the infinite state dynamical systems through abstractions that are intuitive and only require basic convex-analysis and control-theory terminology, which is provided in the appendix. Several examples and illustrations help readers understand and visualize the concepts introduced throughout the book. Front Matter....Pages i-xviii Front Matter....Pages 1-1 Transition Systems....Pages 3-25 Temporal Logics and Automata....Pages 27-38 Front Matter....Pages 39-39 Model Checking....Pages 41-46 Largest Finite Satisfying Region....Pages 47-79 Finite Temporal Logic Control....Pages 81-108 Front Matter....Pages 109-109 Discrete-Time Dynamical Systems....Pages 111-118 Largest Satisfying Region....Pages 119-139 Parameter Synthesis....Pages 141-161 Temporal Logic Control....Pages 163-183 Finite Bisimulations....Pages 185-204 Language Guided Controller Synthesis....Pages 205-230 Optimal Temporal Logic Control....Pages 231-256 Back Matter....Pages 257-284