Resolution-complete safety falsification of continuous time systems

Publication Type:

Conference Paper

Authors:

Amit Bhatia; Emilio Frazzoli

Source:

Decision and Control, 2006 45th IEEE Conference on, p.3297-3302 (2006)

URL:

http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4178057

Keywords:

continuous time systems, continuous-time LTI systems, continuous-time systems, control system analysis, controlled trajectory, deterministic incremental search procedures, linear systems, reachability analysis, resolution-complete algorithm, resolution-complete safety falsification, safety property, safety specification, search problems, target resolution

Abstract:

In this paper we consider a class of analysis problems for control systems, aimed at safety falsification, i.e., checking whether a controlled trajectory exists that violates a given safety property. We introduce a notion of resolution completeness for safety falsification, and present a resolution-complete algorithm applicable to continuous-time LTI systems. The algorithm is based on deterministic incremental search procedures, building feasible trajectories exploring the reachable set at increasing resolution levels. Given a target resolution, the algorithm terminates either with a trajectory that violates the safety specification, or proves that no input within a certain class exists that violates the specification.


Publisher's web site