We describe a methodology for reachability analysis of a certain class of stochastic hybrid systems, whose continuous dynamics is governed by stochastic differential equations and discrete dynamics by state-dependent probabilistic transitions. The main feature of the proposed methodology is that it rests on the weak approximation of the solution to the stochastic differential equation with random mode transitions by a Markov chain. Reachability computations then reduce to propagating the transition probabilities of the approximating Markov chain. An example of applications to system verification is presented.
展开▼
