000			05464cam a2200469Ii 4500
001			95562
003			ES-MaUEC
005			20230102112710.0
006			m o d
007			cr cnu|||unuuu
008			170314t20172017sz ob 001 0 eng d
020			_a331950763X _q(electronic bk.)
020			_a9783319507637 _q(electronic bk.)
020			_z3319507621
020			_z9783319507620
040			_aN$T _cN$T _dIDEBK _dN$T _dGW5XE _dEBLCP _dYDX _dUAB _dNJR _dOCLCF _dIOG _dCOO _dAZU _dUPM _dXPJ _dESU _dJBG _dIAD _dICW _dICN _dOTZ _dVT2 _dOCLCQ _dU3W _dES-MaUEC _bspa
050		4	_aTA352 _b.B458 2017 EB
100	1		_aBelta, Calin, _eautor
245	1	0	_aFormal methods for discrete-time dynamical systems _cCalin Belta, Boyan Yordanov, Ebru Aydin Gol.
264		1	_aCham, Switzerland _bSpringer _c[2017]
264		4	_c2017
300			_a1 recurso en línea
336			_aTexto _btxt _2rdacontent
337			_aelectrónico _bc _2rdamedia
338			_arecurso electrónico _bcr _2rdacarrier
347			_atext file _bPDF _2rda
490	0		_aStudies in systems, decision and control _v89
500			_aSpringerLink _bSpringer Engineering eBooks 2017 English+International
504			_aIncluye referencias bibliográficas e índice
505	0		_aForeword; 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.
505	8		_a10.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.
505	8		_a12.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.
505	8		_a4.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.
505	8		_a7.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.
520	3		_aThis 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.
650		7	_aDinámica _2embne _0(OCoLC)fst00900295 _0 _9138903
700	1		_aGol, Ebru Aydin, _eautor
700	1		_aYordanov, Boyan, _eautor
856	4	0	_uhttps://go.openathens.net/redirector/universidadeuropea.es?url=http://link.springer.com/10.1007/978-3-319-50763-7 _zAcceso a este recurso digital (usuarios Universidad Europea de Madrid)
988			_aEBOOK, asignarmaterias, EBSPRINGER_2017C
998			_b02/2018 _dz _e- _zSI
999			_c95562 _d95562 _x1