I. Introduction
Stochastic hybrid systems are a class of non-linear stochastic continuous time/space hybrid dynamical systems. For these systems different models have been developed by many researchers in the field of hybrid systems. These models can be used to analyse and design complex embedded systems that operate in the presence of variability and uncertainty, and incorporate complex (hybrid/stochastic) dynamics, randomness, multiple modes of operations. Under some natural assumptions on their parameters, their behaviour can be described by stochastic processes having good properties. A very important verification problem for such systems consists mainly in reachability analysis. The aim of reachability analysis is to determine the probability that the system will reach a set of desirable/unsafe states, and the difficulty of this problem comes from the interaction between discrete/continuous dynamics and the active boundaries.