Safety of Stochastic Hybrid Systems Based on Discrete Approximations

Stochastic hybrid system models can be used to analyze and design complex embedded systems that operate in the presence of uncertainty and variability. Verification of safety properties of such systems is a critical problem because of the interaction between the discrete and continuous stochastic dynamics. In this paper, we propose a probabilistic method for verifying safety based on discrete approximations. We show that the safety property can be characterized as a viscosity solution of a system of coupled Hamilton-Jacobi-Bellman equations. We present a computational algorithm for computing the solution based on discrete approximations and we show that this solution converges to the one for the original system as the discretization becomes finer. Finally, we illustrate the approach with a room heater example that has been proposed as a benchmark for hybrid system verification