Finite state approximation for verification of partially observable stochastic hybrid systems
Kendra Lesser, Meeko Oishi · 2015
We consider the problem of verification of safety specifications for stochastic hybrid systems with a controller that has access to partial observations of the state. We address this problem through a finite state approximation of the stochastic hybrid system, which enables the use of existing solution techniques for partially observable Markov decision processes. First, we review a dynamic programming formulation of the safety (viability) problem over an equivalent information state. We then solve a dynamic program over the finite state approximation to generate a lower bound to the viability probability, using a point-based method that generates samples of the information state. Our approach produces approximate probabilistic viable sets and synthesizes a controller to satisfy safety specifications. We provide error bounds and convergence results, assuming additive Gaussian noise in the continuous state dynamics and observations. Finally, we demonstrate performance of the approximation on a simple temperature regulation problem.