δ-complete analysis for bounded reachability of hybrid systems

We present the framework of δ-complete analysis for bounded reachability problems of general hybrid systems. We perform bounded reachability checking through solving δ-decision problems over the reals. The techniques take into account of robustness properties of the systems under numerical perturbations. We prove that the verification problems become much more mathemati-cally tractable in this new framework. Our implementation of the techniques, an open-source tool dReach, scales well on several highly nonlinear hybrid system models that arise in biomedical and robotics applications