Computational Methods for Verification of Stochastic Hybrid Systems

Stochastic hybrid system (SHS) models can be used to analyze and design complex embedded systems that operate in the presence of uncertainty and variability. Verification of reachability properties for such systems is a critical problem. Developing sound computational methods for verification is challenging because of the interaction between the discrete and the continuous stochastic dynamics. In this paper, we propose a probabilistic method for verification of SHSs based on discrete approximations focusing on reachability and safety problems. We show that reachability and safety can be characterized as a viscosity solution of a system of coupled Hamilton

• Type: Journal
• Year: 2008
• Where: TSMC
• Authors: Xenofon D. Koutsoukos, Derek Riley
• Keywords: Continuous Stochastic Dynamics, Discrete Approximation, Reachability, TSMC 2008