Hybrid Systems: From Verification to Falsification

E. Plaku, L. E. Kavraki, and M. Y. Vardi, “Hybrid Systems: From Verification to Falsification,” in International Conference on Computer Aided Verification (CAV), Berlin, Germany, 2007, vol. 4590, pp. 468–481.


We propose HyDICE, Hybrid DIscrete Continuous Exploration, a multi-layered approach for hybrid-system testing that integrates continuous sampling-based robot motion planning with discrete searching. The discrete search uses the discrete transitions of the hybrid system and coarse-grained decompositions of the continuous state spaces or related projections to guide the motion planner during the search for witness trajectories. Experiments presented in this paper, using a hybrid system inspired by robot motion planning and with nonlinear dynamics associated with each of several thousand modes, provide an initial validation of HyDICE and demonstrate its promise as a hybrid-system testing method. Comparisons to related work show computational speedups of up to two orders of magnitude.

Publisher: http://dx.doi.org/10.1007/978-3-540-73368-3_48

PDF preprint: http://kavrakilab.org/publications/plaku-kavraki2007hybrid-systems-from.pdf