The contribution of this research is the development of novel methods for testing of safety properties of hybrid systems that blend recent advances in robotics with methods developed in logic and discrete search. The approach extends the SyCLoP framework to hybrid systems for falsifying safety specifications of such systems.
The discrete search uses the discrete transitions of the hybrid system and a state-space decomposition to guide the search for witness trajectories. Experiments using a hybrid system inspired by robot motion planning and with nonlinear dynamics associated with each of several thousand modes demonstrate the efficiency of HyDICE as a hybrid-system testing and motion-planning method. Comparisons to related work show computational speedups of up to two orders of magnitude.
This work has been supported by CNS 0615328.