Simulation-based verification for stochastic systems

Formal verification of stochastic systems is usually done by means of exhaustive state-space search and numerical techniques. In this way, one can model check precisely (up to arbitrarily small numerical errors) any finite-state stochastic systems. However, this approach quickly leads to state explosion: the number of states in the model grows so large that the techniques become unusable in practice. In this talk, we illustrate a more efficient approach for model checking Markov Decision Processes, based on simulation and machine learning. Next, we sketch a novel approach for model checking stochastic hybrid (continuous/discrete) systems, based on verified simulation.