Computer Science Speaking Skills Talk

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/

For More Information, Contact:

deb@cs.cmu.edu

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.

Keywords:

Speaking Skills