Hybrid Dynamical Systems: Fundamentals and Methods

Series Editor’s Foreword
Preface
Acknowledgements
Contents
About the Authors
1 Introduction
	1.1 What is a Hybrid Dynamical System?
	1.2 Why Do We Need a New Theory?
	1.3 Research Approaches
	1.4 Book Structure and Contents
	1.5 A Brief Instructor's Guide
	References
2 Modeling of Hybrid Systems
	2.1 Finite Automata
		2.1.1  Finite Automaton Model
		2.1.2 Properties of Finite Automata
		2.1.3 Regular Languages
	2.2 Hybrid Automata
		2.2.1 Hybrid Automata Models
		2.2.2 Hybrid Automata Composition
		2.2.3 Hybrid Execution
		2.2.4 Determinism and Non-blocking Properties
	2.3 Switched and Piecewise Affine Systems
		2.3.1 Switched Systems
		2.3.2 Piecewise Affine Systems
		2.3.3 Existence and Uniqueness of Solutions
	2.4 Summary
	2.5 Notes and Further Reading
	2.6 Exercises
	References
3 Formal Verification
	3.1 Labeled Transition Systems
		3.1.1 Transition Systems
		3.1.2 Labeled Transition System
	3.2 Linear Temporal Logic
		3.2.1 Linear Temporal Logic
		3.2.2 LTL Model Checking
	3.3 Computation Tree Logic
		3.3.1 Computation Tree Logic
		3.3.2 CTL Model Checking
		3.3.3 Comparison Between LTL and CTL
	3.4 Bisimulation
		3.4.1 Simulation Relation
		3.4.2 Bisimulation Quotient
		3.4.3 Computing Bisimulations
	3.5 Timed Automata
		3.5.1 Timed Automata
		3.5.2 Timed Language
		3.5.3 Timed Computation Tree Logic
		3.5.4 Timed Automata Model Checking
		3.5.5 Extensions of Timed Automata
		3.5.6 Zone Automata and Symbolic Reachability Analysis
	3.6 Linear Hybrid Automata
		3.6.1 Linear Hybrid Automata
		3.6.2 Runs of Linear Hybrid Automata
		3.6.3 Symbolic Reachability Analysis of Linear Hybrid Automata
		3.6.4 Symbolic Model Checking
	3.7 Verification of More General Hybrid Systems
		3.7.1 Linear Dynamics
		3.7.2 Barrier Certificate
	3.8 Summary
	3.9 Notes and Further Reading
	3.10 Exercises
	References
4 Stability and Stabilization
	4.1 Lyapunov Stability Theory
		4.1.1 Lyapunov Stability
		4.1.2 Stability of Linear Time-Invariant Systems
		4.1.3 Lyapunov Stability for Time-Varying Systems
		4.1.4 Converse Lyapunov Theorem
	4.2 Stability of Hybrid Automata
	4.3 Arbitrary Switching
		4.3.1 Common Lyapunov Functions
		4.3.2 Common Quadratic Lyapunov Functions
		4.3.3 Commutative Systems
		4.3.4 Triangular Systems
		4.3.5 A Lie Algebraic Condition
		4.3.6 Switched Quadratic Lyapunov Functions
	4.4 Constrained Switching
		4.4.1 Stability with Dwell Time
		4.4.2 Stability with Average Dwell Time
		4.4.3 Discrete-Time Case
	4.5 Multiple Lyapunov Functions
		4.5.1 Multiple Lyapunov Functions Theorem
		4.5.2 Piecewise Quadratic Lyapunov Functions
	4.6 Design of Stabilizing Switching Sequences
		4.6.1 Quadratic Stabilization
		4.6.2 Piecewise Quadratic Stabilization
	4.7 Summary
	4.8 Notes and Further Reading
	4.9 Exercises
	References
5 Optimal Control
	5.1 Optimal Control Problem
	5.2 The Minimum Principle
		5.2.1 Calculus of Variations
		5.2.2 Necessary Conditions for Optimal Control Solutions
		5.2.3 Pontryagin's Minimum Principle
	5.3 Hybrid Optimal Control
		5.3.1 Hybrid Optimal Control Problem
		5.3.2 Basic Hybrid Minimum Principle
		5.3.3 Extensions of the Hybrid Minimum Principle
		5.3.4 Further Extensions of Hybrid Minimum Principles
	5.4 Optimal Control of Switched Systems
		5.4.1 Optimal Control Problem for Switched Systems
		5.4.2 Two-Stage Optimization
		5.4.3 Embedding Optimization
	5.5  Model Predictive Control
		5.5.1 Mixed-Logic Dynamical Systems
		5.5.2 Mixed-Integer Programming
	5.6 Summary
	5.7 Notes and Further Reading
	5.8 Exercises
	References
6 Formal Synthesis
	6.1 Discrete Games
		6.1.1 Game Structure
		6.1.2 Safety Games
		6.1.3 Reachability Games
		6.1.4 Büchi Games
	6.2 Differential Games
		6.2.1 Open-Loop Strategy
		6.2.2 Closed-Loop Strategy for One-Player Game
		6.2.3 State-Feedback Strategy for Two-Player Games
		6.2.4 Two-Player Zero-Sum Games
		6.2.5 Pursuit–Evasion Games
	6.3 Unifying Discrete Games and Differential Games
		6.3.1 Solving Discrete Games by Value Iteration
		6.3.2 Differential Safety Games
	6.4 Timed Games
		6.4.1 Timed Game Automata
		6.4.2 Abstraction of a Timed Game
		6.4.3 Symbolic Approach
		6.4.4 Timed Automata Optimal Control
	6.5 Hybrid Games
		6.5.1 Hybrid Game Automata
		6.5.2 Solve the Reach-While-Avoid Operator as a Pursuit–Evasion Game
	6.6 Control-Oriented Abstraction
		6.6.1 Temporal Logic over Reals
		6.6.2 Linear Control Systems
		6.6.3 Multi-affine Control Systems
		6.6.4 Approximate Bisimulation and Nonlinear Control Systems
	6.7 Optimization-Based Approaches
		6.7.1 Signal Temporal Logic
		6.7.2 Trajectory Synthesis
		6.7.3 Robust Semantics
	6.8 Summary
	6.9 Notes and Further Reading
	6.10 Exercises
	References
Appendix A Continuous and Sampled-Data Systems
A.1  Modeling Signals and Systems
A.2  Continuous- and Discrete-Time Linear Systems
A.3  Modeling Sampled-Data Systems
A.4  Notes and Further Reading
Appendix B Languages and Automata
B.1  Regular Languages and Finite Automata
B.2  Büchi Automata
B.3  Generalized Büchi Automaton
B.4  Converting LTL to Büchi Automata
B.5  Notes and Further Reading
	References
Index