Verification Issues for Stochastic Hybrid Systems

Uncertainties about the environment and system components, or intrinsic system properties, motivate the need for introducing stochastic behavior in a system description. Uncertainty may be modeled via a probability distribution, thereby resulting in stochastic systems. Examples include biological signaling pathways, embedded control systems and, more recently, stochastic processors. Due to the state explosion problem, the verification of stochastic systems can be a very difficult task. Statistics-based verification techniques can be effectively used for combating the state explosion problem, although they are not a panacea. In this talk we address several issues and benefits of statistical verification techniques for stochastic hybrid systems. We focus in particular on the verification of transient and long-running properties.