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.
This project is supported 2013-2016 by the German Research Foundation (DFG) under the project number AB 461/4-1.
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.
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.
Our collection of continuous and hybrid system benchmarks can be found here.
|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.|
|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.|
|Erika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis. Proc. Numerical Software Verification (NSV'17), , 2017.|
|Erika Abraham, Sergiy Bogomolov editors. Proc. of the 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis, SNR@ETAPS 2017. , Volume 247 of EPTCS, 2017.|
|Jannik Hüls, Stefan Schupp, Anne Remke, Erika Abraham. Analyzing Hybrid Petri nets with multiple stochastic firings using HyPro. Proc. of the 11th EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'17), , 2017.|