Markov modeling of Stochastic Hybrid Systems

Hybrid systems are a useful abstraction for systems that have a combination of discrete and continuous dynamics. For typical examples of hybrid systems, there can be various sources of stochasticity. The source of stochasticity can be in the dynamics of the continuous states, the probabilistic switching between various modes of the system and the probabilistic resetting of the continuous state after switches. Such systems can be mathematically modeled by Discrete Time Stochastic Hybrid Systems (DTSHS). If the uncertainty in the initial condition of the stochastic hybrid system is specified by a probability distribution, it is useful to compute the probability distribution of the state of the system for some time in the future. This would allow one to quantify the probability of the system to be in an undesired or unsafe set. Such computations can be useful for probabilistic verification and validation of systems. In this paper, we discuss state space models for DTSHS and present computational methods to propagate probability distributions for DTSHS.