Reachability analysis for nonlinear hybrid systems

Luca Geretti - University of Verona

Date and time
Wednesday, May 30, 2018 at 3:30 PM - room Tessari

Contact person
Marco Caliari

Publication date
May 4, 2018

Computer Science  


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

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 ARIADNE, 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.

© 2002 - 2022  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234