Scalable safety verification of stochastic hybrid systems

Abstract

Stochastic hybrid systems consist of software-controlled physical processes, where uncertainties manifest due to either disturbance in the environment in which the physical systems operate or the noise in sensors/actuators through which they interact with the software. The safety analysis of such systems is challenging due to complex dynamics, uncertainties, and infinite state space. This thesis introduces fully automated methods for bounded/unbounded safety analysis of certain subclasses of the stochastic hybrid systems against given safety specifications. Our first contribution is to compute the maximum/minimum bounded probability of reachability of polyhedral probabilistic hybrid systems, where plant dynamics are expressed as a set of linear constraints over the rate of state variables, and uncertainties are involved in discrete transitions represented as discrete probability distributions over the set of locations/modes. Our broad approach is to encode all possible bounded probabilistic behaviors into an appropriate logic along with the given safety specifications. Then, we perform optimization over all possible behaviors for the maximum/minimum probability via state-of-the-art optimization solvers. The second contribution is to present fully automatic unbounded safety analysis of the polyhedral probabilistic hybrid systems (PHS). We present a novel counterexample guided abstraction refinement (CEGAR) algorithm for polyhedral PHS. Developing a CEGAR algorithm for the polyhedral PHS is complex owing to the uncertainties in the discrete transitions, and the infinite state space due to the real-valued variables. We present a practical algorithm by choosing a succinct representation for counterexamples, an efficient validation algorithm and a constructive method for refinement that ensures progress towards the elimination of a spurious abstract counterexample. The third contribution is to extend unbounded safety analysis to the class of linear probabilistic hybrid systems (PHS). Developing an abstraction for the linear PHS is a challenge when the dynamics is linear, because the solutions are exponential and require solving exponential constraints to construct the finite state MDP. Hence, we consider a hierarchical abstraction, where we first abstract a linear PHS to a polyhedral PHS using hybridization and then apply predicate abstraction to construct the finite state MDP. Finally, we consider uncertainties in plant dynamics, and develop an abstraction based method for both bounded/unbounded safety analysis of linear stochastic systems. The bounded safety analysis is similar to the encoding in bounded model checking, where we encode bounded stochastic behaviors instead of continuous behaviors and solve the encoding using a semi-definite program solver. For the unbounded safety analysis, we abstract the linear stochastic system into a finite state system, and analyze its safety using graph search algorithms.