Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Adaptive Parameter Tuning for Reachability Analysis of Linear Systems

Mark Wetzlinger, Niklas Kochdumper, Matthias Althoff

TL;DR

This work tackles the barrier to practical reachability analysis for linear systems posed by manual parameter tuning. It introduces a generic, runtime adaptive framework that automatically tunes time steps, propagation parameters, and set-representation complexity to keep the over-approximation error below a user-defined bound, proven to converge under mild assumptions. The approach decomposes the reachable set into a homogeneous and an inhomogeneous part and uses Taylor-based set computations with interval remainders, implemented with zonotopes to balance tightness and efficiency. Empirical results on ARCH benchmarks and random systems show the method outperforms manually-tuned configurations and is orders of magnitude faster than genetic algorithms, with manageable overhead and broad applicability to different reachability algorithms.

Abstract

Despite the possibility to quickly compute reachable sets of large-scale linear systems, current methods are not yet widely applied by practitioners. The main reason for this is probably that current approaches are not push-button-capable and still require to manually set crucial parameters, such as time step sizes and the accuracy of the used set representation -- these settings require expert knowledge. We present a generic framework to automatically find near-optimal parameters for reachability analysis of linear systems given a user-defined accuracy. To limit the computational overhead as much as possible, our methods tune all relevant parameters during runtime. We evaluate our approach on benchmarks from the ARCH competition as well as on random examples. Our results show that our new framework verifies the selected benchmarks faster than manually-tuned parameters and is an order of magnitude faster compared to genetic algorithms.

Adaptive Parameter Tuning for Reachability Analysis of Linear Systems

TL;DR

This work tackles the barrier to practical reachability analysis for linear systems posed by manual parameter tuning. It introduces a generic, runtime adaptive framework that automatically tunes time steps, propagation parameters, and set-representation complexity to keep the over-approximation error below a user-defined bound, proven to converge under mild assumptions. The approach decomposes the reachable set into a homogeneous and an inhomogeneous part and uses Taylor-based set computations with interval remainders, implemented with zonotopes to balance tightness and efficiency. Empirical results on ARCH benchmarks and random systems show the method outperforms manually-tuned configurations and is orders of magnitude faster than genetic algorithms, with manageable overhead and broad applicability to different reachability algorithms.

Abstract

Despite the possibility to quickly compute reachable sets of large-scale linear systems, current methods are not yet widely applied by practitioners. The main reason for this is probably that current approaches are not push-button-capable and still require to manually set crucial parameters, such as time step sizes and the accuracy of the used set representation -- these settings require expert knowledge. We present a generic framework to automatically find near-optimal parameters for reachability analysis of linear systems given a user-defined accuracy. To limit the computational overhead as much as possible, our methods tune all relevant parameters during runtime. We evaluate our approach on benchmarks from the ARCH competition as well as on random examples. Our results show that our new framework verifies the selected benchmarks faster than manually-tuned parameters and is an order of magnitude faster compared to genetic algorithms.

Paper Structure

This paper contains 21 sections, 7 theorems, 32 equations, 3 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. State of the Art
  3. Contributions
  4. Preliminaries
  5. Notation
  6. Reachability Analysis of Linear Systems
  7. Self-Parametrization
  8. Overview of Algorithm Parameters
  9. Error measures
  10. Adaptive Parameter Tuning
  11. Implementation
  12. Computation of Reachable Sets
  13. Verification of Assumptions
  14. Set Representation
  15. Numerical Examples
  16. ...and 6 more sections

Key Result

Proposition 1

Let ${\mathcal{S}_{=}}{} \subset \mathbb{R}^{n}$ and $\mathcal{S}_{+}{} \subset \mathbb{R}^{n}$ with ${0 \in \mathcal{S}_{+}{}}$ be non-empty compact, convex sets. The Hausdorff distance between ${\mathcal{S}_{=}}{}$ and ${\mathcal{S}_{\text{tot}}}{} := {\mathcal{S}_{=}}{} \oplus \mathcal{S}_{+}{}$ where $\texttt{box}(\mathcal{S}_{+}{})$ is the box enclosure of $\mathcal{S}_{+}{}$ and $r(\cdot)$

Figures (3)

  • Figure 1: Time consumption by parameter tuning in relation to total execution time using 50 randomly-generated systems per dimension.
  • Figure 2: Benchmark ISSF01 with the specifications ISS01, ISU01, and the reachable sets $\mathcal{R}([0,T])$ in dark gray ($\varepsilon_{\text{max}}{} = 20 \cdot 10^{-3}$), light gray ($\varepsilon_{\text{max}}{} = 10 \cdot 10^{-3}$), and ivory ($\varepsilon_{\text{max}}{} = 2 \cdot 10^{-3}$).
  • Figure 3: Benchmark ISSF01: $\Delta t, \eta, \rho{}$ for different $\varepsilon_{\text{max}}{}$: black ($\varepsilon_{\text{max}}{}=20\cdot 10^{-3}$), gray ($\varepsilon_{\text{max}}{}=10\cdot 10^{-3}$), and blue ($\varepsilon_{\text{max}}{}=2\cdot 10^{-3}$).

Theorems & Definitions (13)

  • Proposition 1
  • proof
  • Definition 1
  • Proposition 2
  • Theorem 1
  • proof
  • Proposition 3
  • proof
  • Proposition 4
  • proof
  • ...and 3 more