A simulation-based approach to the approximation of stochastic hybrid systems

We study the problem of approximating a stochastic, possibly hybrid, system by means of some abstracted model to the purpose of simplifying the analysis of properties such as probabilistic safety and reachability. We suppose that the property to be analyzed depends on the behavior of some output signal of the system and that the model is designed in order to reproduce that signal as close as possible, for the different possible realizations of the stochastic input affecting the system. The idea developed in this paper is to assess the quality of a model as an approximation of a stochastic system by testing how close are their output signals over a finite number of input realizations. Under suitable assumptions, we show that, with high confidence, the quality assessed on a few input realizations is guaranteed to hold also for all the unseen ones except for a set of pre-defined probability epsilon. The proposed approach can be applied to an arbitrary system, the only requirement being to be able to run multiple simulations of its behavior for different input realizations.