Sampling-Based Resolution-Complete Algorithms for Safety Falsification of Linear Systems

TL;DR

This paper introduces sampling-based algorithms that guarantee finite-time termination for safety falsification of linear systems by systematically exploring input resolutions to find counterexamples or prove safety.

Contribution

It proposes the concept of resolution completeness and develops deterministic incremental search algorithms for safety analysis over infinite horizons.

Findings

Algorithms guarantee termination with conclusive safety or counterexample results.

The approach is applicable to linear time-invariant systems over infinite time horizons.

Provides a systematic method for safety falsification with finite resolution levels.

Abstract

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.