<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Plaku, E.</style></author><author><style face="normal" font="default" size="100%">Lydia E. Kavraki</style></author><author><style face="normal" font="default" size="100%">Moshe Y. Vardi</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Falsiﬁcation of LTL Safety Properties in Hybrid Systems</style></title><secondary-title><style face="normal" font="default" size="100%">Proc. of the Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)</style></secondary-title></titles><keywords><keyword><style  face="normal" font="default" size="100%">Counterexample Search</style></keyword><keyword><style  face="normal" font="default" size="100%">hybrid systems</style></keyword><keyword><style  face="normal" font="default" size="100%">kavrakilab</style></keyword><keyword><style  face="normal" font="default" size="100%">Linear Temporal Logic</style></keyword><keyword><style  face="normal" font="default" size="100%">LTL</style></keyword><keyword><style  face="normal" font="default" size="100%">path planning</style></keyword><keyword><style  face="normal" font="default" size="100%">robotics</style></keyword><keyword><style  face="normal" font="default" size="100%">Safety Falsification</style></keyword><keyword><style  face="normal" font="default" size="100%">Sampling-based algorithms</style></keyword></keywords><dates><year><style  face="normal" font="default" size="100%">2009</style></year></dates><pub-location><style face="normal" font="default" size="100%">York, UK</style></pub-location><abstract><style face="normal" font="default" size="100%">This paper develops a novel computational method for the falsiﬁcation of safety properties speciﬁed by syntactically safe linear temporal logic (LTL) formulas φ for hybrid systems with general nonlinear dynamics and input controls. The method is based on an eﬀective 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 preﬁxes of φ. </style></abstract></record></records></xml>