Combining analytical technique and randomized algorithm in safety verification of stochastic hybrid systems

We consider the problem of probabilistic safety verification for stochastic hybrid systems. In particular, we propose a method that combines two existing approaches, namely, analytical techniques and randomized algorithms. Analytical techniques, such as using stochastic approximate bisimulation, are able to handle non-deterministic initial states. However, their practical applicability is limited to relatively simple stochastic dynamics. On the other hand, randomized algorithms are able to handle more complex dynamics. However, it typically requires running a large number of simulations, and cannot be used for non-deterministic initial states. Our combined approach basically uses an analytical technique when the stochastic dynamics is simple, and switches to a randomized algorithm when the dynamics is nonlinear. The main idea is that by using the analytical technique, we can bound the gaps between the probability density functions corresponding to the family of non-deterministic initial states. This, in turn, enables randomized algorithms that provide upper- and lower-bounds on the safety and unsafety probabilities. We illustrate our approach with an example from air traffic management.