E. Plaku, L. E. Kavraki, and M. Y. Vardi, “Falsification of LTL Safety Properties in Hybrid Systems,” in Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), York, UK, 2009.
This paper develops a novel computational method for the falsification of safety properties specified by syntactically safe linear temporal logic (LTL) formulas φ for hybrid systems with general nonlinear dynamics and input controls. The method is based on an effective combination of robot motion planning and model checking. Experiments on a hybrid robotic system benchmark with nonlinear dynamics show significant speedup over related work. The experiments also indicate significant speedup when using minimized DFA instead of non-minimized NFA, as obtained by standard tools, for representing the violating prefixes of φ.
Publisher: http://dx.doi.org/10.1007/s10009-012-0233-2
PDF preprint: http://kavrakilab.org/publications/plaku-kavraki2009falsification-of-ltl.pdf