Scalable safety verification of stochastic hybrid systems

dc.contributor.authorLal, Ratan
dc.description.abstractStochastic 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.en_US
dc.description.advisorPavithra Prabhakaren_US
dc.description.degreeDoctor of Philosophyen_US
dc.description.departmentDepartment of Computer Scienceen_US
dc.description.sponsorshipNational Science Foundation CAREER Award No. 1552668 National Science Foundation CAREER Award No. 2008957 Young Investigator Program - Office of Naval Research Award No. N000141712577 The United States Department of Agriculture Award No. 2017-67007-26153en_US
dc.subjectProbabilistic hybrid systemsen_US
dc.subjectStochastic systemsen_US
dc.subjectHierarchical abstractionen_US
dc.subjectCounterexample guided abstraction refinementen_US
dc.subjectReachability analysisen_US
dc.subjectSafety analysisen_US
dc.titleScalable safety verification of stochastic hybrid systemsen_US


Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
6.65 MB
Adobe Portable Document Format
Main article
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
1.62 KB
Item-specific license agreed upon to submission