Monday, May 18, 2015 - 10:00am to 11:00am
Location:8102 Gates & Hillman Centers
Speaker:SOONHO KONG, Ph.D. Student http://www.cs.cmu.edu/~soonhok/
We present the framework of delta-complete analysis for bounded reachability problems of hybrid systems. It encodes reachability problems of hybrid systems to first-order formulas over real numbers, which are solved by delta-decision procedures. The key idea is to check an over-approximated reachability problem which can demonstrate robustness of a hybrid system. The analysis strengthens the verification because robustness implies safety. In contrast to the undecidability result of the general reachability problem for non-linear hybrid systems, delta-reachability problem is decidable and has a reasonable complexity bound (PSPACE-complete). Our implementation of the techniques, an open-source tool dReach, shows that it can handle several highly nonlinear hybrid system models that arise in biomedical and robotics applications. This is a joint work with Sicun Gao (MIT) and Prof. Edmund Clarke (CMU). Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.