Hierarchical Abstractions for Reachability Analysis of Probabilistic Hybrid Systems
Ratan Lal, Pavithra Prabhakar · 2018
We consider the problem of reachability analysis of probabilistic hybrid systems (PHS) which model discrete, continuous and probabilistic behaviors. The discrete and probabilistic dynamics are captured using finite state Markov decision processes (MDP), and the continuous dynamics are modeled by annotating the states of the MDP with differential equations/inclusions. We focus on linear dynamics and propose a two tier abstraction for computing bounds on the probability of reachability, wherein the first step performs dynamics simplification by applying hybridization such that the resulting dynamics is a polyhedral inclusion and the second step constructs a finite state Markov decision process that abstracts the polyhedral inclusion dynamics. This two-tier abstraction is computationally simpler than applying predicate abstraction directly on the linear PHS. We have implemented the abstraction and analysis algorithms in a Python toolbox. Our experimental results demonstrate the feasibility of the approach.