We propose
HyDICE, Hybrid Discrete Continuous Exploration, a multi-layered approach for hybrid-system falsification that combines motion planning
with discrete search and discovers safety violations by computing witness trajectories to unsafe states. The discrete search
uses discrete transitions and a state-space decomposition to guide the motion planner during the search for witness trajectories.
Experiments on a nonlinear hybrid robotic system with over one million modes and experiments with an aircraft conflict-resolution
protocol with high-dimensional continuous state spaces demonstrate the effectiveness of
HyDICE. Comparisons to related work show computational speedups of up to two orders of magnitude.
Keywords Hybrid system - Safety properties - Robot motion planning - Discrete search - Sampling-based planning - Decomposition - Nonlinear dynamics
Work supported in part by NSF CNS 0615328 (EP, LK, MV), NSF 0713623 (EP, LK), a Sloan Fellowship (LK), and NSF CCF 0613889
(MV). Equipment supported by NSF CNS 0454333 and NSF CNS 0421109 in partnership with Rice, AMD, and Cray.
A preliminary version of this work was published in the Proceedings of the 19th International Conference on Computer Aided
Verification (CAV 2007). Lecture Notes in Computer Science, eds. W. Damm and H. Hermanns, vol. 4590, pp. 468–481. This work
contains substantial improvements to the overall computational method introduced in the preliminary work and new experiments
that were not included in the preliminary work.