Bounded Verification of Reachability of Probabilistic Hybrid Systems

In this paper, we consider the problem of bounded reachability analysis of probabilistic hybrid systems which model discrete, continuous and probabilistic behaviors. The discrete and probabilistic dynamics are modeled using a finite state Markov decision process (MDP), and the continuous dynamics is incorporated by annotating the states of the MDP with differential equations/inclusions. We focus on polyhedral dynamical systems to model continuous dynamics. Our broad approach for computing probabilistic bounds on reachability consists of the computation of the exact minimum/maximum probability of reachability within k discrete steps in a polyhedral probabilistic hybrid system by reducing it to solving an optimization problem with satisfiability modulo theory (SMT) constraints. We have implemented analysis algorithms in a Python toolbox, and use the Z3opt optimization solver at the backend. We report the results of experimentation on a case study involving the analysis of the probability of the depletion of the charge in a battery used in the nano-satellite.