  In this paper, we describe a novel approach for checking safety
specifications of a dynamical system with exogenous inputs over infinite time
horizon that is guaranteed to terminate in finite time with a conclusive
answer. We introduce the notion of resolution completeness for analysis of
safety falsification algorithms and propose sampling-based resolution-complete
algorithms for safety falsification of linear time-invariant discrete time
systems over infinite time horizon. The algorithms are based on deterministic
incremental search procedures, exploring the reachable set for feasible counter
examples to safety at increasing resolution levels of the input. Given a target
resolution of inputs, the algorithms are guaranteed to terminate either with a
reachable state that violates the safety specification, or prove that no input
exists at the given resolution that violates the specification.
