Rare Event Simulation for Stochastic Hybrid Systems Using Symbolic Importance Functions

The formal modeling and evaluation of realistic cyber-physical systems requires stochastic hybrid models, for which traditional verification methods like model checking are severely limited in applicability and scalability. Simulation-based approaches like statistical model checking are a popular alternative, but break down when faced with the rare events typical for safety-critical systems and infrastructures with high reliability requirements. To overcome this challenge, we propose a novel rare-event simulation approach for stochastic hybrid models that combines importance splitting with a compact symbolic precomputation of the reachable states. We focus on HPnG models, a stochastic hybrid extension of Petri nets. The precomputation extracts all information about the behavior of the HPnG needed to automatically identify an importance function tailored to the specific STL property defining the rare event of interest. We implement our approach in the hpnmg tool and illustrate its feasibility on three case studies, experimentally comparing performance and scalability in combination with the Fixed effort and Restart importance splitting methods.