Formal methods for discrete-time dynamical systems
Belta, Calin,
Formal methods for discrete-time dynamical systems Calin Belta, Boyan Yordanov, Ebru Aydin Gol. - 1 recurso en línea - Studies in systems, decision and control 89 .
SpringerLink
Incluye referencias bibliográficas e índice
Foreword; Preface; Motivation and Objectives; Intended Audience; Book Outline and Usage; Related Books; Acknowledgements; Contents; Notations; 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. 10.1 Bisimulation Quotient10.1.1 Level Sets and Slices; 10.1.2 Abstraction Algorithm; 10.1.3 Extensions; 10.1.4 Complexity; 10.2 Synthesis and Verification; 10.2.1 Synthesis; 10.2.2 Verification; 10.3 Notes; 11 Language Guided Controller Synthesis; 11.1 Dual Automaton Construction and Simplification; 11.2 Dual Automaton Refinement; 11.2.1 Transition Controllers; 11.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 Function12.3 MPC Strategies; 12.3.1 MPC with Terminal Constraints; 12.3.2 MPC with Terminal Cost; 12.4 Notes; Appendix A Background; A.1 Polytopes; A.2 Operations on Polytopes; A.3 Affine Functions on Polytopes; A.4 Semi-linear Sets and Affine Functions; A.5 Lyapunov Theory; A.6 Reach Control Problems on Polytopes; A.6.1 Iterative Pre-computation; A.6.2 Vertex Interpolation; A.6.3 Contractive Sets; A.7 Control Potential Functions; A.7.1 Control Potential Function Based on One Step Controllable Sets. 4.1 Model-Checking-Based Solution4.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; 6.1 Piecewise Affine Systems; 6.2 Switched Linear Systems; 6.3 Notes; 7 Largest Satisfying Region. 7.1 PWA Systems with Fixed and Additive Uncertain Parameters7.2 PWA Systems with Uncertain Parameters; 7.3 Formula-Guided Refinement; 7.4 Notes; 8 Parameter Synthesis; 8.1 Counterexample-Guided Pruning of Finite Systems; 8.2 Parameter Sets and Transitions; 8.3 Transient Parameters; 8.4 Parameter Synthesis for PWA Systems; 8.5 Parameter Synthesis Using Bisimulations; 8.6 Notes; 9 Temporal Logic Control; 9.1 Control Abstraction; 9.1.1 Definition; 9.1.2 Computation; 9.2 LTL Control of PWA Systems; 9.3 Conservatism and Stuttering Behavior; 9.4 Notes; 10 Finite Bisimulations.
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.
331950763X 9783319507637
Dinámica
TA352 / .B458 2017 EB
Formal methods for discrete-time dynamical systems Calin Belta, Boyan Yordanov, Ebru Aydin Gol. - 1 recurso en línea - Studies in systems, decision and control 89 .
SpringerLink
Incluye referencias bibliográficas e índice
Foreword; Preface; Motivation and Objectives; Intended Audience; Book Outline and Usage; Related Books; Acknowledgements; Contents; Notations; 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. 10.1 Bisimulation Quotient10.1.1 Level Sets and Slices; 10.1.2 Abstraction Algorithm; 10.1.3 Extensions; 10.1.4 Complexity; 10.2 Synthesis and Verification; 10.2.1 Synthesis; 10.2.2 Verification; 10.3 Notes; 11 Language Guided Controller Synthesis; 11.1 Dual Automaton Construction and Simplification; 11.2 Dual Automaton Refinement; 11.2.1 Transition Controllers; 11.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 Function12.3 MPC Strategies; 12.3.1 MPC with Terminal Constraints; 12.3.2 MPC with Terminal Cost; 12.4 Notes; Appendix A Background; A.1 Polytopes; A.2 Operations on Polytopes; A.3 Affine Functions on Polytopes; A.4 Semi-linear Sets and Affine Functions; A.5 Lyapunov Theory; A.6 Reach Control Problems on Polytopes; A.6.1 Iterative Pre-computation; A.6.2 Vertex Interpolation; A.6.3 Contractive Sets; A.7 Control Potential Functions; A.7.1 Control Potential Function Based on One Step Controllable Sets. 4.1 Model-Checking-Based Solution4.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; 6.1 Piecewise Affine Systems; 6.2 Switched Linear Systems; 6.3 Notes; 7 Largest Satisfying Region. 7.1 PWA Systems with Fixed and Additive Uncertain Parameters7.2 PWA Systems with Uncertain Parameters; 7.3 Formula-Guided Refinement; 7.4 Notes; 8 Parameter Synthesis; 8.1 Counterexample-Guided Pruning of Finite Systems; 8.2 Parameter Sets and Transitions; 8.3 Transient Parameters; 8.4 Parameter Synthesis for PWA Systems; 8.5 Parameter Synthesis Using Bisimulations; 8.6 Notes; 9 Temporal Logic Control; 9.1 Control Abstraction; 9.1.1 Definition; 9.1.2 Computation; 9.2 LTL Control of PWA Systems; 9.3 Conservatism and Stuttering Behavior; 9.4 Notes; 10 Finite Bisimulations.
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.
331950763X 9783319507637
Dinámica
TA352 / .B458 2017 EB