Falsification of LTL 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.
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.
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.
This work has been supported by CNS 0615328.
