Reachability Analysis for Stochastic Hybrid Systems

• Applicants: Professorin Dr. Anne Remke; Professorin Dr. Erika Ábrahám
• Subject Area: Theoretical Computer Science
• Term: since 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 471367371

Our society and economy rely on the well-operation of highly dynamic and complex safety-critical systems. Users need to be able to place a high level of trust in the operation of such systems. However, uncertainty in the environment, security issues, as well as errors in physical devices pose a serious threat to their reliable operation.To increase reliability, formal methods aim at providing modeling approaches and corresponding analysis techniques to examine how such systems behave. Stochastic hybrid models are well-suited to naturally model a wide range of relevant real-world systems, where discrete and continuous behavior as well as random aspects need to be considered in combination. However, the expressivity of such models turns their analysis to a highly challenging task, for which currently only a few methods and tools are available. Such methods make use of abstraction and approximation and the accuracy of the computed results decreases significantly with the size of the model at hand.Our main objective in this project is to provide better algorithmic approaches and tool support for the reachability analysis of stochastic hybrid models, building on the idea to separately analyse the deterministic and the stochastic behavior of such models. This idea has previously been investigate in the context of stochastic hybrid Petri nets. Petri nets are well-suited to model concurrent behaviour and naturally exhibit a large degree of compositionality.The project combines the experience of the project partners on reachability analysis, probabilistic systems and stochastic extensions of hybrid Petri nets aiming at synergy effects between these areas: our aim is to first develop a compositional reachability analysis for the non-stochastic part of the model and to reintegrate the aspects of the stochastic model evolution in a second step via a multi-dimensional integration. We expect this approach to yield an increased efficiency and extended applicability for a larger class of supported models.To do so, we will develop analysis techniques for automata-based stochastic hybrid models and extend their applicability to Petri-net-based models by offering a transformation. In addition to stochastic hybrid systems, modules of our project will partly have double impact and increase also the power of reachability analysis for non-stochastic hybrid systems.In addition to the theoretical developments, we aim at the implementation and rigorous evaluation of these methods. In the first place, the resulting implementation should provide an executable tool for end-users, but it should also serve as an extensible software framework for the fast prototypical implementation of further verification methods. Throughout the project the developed methods will be tested on characteristic case studies and benchmarks from the field of safety-critical systems.

• DFG Programme: Research Grants
• International Connection: Austria
• Cooperation Partner: Dr. Stefan Schupp