A Toolbox for the Reachability Analysis of Hybrid Systems using Geometric Approximations (HyPro)

hypro_Logo

In this project we develop a toolbox to support the implementation of algorithms for the reachability analysis of hybrid systems with mixed discrete-continuous behavior. Our toolbox offers C++ implementations for different datatypes to represent state sets for hybrid systems, and efficient operations on them, such that users may easily implement their reachability analysis algorithms based on it. On top of these datatypes, we also offer iterative reachability analysis algorithms that are based on abstraction and iterative (counterexample-guided) abstraction refinement  for increased scalability.

Funding

The project is supported in two phases 2013-2016 and 2017-2019 by the German Research Foundation (DFG) under the project numbers AB 461/4-1 and AB 461/4-2.

Team

Current Development team

RWTH Aachen University, Germany
     Erika Ábrahám
     Stefan Schupp

Former team members

RWTH Aachen University, Germany
     Xin Chen
     Stefan Kowalewski
     Ibtissem Ben Makhlouf

University of Colorado, Boulder, USA

Reachable set representations

We offer a C++ programming library including different datatypes to represent state sets of hybrid systems. These representations can be used in implementations of reachability analysis algorithms, most representatively for those based on flowpipe construction. Flowpipe-construction-based methods assume a time horizon, within which we want to predict which states a hybrid system can evolve into. We split this time horizon into smaller segments and the system states reachable within each of the those time segments is over-approximated separately.

In order to generate over-approximations which are easy to manipulate, several geometric objects are proposed as the representations, such as convex polyhedra, rectangles, ellipsoids and zonotopes. There are also symbolic representations such as support functions.

Tools

HyPro is our C++ library that offers several such representations and (exact or approximative) conversions between them. The source is available on github, the manual can be found here and the API documentation here.

A poster about recent development, which will be presented at TACAS’18 can be found here.

HyDra uses the datatypes offered by HyPro to implement different approaches for the reachability analysis of hybrid systems. Besides a counterexample-guided abstraction refinement (CEGAR) approach, HyDra exploits parallelization and computation in subspace projections to speed-up the computations.

Flow* is a tool for the reachability analysis of non-linear hybrid systems. More details of Flow* can be found here. There is also a case study website of Flow*.

Benchmarks

Our collection of continuous and hybrid system benchmarks can be found here.

Publications