Approximate Model Checking of Stochastic Hybrid Systems

A method for approximate model checking of stochastic hybrid systems with provable approximation guarantees is proposed. We focus on the probabilistic invariance problem for discrete time stochastic hybrid systems and propose a two-step scheme. The stochastic hybrid system is first approximated by a finite state Markov chain. The approximating chain is then model checked for probabilistic invariance. Under certain regularity conditions on the transition and reset kernels governing the dynamics of the stochastic hybrid system, the invariance probability computed using the approximating Markov chain is shown to converge 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. The performance of the two-step approximate model checking procedure is assessed on a case study of a multi-room heating system.