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.
Publications
| 2019 | |
|---|---|
 [bibtex] | Francesco Leofante, Stefan Schupp, Erika Abraham, Armando Tacchella. Engineeering Controllers for Swarm Robotics via Reachability Analysis in Hybrid Systems. 33rd International ECMS European Conference on Modelling and Simulation (ECMS'19), pages 407–413, European Council for Modeling and Simulation, 2019. |
| 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. |
[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. |
| 2017 | |
[bibtex] | 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. |
[bibtex] | Erika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis. Proceedings of the 10th International Workshop on Numerical Software Verification (NSV'17), pages XVI-XVII, , 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] | Stefan Schupp, Johanna Nellen, Erika Abraham. Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis. Proc. of the 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'17), Volume 250 of EPTCS, pages 1–14, Open Publishing Association, 2017. |
[bibtex] | 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. |
[bibtex] | Matthias Althoff, Stanley Bak, Dario Cattaruzza, Xin Chen, Goran Frehse, Rajarshi Ray, Stefan Schupp. ARCH-COMP17 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, Volume 48 of EPiC Series in Computing, pages 143–159, EasyChair, 2017. |
| 2015 | |
[bibtex] | Xin Chen. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Phd Thesis at RWTH Aachen University, 2015. |
[bibtex] | Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Abraham, Goran Frehse, Stefan Kowalewski. A Benchmark Suite for Hybrid Systems Reachability Analysis. Proc. of the 7th NASA Formal Methods Symp. (NFM'15), Volume 9058 of LNCS, pages 408–414, Springer, 2015. |
[bibtex] | Stefan Schupp, Erika Abraham, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski. Current Challenges in the Verification of Hybrid Systems. Proc. of the 5th Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy’15), Volume 9361 of Information Systems and Applications, incl. Internet/Web, and HCI, pages 8–24, Springer, 2015. |
[bibtex] | Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Flow* 1.2: More Effective to Play with Hybrid Systems. Proceedings of the 1st and 2nd Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH'15), Volume 34 of EasyChair Proceedings in Computing, pages 152–159, EasyChair, 2015. |
| 2014 | |
[bibtex] | Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Under-approximate Flowpipes for Non-linear Continuous Systems. Proc. of Formal Methods in Computer-Aided Design (FMCAD'14), pages 59–66, IEEE/ACM, 2014. |
[bibtex] | Johanna Nellen, Erika Abraham, Xin Chen, Pieter Collins. Counterexample Generation for Hybrid Automata. Proc. of the 2nd Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'13), Volume 419 of CCIS, pages 88–106, Springer, 2014. |
| 2013 | |
[bibtex] | Sriram Sankaranarayanan, Xin Chen, Erika Abraham. Lyapunov Function Synthesis using Handelman Representations. The 9th IFAC Symposium on Nonlinear Control Systems (NOLCOS'13) (invited paper), , 2013. |
[bibtex] | Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Fabio Somenzi, Erika Abraham. From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits. Proc. of the 2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'13), pages 662–669, IEEE, 2013. |
[bibtex] | Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Empirical Flowpipe Constructions for Analog Circuits. Workshop on Frontiers in Analog CAD (FAC'13), , 2013. |
[bibtex] | Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Flow*: An Analyzer for Non-Linear Hybrid Systems. Proc. of the 25th Int. Conf. on Computer Aided Verification (CAV'13), Volume 8044 of LNCS, pages 258–263, Springer-Verlag, 2013. |
[bibtex] | Ibtissem Ben Makhlouf, Paul Haensch, Stefan Kowalewski. Comparison of Reachability Methods for Uncertain Linear Time-Invariant Systems. ECC13: European Control Conference , Zurich, Switzerland July 17-19,, pages 1101–1106, EUCA, 2013. |
[bibtex] | Ibtissem Ben Makhlouf, Hilal Diab, Stefan Kowalewski. Reachability Analysis for Managing Platoons at Intersections. 21st Mediterranean Conference on Control & Automation (MED) Platanias-Chania, Crete, Greece, June 25-28,, pages 1141–1147, IEEE, 2013. |
| 2012 | |
[bibtex] | Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. Proc. of the 33rd IEEE Real-Time Systems Symposium (RTSS'12), pages 183–192, IEEE Computer Society, 2012. |
[bibtex] | Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Taylor Model Over-approximations for Flowpipe/Guard Intersections. 5th Int. Workshop on Numerical Software Verification (NSV'12), , 2012. |
[bibtex] | Paul Hänsch, Hilal Diab, Ibtissem Ben Makhlouf, Stefan Kowalewski. Reachability Analysis of Linear Systems with Stepwise Constant Inputs. 1st ETAPS Workshop on "Hybrid Autonomous Systems" (HAS 2011), Elsevier, 2012. |
[bibtex] | Ibtissem Ben Makhlouf, Hilal Diab, Stefan Kowalewski. Safety Verification of a Controlled Cooperative Platoon Under Loss of Communication Using Zonotopes. ADHS 2012, Eindhoven, NL, pages 333–338, Inproceeding of the 4th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 12), 2012. |
| 2011 | |
[bibtex] | Xin Chen, Erika Abraham, Goran Frehse. Efficient Bounded Reachability Computation for Rectangular Automata. 5th Workshop on Reachability Problems (RP'11), Volume 6945 of LNCS, pages 139–152, Springer Berlin Heidelberg, 2011. |
[bibtex] | Xin Chen, Erika Abraham, Goran Frehse. Efficient Bounded Reachability Computation for Rectangular Automata. Technical report at RWTH Aachen University, Germany number AIB 2011-15, 2011. |
[bibtex] | Xin Chen, Erika Abraham. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems. 13th Int. Conf. on Computer Aided Systems Theory (EUROCAST'11), Volume 6927 of LNCS, pages 535–542, Springer Berlin Heidelberg, 2011. |
[bibtex] | Ibtissem Ben Makhlouf, Jan Philipp Maschuw, Paul Hänsch, Hilal Diab, Stefan Kowalewski, Dirk Abel. Safety Verification of a Cooperative Vehicle Platoon with Uncertain Inputs Using Zonotopes. 18th IFAC World Congress, 2011, Milano, Italy, pages 9769–9774, IFAC, 2011. |
| 2009 | |
[bibtex] | Ibtissem Ben Makhlouf, Stefan Kowalewski, Martin Chavez Grunewald, Dirk Abel. Safety Assessment of Networked Vehicle Platoon Controllers– Practical Experiences With Available Tools. 3rd IFAC Conference on Analysis and Design of HybridSystems, Zaragoza, Spain, , 2009. |
| 2006 | |
[bibtex] | Ibtissem Ben Makhlouf, Stefan Kowalewski. An Evaluation of Two Recent Reachability Analysis Tools for Hybrid Systems. 2nd IFAC Conference on Analysis and Design of Hybrid Systems, pages 377–382, IFAC-PapersOnline, 2006. |
| 2002 | |
[bibtex] | Stefan Kowalewski. Introduction to the Analysis and Verification of Hybrid Systems. In Sebastian Engell, Goran Frehse, Eckehard Schnieder editors, Modelling, Analysis, and Design of Hybrid Systems, pages 153–171, Volume 279 of Lecture Notes in Control and Information Sciences, 2002. |
| 1999 | |
[bibtex] | Jörg Preussig, Olaf Stursberg, Stefan Kowalewski. Reachability Analysis of a Class of Switched Continuous Systems by Integrating Rectangular Approximation and Rectangular Analysis. In HSCC 99: Hybrid Systems—Computation and Control, LNCS 1569, pages 209–222, Springer, 1999. |