Formal methods for discrete-time dynamical systems. ([2017])

• Record Type: Book
• Further Information: Note: Calin Belta, Boyan Yordanov, Ebru Aydin Gol.
• Authors: Belta, Calin; Yordanov, Boyan; Gol, Ebru Aydin
• Contents: 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. 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. 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.
• Publisher Details: Cham, Switzerland : Springer
• Publication Date: 2017
• Copyright Date: 2017
• Extent: 1 online resource
• Subjects: 620.1/04; Engineering; Dynamics; TECHNOLOGY & ENGINEERING -- Engineering (General); TECHNOLOGY & ENGINEERING -- Reference; Dynamics; Technology & Engineering -- General; Science -- System Theory; Cybernetics & systems theory; Systems theory; Technology & Engineering -- Automation; Automatic control engineering; Electronic books
• Languages: English
• ISBNs: 9783319507637
• Related ISBNs: 331950763X; 9783319507620; 3319507621
• Notes: Note: Includes bibliographical references and index.; Note: Vendor-supplied metadata.
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.