Hybrid systems are formal models that are used to model systems exhibiting both continuous and discrete behaviour in their evolution. Hybrid systems play an important role in modeling complex systems in fields like transportation networks, manufacturing processes, robotics, medicine, biology, and many others. The evolution of the state of a physical system is usually governed by a set of differential equations. When such a system is controlled at a high level using digital logic and computer programs through an interface defined by analog-to-digital (A/D) and digital-to-analog (D/A) converters, the overall system shows hybrid behavior. The state of such a system has a continuous component and a discrete component.
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 the set of initial 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.
Motivated by the success of multi-layered planning approaches for solving challenging motion planning problems efficiently (SyCLoP), we have recently proposed a similar set of approaches for falsification of safety specifications (HyDICE) and the more complex specifications expressed in Linear Temporal Logic (LTL) (TemporalHyDICE) for hybrid systems. The approaches synergistically combine planning on state-space of the system with discrete high-level planning to search for feasible counterexamples to given specifications. The results obtained so far are encouraging and the proposed approaches have been shown to perform significantly better than other state-of-the-art approaches proposed recently.
This work has been supported by CNS 0615328 and NSF CCF 1018798.