Reachability Analysis of Large Linear Systems with Uncertain Inputs in the Krylov Subspace

TL;DR

This paper introduces a Krylov subspace-based method for reachability analysis of large linear systems with uncertain, arbitrarily varying inputs, enabling analysis of systems with thousands of states.

Contribution

It extends Krylov methods to handle arbitrarily varying inputs, significantly improving the scalability of reachability analysis for large systems.

Findings

Able to analyze systems with thousands of states

Handles arbitrarily varying inputs in reachability analysis

Improves scalability over previous methods

Abstract

One often wishes for the ability to formally analyze large-scale systems---typically, however, one can either formally analyze a rather small system or informally analyze a large-scale system. This work tries to further close this performance gap for reachability analysis of linear systems. Reachability analysis can capture the whole set of possible solutions of a dynamic system and is thus used to prove that unsafe states are never reached; this requires full consideration of arbitrarily varying uncertain inputs, since sensor noise or disturbances usually do not follow any patterns. We use Krylov methods in this work to compute reachable sets for large-scale linear systems. While Krylov methods have been used before in reachability analysis, we overcome the previous limitation that inputs must be (piecewise) constant. As a result, we can compute reachable sets of systems with several thousand state variables for bounded, but arbitrarily varying inputs.