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.