RealySt: Reachability Analysis for Stochastic Hybrid Systems

Funding

RealySt, Reachability Analysis for Stochastic Hybrid Systems, is a collaborative project involving Prof. Dr. Dr. h.c. Erika Ábrahám from RWTH Aachen University and Prof. Dr. Anne Remke from WWU Münster. It is funded by German Research Foundation (DFG), under project number 471367371.

About the project

Our society and economy depend on the effective functioning of complex and highly dynamic safety-critical systems. Users must have a strong trust in how these systems operate. However, environmental uncertainties, security challenges, and potential errors in physical devices present significant risks to their reliable performance.

Various modeling languages have been created that allow for a flexible integration of discrete and continuous components, along with stochastic behavior. There is growing research interest and activity focused on analysis techniques for these stochastic hybrid models. In this project, we aim to address the stochastic reachability problem, which involves calculating the probability bounds of reaching certain (often unsafe) states from a specified target set.

We focus on Hybrid Automata as a modelling language and develope the theoretical background and the actual algorithms for the above mentioned stochastic reachability problems. We will also provide an implementation for the theoretical results in a new software tool called Realyst.

Team

RWTH Aachen University, Germany
Erika Ábrahám

József Kovács

WWU University of Münster

Anne Remke

Joanna Delicaris

Jonas Stübbe

Tools

Within the scope of the project a new tool was developed, namely RealySt and further improvements were made in the tool HyPro.

Publications

  • [DSAR23b] Joanna Delicaris, Stefan Schupp, Erika Ábrahám, Anne Remke: Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks. TASE 2023: 164-182, https://doi.org/10.1007/978-3-031-35257-7_10
  • [DSSR23] Joanna Delicaris, Jonas Stübbe, Stefan Schupp, Anne Remke: RealySt: A C++ Tool for Optimizing Reachability Probabilities in Stochastic Hybrid Systems. VALUETOOLS 2023: 170-182, https://doi.org/10.1007/978-3-031-48885-6_11
  • [DSAR23a] Joanna Delicaris, Stefan Schupp, Erika Ábrahám, Anne Remke: Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks. CoRR abs/2304.14996 (2023), https://doi.org/10.48550/arXiv.2304.14996