E. Plaku, L. E. Kavraki, and M. Y. Vardi, “Hybrid systems: from verification to falsification by combining motion planning and discrete search,” Formal Methods in System Design, vol. 34, pp. 157–182, 2009.
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 tra jectories to unsafe states. The discrete search uses discrete transitions and a state-space decomposition to guide the motion planner during the search for witness tra jectories. 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.
Publisher: http://dx.doi.org/10.1007/s10703-008-0058-5
PDF preprint: http://kavrakilab.org/publications/plaku-kavraki2009hybrid-systems-from.pdf