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

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

  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.

A poster about recent development, which will be presented at TACAS’18 can be found 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

2018
Link
[bibtex]
Stefan Schupp, Justin Winkens, Erika Abraham. Context-Dependent Reachability Analysis for Hybrid Systems. 2018 IEEE International Conference on Information Reuse and Integration (IRI 2018), pages 518-525, IEEE, 2018.
DOI
[bibtex]
Stefan Schupp, Erika Abraham. Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems. Proceedings of the 16th International Conference on Software Engineering and Formal Methods (SEFM 2018), Volume 10886 of LNCS, pages 89–104, Springer, 2018.
Download
[bibtex]
Stefan Schupp, Erika Abraham. Efficient dynamic error reduction for hybrid systems reachability analysis. Proc. of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), Volume of LNCS, Springer, 2018.

[bibtex]
Matthias Althoff, Stanley Bak, Xin Chen, Chuchu Fan, Marcelo Forets, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Rajarshi Ray, Christian Schilling, Stefan Schupp. ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, Volume 54 of EPiC Series in Computing, pages 23–52, EasyChair, 2018.
Show all