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 behaviour. Our toolbox offers different datatypes for the representation of state sets for hybrid systems, and efficient operations on them, such that users may easily implement their reachability analysis algorithms based on it.

Funding

This project is supported 2013-2016 by the German Research Foundation (DFG) under the project number AB 461/4-1.

Team

  RWTH Aachen University, Germany
    
Erika Ábrahám
     Xin Chen
     Stefan Kowalewski
     Ibtissem Ben Makhlouf
     Stefan Schupp

  University of Colorado, Boulder, USA

Reachable set representations

Since the reachability problem on general hybrid systems is undecidable, we consider to use over-approximation representations for the reachable set in safety checking tasks. The two popular ways to do that are

  • flowpipe construction: we split the time horizon into small intervals and over-approximate the reachable set in each of them;
  • invariant construction: we try to find one over-approximation for the reachable set in a bounded or unbounded time horizon.

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.In the project, we will propose and implement several heuristics to (exactly or approximately) transform one representation to another such that users may apply combinations of them in their analysis work.

Tools

HyPro is a C++ library providing implementations for the most prominent state set representations used in flowpipe construction based reachability analysis algorithms. The source is available on github, the manual can be found here and the API documentation here.

Flow* is a tool of 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

2017

[bibtex]
Stefan Schupp, Erika Abraham, Ibtissem Ben Makhlouf, Stefan Kowalewski. HyPro: A C++ Library for State Set Representations for Hybrid Systems Reachability Analysis. Proc. of the 9th NASA Formal Methods Symposium (NFM'17), Volume 10227 of LNCS, pages 288–294, Springer International Publishing, 2017.
Download
[bibtex]
Erika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis. Proc. Numerical Software Verification (NSV'17), , 2017.
Show all