1Approximate Verification of Partially Observable Discrete Time Stochastic Hybrid Systems

Assuring safety in discrete time stochastic hybrid systems is particularly difficult when only partial observations are available. We first review a formulation of the probabilistic viability (i.e. safety) problem under noisy hybrid observations as a dynamic program. Two methods for approximately solving the dynamic program are presented. The first method approximates the hybrid system as an equivalent finite state Markov decision process, so that the information state is a probability mass function. The second approach approximates an indicator function over the safe region using radial basis functions, to represent the information state as a Gaussian mixture. In both cases, we discretize the hybrid observation process and generate a sampled set of information states, then use point-based value iteration to under-approximate the viability probability. We obtain error bounds and convergence results in both cases, assuming additive Gaussian noise in the continuous state dynamics and observations. We compare the performance of the finite state and Gaussian mixture approaches on a simple numerical example. I