Hybrid Discrete Continuous Exploration (HyDICE)
|
Hybrid systems are formal models that combine discrete and continuous dynamics. Hybrid systems play an important role in transportation networks, manufacturing, robotics, medicine, biology, and other fields. As hybrid systems are often part of devices operating in safety-critical situations, the verification of safety properties of hybrid systems becomes increasingly important. A hybrid system is considered safe if unsafe states cannot be reached from initial safe states. Although significant progress has been made in the development of computational methods for the verification of safety properties of hybrid systems, novel approaches are needed for high-dimensional hybrid systems. Existing methods are limited to low-dimensional systems with five-six dimensions, simple dynamics, and/or few or no input controls. |
|
The contribution of this research is the development of novel methods for motion planning and testing of safety properties of hybrid systems that blend recent advances in robotics with methods developed in logic and discrete search. 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.