Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem

We present a dynamic programming based solution to a probabilistic reach-avoid problem for a controlled discrete time stochastic hybrid system. We address two distinct interpretations of the reach-avoid problem via stochastic optimal control. In the first case, a sum-multiplicative cost function is introduced along with a corresponding dynamic recursion which quantifies the probability of hitting a target set at some point during a finite time horizon, while avoiding an unsafe set during each time step preceding the target hitting time. In the second case, we introduce a multiplicative cost function and a dynamic recursion which quantifies the probability of hitting a target set at the terminal time, while avoiding an unsafe set during the preceding time steps. In each case, optimal reach while avoid control policies are derived as the solution to an optimal control problem via dynamic programming. Computational examples motivated by two practical problems in the management of fisheries and finance are provided.