Falsification of LTL Safety Properties in Hybrid Systems

Publication Type:

Conference Paper

Authors:

Plaku, E.; L. E. Kavraki; Moshe Y. Vardi

Source:

Proc. of the Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), York, UK (2009)

Keywords:

Counterexample Search, hybrid systems, kavrakilab, Linear Temporal Logic, LTL, multi-layered synergistic planning, path planning, robotics, Safety Falsification, Sampling-based algorithms, TemporalHyDICE

Abstract:

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 φ.


Preprint PDF