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 ran- domness 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 the 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.

8th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 2017

Back