Anzeige
Erschienen in:
2017 | OriginalPaper | Buchkapitel
Simulation-Equivalent Reachability of Large Linear Systems with Inputs
verfasst von : Stanley Bak, Parasara Sridhar Duggirala
Erschienen in: Computer Aided Verification
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
Control systems can be subject to outside inputs, environmental effects, disturbances, and sensor/actuator inaccuracy. To model such systems, linear differential equations with constrained inputs are often used, \(\dot{x}(t) = A x(t) + B u(t)\), where the input vector u(t) stays in some bound. Simulating these models is an important tool for detecting design issues. However, since there may be many possible initial states and many possible valid sequences of inputs, simulation-only analysis may also miss critical system errors. In this paper, we present a scalable verification method that computes the simulation-equivalent reachable set for a linear system with inputs. This set consists of all the states that can be reached by a fixed-step simulation for (i) any choice of start state in the initial set and (ii) any choice of piecewise constant inputs.
Building upon a recently-developed reachable set computation technique that uses a state-set representation called a generalized star, we extend the approach to incorporate the effects of inputs using linear programming. The approach is made scalable through two optimizations based on Minkowski sum decomposition and warm-start linear programming. We demonstrate scalability by analyzing a series of large benchmark systems, including a system with over 10,000 dimensions (about two orders of magnitude larger than what can be handled by existing tools). The method detects previously-unknown violations in benchmark models, finding complex counter-example traces which validate both its correctness and accuracy.