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

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

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

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

Show all |