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

[bibtex] | Erika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis. Proc. Numerical Software Verification (NSV'17), , 2017. |

Show all |