Belta / Yordanov / Aydin Gol Formal Methods for Discrete-Time Dynamical Systems

1. Auflage 2017
ISBN: 978-3-319-50763-7
Verlag: Springer Nature Switzerland
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band 89, 291 Seiten

Reihe: Studies in Systems, Decision and Control

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.

Autoren/Hrsg.

Belta, Calin

Yordanov, Boyan

Aydin Gol, Ebru

Inhaltsverzeichnis

1;Foreword;7
2;Preface;9
2.1;Motivation and Objectives;9
2.2;Intended Audience;10
2.3;Book Outline and Usage;10
2.4;Related Books;11
2.5;Acknowledgements;12
3;Contents;13
4;Notations;16
5;Part I Transition Systems, Automata, and Temporal Logics;18
6;1 Transition Systems;19
6.1;1.1 Definitions and Examples;19
6.2;1.2 Discrete-Time Dynamical Systems as Transition Systems;29
6.3;1.3 Simulation and Bisimulation;32
6.4;1.4 Notes;40
7;2 Temporal Logics and Automata;42
7.1;2.1 Linear Temporal Logic;42
7.2;2.2 Automata;46
7.3;2.3 Notes;51
8;Part II Analysis and Control of Finite Transition Systems;54
9;3 Model Checking;55
9.1;3.1 Notes;60
10;4 Largest Finite Satisfying Region;61
10.1;4.1 Model-Checking-Based Solution;64
10.2;4.2 Abstraction-Based Solution;66
10.3;4.3 Iterative Strategies;70
10.4;4.4 Conservative Quotient Refinement;72
10.5;4.5 Formula-Equivalence;81
10.6;4.6 Notes;92
11;5 Finite Temporal Logic Control;94
11.1;5.1 Control of Transition Systems from LTL Specifications;95
11.2;5.2 Control of Transition Systems from dLTL Specifications;108
11.3;5.3 Control of Transition Systems from scLTL Specifications;116
11.4;5.4 Notes;119
12;Part III Analysis and Control of Discrete-Time Dynamical Systems;122
13;6 Discrete-Time Dynamical Systems;123
13.1;6.1 Piecewise Affine Systems;123
13.2;6.2 Switched Linear Systems;128
13.3;6.3 Notes;129
14;7 Largest Satisfying Region;131
14.1;7.1 PWA Systems with Fixed and Additive Uncertain Parameters;132
14.2;7.2 PWA Systems with Uncertain Parameters;140
14.3;7.3 Formula-Guided Refinement;147
14.4;7.4 Notes;149
15;8 Parameter Synthesis;152
15.1;8.1 Counterexample-Guided Pruning of Finite Systems;154
15.2;8.2 Parameter Sets and Transitions;158
15.3;8.3 Transient Parameters;162
15.4;8.4 Parameter Synthesis for PWA Systems;163
15.5;8.5 Parameter Synthesis Using Bisimulations;168
15.6;8.6 Notes;170
16;9 Temporal Logic Control;173
16.1;9.1 Control Abstraction;174
16.1.1;9.1.1 Definition;174
16.1.2;9.1.2 Computation;176
16.2;9.2 LTL Control of PWA Systems;179
16.3;9.3 Conservatism and Stuttering Behavior;180
16.4;9.4 Notes;190
17;10 Finite Bisimulations;194
17.1;10.1 Bisimulation Quotient;197
17.1.1;10.1.1 Level Sets and Slices;197
17.1.2;10.1.2 Abstraction Algorithm;199
17.1.3;10.1.3 Extensions;202
17.1.4;10.1.4 Complexity;204
17.2;10.2 Synthesis and Verification;208
17.2.1;10.2.1 Synthesis;208
17.2.2;10.2.2 Verification;209
17.3;10.3 Notes;212
18;11 Language Guided Controller Synthesis;214
18.1;11.1 Dual Automaton Construction and Simplification;216
18.2;11.2 Dual Automaton Refinement;222
18.2.1;11.2.1 Transition Controllers;223
18.2.2;11.2.2 Refinement;224
18.2.3;11.2.3 Partitioning;225
18.3;11.3 Control Strategy;230
18.4;11.4 Notes;238
19;12 Optimal Temporal Logic Control;240
19.1;12.1 Automaton Generation;241
19.2;12.2 Lyapunov-Type Functions for Dual Automaton;242
19.2.1;12.2.1 Potential Function;242
19.2.2;12.2.2 Contractive Potential Function;245
19.3;12.3 MPC Strategies;247
19.3.1;12.3.1 MPC with Terminal Constraints;248
19.3.2;12.3.2 MPC with Terminal Cost;254
19.4;12.4 Notes;263
20;Appendix A Background;266
20.1;A.1 Polytopes;266
20.2;A.2 Operations on Polytopes;268
20.3;A.3 Affine Functions on Polytopes;268
20.4;A.4 Semi-linear Sets and Affine Functions;269
20.5;A.5 Lyapunov Theory;271
20.6;A.6 Reach Control Problems on Polytopes;272
20.7;A.6.1 Iterative Pre-computation;273
20.8;A.6.2 Vertex Interpolation;274
20.9;A.6.3 Contractive Sets;275
20.10;A.7 Control Potential Functions;278
20.11;A.7.1 Control Potential Function Based on One Step Controllable Sets;278
20.12;A.7.2 Control Potential Function Based on Feedback Controllers;278
20.13;A.7.2.1 Vertex Interpolation;279
20.14;A.7.2.2 Polyhedral LFs;279
20.15;A.7.2.3 Contractive Sets;279
21;References;281
22;Index;290