Volume 34, Number 2, 157-182, DOI: 10.1007/s10703-008-0058-5

Hybrid systems: from verification to falsification by combining motion planning and discrete search

Erion Plaku, Lydia E. Kavraki and Moshe Y. Vardi

From the issue entitled "Special Issue: Selected Papers from CAV 2007; Guest Editors: Werner Damm, Holger Hermanns, and Jürgen Niehaus"

View Related Documents

Abstract

We propose HyDICE, Hybrid Discrete Continuous Exploration, a multi-layered approach for hybrid-system falsification that combines motion planning with discrete search and discovers safety violations by computing witness trajectories to unsafe states. The discrete search uses discrete transitions and a state-space decomposition to guide the motion planner during the search for witness trajectories. Experiments on a nonlinear hybrid robotic system with over one million modes and experiments with an aircraft conflict-resolution protocol with high-dimensional continuous state spaces demonstrate the effectiveness of HyDICE. Comparisons to related work show computational speedups of up to two orders of magnitude.

Keywords  Hybrid system - Safety properties - Robot motion planning - Discrete search - Sampling-based planning - Decomposition - Nonlinear dynamics

Work supported in part by NSF CNS 0615328 (EP, LK, MV), NSF 0713623 (EP, LK), a Sloan Fellowship (LK), and NSF CCF 0613889 (MV). Equipment supported by NSF CNS 0454333 and NSF CNS 0421109 in partnership with Rice, AMD, and Cray.
A preliminary version of this work was published in the Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007). Lecture Notes in Computer Science, eds. W. Damm and H. Hermanns, vol. 4590, pp. 468–481. This work contains substantial improvements to the overall computational method introduced in the preliminary work and new experiments that were not included in the preliminary work.

Fulltext Preview

Image of the first page of the fulltext document