A two-step scheme for approximate model checking of stochastic hybrid systems

In this paper we describe a two-step scheme for approximate model checking of discrete time stochastic hybrid systems. In the first step, the stochastic hybrid system is approximated by a finite state Markov chain. In the second step, the Markov chain is model checked for the desired property. In particular, we consider the probabilistic invariance property and show that, under certain regularity conditions, the invariance probability computed using the approximatingMarkov chain converges to the invariance probability of the original stochastic hybrid system, as the grid used in the approximation gets finer. A bound on the convergence rate is also provided.