Formal Methods for Discrete-Time Dynamical Systems (eBook)

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