Abstraction Based Reachability Analysis for Finite Branching Stochastic Hybrid Systems

In this paper, we address the problem of computing the probability of reaching a desired set in a subclass of stochastic hybrid systems, wherein the stochasticity arises from the randomness of the initial distribution of continuous states, and the probabilistic transitions in the underlying finite state Markov chain. In particular, the continuous dynamics is deterministic for each mode and hence, there are finitely many probabilistic successors for a given state. We exploit this property and extend a partition based abstraction technique developed for finite state systems to the stochastic hybrid system setting. We prove the correctness of our algorithm by defining appropriate simulation relations that relate the stochastic hybrid system to a finite state "generalized" probabilistic transition system that we obtain as a result of abstraction. We show that the simulation relation defined provides upper and lower bounds on the probability of reachability. In particular, tighter bounds can be obtained by refining the partition. We apply our algorithm to automatically analyze a smart home application.