Kavraki Lab

Falsification of Safety Specifications using Sampling-based Algorithms

The contribution of this research is the development of a novel approach for falsifying LTL safety specifications for hybrid systems using decomposition-based planning algorithms. The approach extends the HyDICE approach so that complex specifications expressed using Linear Temporal Logic (LTL) can be falsified efficiently.

TemporalHyDICE

The approach combines state-of-the-art ideas from model checking, motion planning and discrete planning. The abstractions for such class of problems are based on the set of propositions (defined on the state-space) and the underlying discrete structure of the hybrid system.

 

Abstractions used in TemporalHyDICE

As we show, the proposed approach performs significantly better than using simpler approaches like monitor-based approach or a model-checker guided search on the continuous space. This work highlights the importance of combining discrete search with planning in system’s state-space in a synergistic fashion. The same observation was seen while solving different class of planning problems in the SyCLoP and the HyDICE framework.

Performance comparison of TemporalHyDICE with other approaches

This work has been supported by CNS 0615328 and NSF CCF 1018798.