PhD Course on “Numerical verification of nonlinear hybrid automata”
- Period
- 14-28 september 2020
- Academic staff
-
Luca Geretti
Series to which this belongs
- 33° ciclo
- 34° ciclo
- 35° ciclo
Description
The course offers an overview of the verification problem for nonlinear hybrid systems, in particular when modeled by hybrid automata. Compared to systems with restricted dynamics (e.g., linear systems or systems with clocks), nonlinearity limits the range of approaches available for analysis, in particular with respect to symbolic reasoning. We explore the challenges to design a numerically validated approach to verification, we introduce the state-of-art tools and finally we focus on the Ariadne library, developed in our Department in collaboration with an international team. During the lectures, there will be live demonstrations of Ariadne, and case studies for home experiments will be made available.
Outline:
Introduction to numerical verification; the problem of reachability; computable analysis
Hybrid automata and the different classes of expressivity
Representations for reachable sets
Tools for numerical verification of hybrid automata
Computing the continuous evolution of a nonlinear system
Computing the hybrid evolution of a nonlinear system
Verification of nonlinear hybrid automata
Compositionality and contract-based design
Attachments
- Documents
-