Position: Ph.D. Student

Current Institution: Carnegie Mellon University

Abstract:
Probabilistic Bounded Delta-Reachability Analysis for Stochastic Hybrid Systems

We consider probabilistic bounded reachability problems for two classes of models of stochastic hybrid systems. The first one is (nonlinear) hybrid automata with parametric uncertainty. The second one is probabilistic hybrid automata with additional randomness for both transition probabilities and variable resets. Standard approaches to reachability problems for linear hybrid systems require numerical solutions for large optimization problems, and become infeasible for systems involving both nonlinear dynamics over the reals and stochasticity. Our method encodes stochastic information by using a set of introduced random variables, and combines delta-complete decision procedures and statistical tests to solve delta-reachability problems in a sound manner, i.e., it always decides correctly if, for a given assignment to all random variables, the system actually reaches the unsafe region. Compared to standard simulation-based methods, it supports non-deterministic branching, increases the coverage of simulation, and avoids the zero-crossing problem. We demonstrate its applicability by discussing three representative biological models and additional benchmarks for nonlinear hybrid systems with multiple probabilistic system parameters.

Bio:
I am a final year Ph.D. student under the supervision of Prof. Edmund M. Clarke (Turing Award 2007) at Computer Science Department, Carnegie Mellon University. Before this, I received a B.A. degree in computer science from Wuhan University, China in 2006, and a M.A. degree in computer science from Institute of Software, Chinese Academy of Sciences, China. I was an intern at Microsoft Research Cambridge with Dr. Jasmin Fisher in Fall 2011. I was awarded a Richard King Mellon Foundation Presidential Fellowship in the Life Sciences by Carnegie Mellon University from year 2015 to 2016. My research focuses on formal specification and verification of software and hardware, especially reachability analysis of stochastic hybrid systems. I am also interested in developing formal models, modeling languages, and algorithms that address problems of practical biological and medical concerns.