Reachability Analysis for nonlinear Hybrid Systems

Reachability Analysis for nonlinear Hybrid Systems
Relatore:  Luca Geretti - Università di Verona
  mercoledì 24 maggio 2017 alle ore 13.30 Starting date
In many applicative fields there is the need to model and design complex systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either discrete or continuous models only. Such systems consist of a discrete control part that operates in a continuous environment and are named hybrid systems because of their mixed nature.

Unfortunately, most of the verification problems for hybrid systems, like reachability analysis, turn out to be undecidable. Because of this, many approximation techniques and tools to estimate the reachable set have been proposed in the literature. However, most of the tools are unable to handle nonlinear dynamics and constraints. We describe an open-source framework for hybrid system verification, called  RIADNE, developed by a joint team led by the University of Verona, which exploits approximation techniques based on the theory of  computable analysis for implementing formal verification algorithms. ARIADNE can be used to verify complex hybrid systems, supporting an assume-guarantee reasoning approach.

The library has been tested in some interesting critical applications (e.g., for verification of plans in robotic surgery) and it is in full development, posing challenging research  problems that call for active involvement by students and researchers interested in scientific computing and modeling of dynamical systems.

May, wed 24, 13.30-15.30, room M
May, thu 25, 15.30-17.30, room G

Referente
Marco Caliari

Referente esterno
Data pubblicazione
27 marzo 2017

Offerta formativa

Condividi