.

0 (hodnocen0 x )

EB

EB

ONLINE

Cham : Springer International Publishing, 2017

1 online zdroj

ISBN 978-3-319-50763-7 (e-kniha)

ISBN 978-3-319-50762-0 (print)

Studies in Systems, Decision and Control, ISSN 2198-4182 ; 89

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

001477431

Part I Transition Systems, Automata, and Temporal Logics // 1 Transition Systems // 1.1 Definitions and Examples // 1.2 Discrete-Time Dynamical Systems as Transition Systems // 1.3 Simulation and Bisimulation // 1.4 Notes // 2 Temporal Logics and Automata // 2.1 Linear Temporal Logic // 2.2 Automata // 2.3 Notes // Part II Analysis and Control of Finite Transition Systems // 3 Model Checking // 3.1 Notes // 4 Largest Finite Satisfying Region // 4.1 Model-Checking-Based Solution // 4.2 Abstraction-Based Solution // 4.3 Iterative Strategies // 4.4 Conservative Quotient Refinement // 4.5 Formula-Equivalence // 4.6 Notes // 5 Finite Temporal Logic Control // 5.1 Control of Transition Systems from LTL Specifications // 5.2 Control of Transition Systems from dLTL Specifications // 5.3 Control of Transition Systems from scLTL Specifications // 5.4 Notes // Part III Analysis and Control of Discrete-Time Dynamical Systems // 6 Discrete-Time Dynamical Systems 111 // 6.1 Piecewise Affine Systems 111 // 6.2 Switched Linear Systems 116 // 6.3 Notes 117 // 7 Largest Satisfying Region 119 // 7.1 PWA Systems with Fixed and Additive Uncertain Parameters 120 // 7.2 PWA Systems with Uncertain Parameters 128 // 7.3 Formula-Guided Refinement 135 // 7.4 Notes 137 // 8 Parameter Synthesis 141 // 8.1 Counterexample-Guided Pruning of Finite Systems 143 // 8.2 Parameter Sets and Transitions 147 // 8.3 Transient Parameters 151 // 8.4 Parameter Synthesis for PWA Systems 152 // 8.5 Parameter Synthesis Using Bisimulations 157 // 8.6 Notes 159 // 9 Temporal Logic Control 163 // 9.1 Control Abstraction 164 // 9.1.1 Definition 164 // 9.1.2 Computation 166 // 9.2 LTL Control of PWA Systems 169 // 9.3 Conservatism and Stuttering Behavior 170 // 9.4 Notes 180 // 10 Finite Bisimulations 185 // 10.1 Bisimulation Quotient 188 // 10.1.1 Level Sets and Slices 188 // 10.1.2 Abstraction Algorithm 190 //

10.1.3 Extensions 193 // 10.1.4 Complexity 195 // 10.2 Synthesis and Verification 199 // 10.2.1 Synthesis 199 // 10.2.2 Verification 200 // 10.3 Notes 203 // 11 Language Guided Controller Synthesis 205 // 11.1 Dual Automaton Construction and Simplification 207 // 11.2 Dual Automaton Refinement 213 // 11.2.1 Transition Controllers 214 // 4Contents // H.2.2 Refinement // 11.2.3 Partitioning. // 11.3 Control Strategy // 11.4 Notes // 12 Optimal Temporal Logic Control // 12.1 Automaton Generation // 12.2 Lyapunov-Type Functions for Dual Automaton // 12.2.1 Potential Function // 12.2.2 Contractive Potential Function // 12.3 MPC Strategies // 12.3.1 MPC with Terminal Constraints // 12.3.2 MPC with Terminal Cost // 12.4 Notes // Appendix A: Background // References // Index