Sampling-Based Resolution-Complete Safety Falsification Of Linear Hybrid Systems

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 discrete-time LTI hybrid 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.