Fully-Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets

TL;DR

This work tackles the challenge of formally verifying safety for linear time-invariant systems under uncertainty without requiring expert parameter tuning. It introduces a fully automated reachability framework that guarantees a user-specified Hausdorff distance bound between the exact and computed reach sets by adaptively tuning the time step, truncation order, and zonotope order. A novel Minkowski-difference-based mechanism extracts inner-approximations from the outer enclosures, enabling a sound automated verifier that iteratively refines both approximations to prove or falsify time-varying safety specifications. The approach is implemented in CORA and demonstrated on electrical circuits, ARCH benchmarks, and an autonomous-car scenario, showing competitive performance with state-of-the-art tools while eliminating manual parameter tuning. Overall, the method lowers the barrier to formal verification for linear systems and provides a scalable pathway toward broader adoption in safety-critical contexts.

Abstract

Reachability analysis is a formal method to guarantee safety of dynamical systems under the influence of uncertainties. A substantial bottleneck of all reachability algorithms is the necessity to adequately tune specific algorithm parameters, such as the time step size, which requires expert knowledge. In this work, we solve this issue with a fully automated reachability algorithm that tunes all algorithm parameters internally such that the reachable set enclosure respects a user-defined approximation error bound in terms of the Hausdorff distance to the exact reachable set. Moreover, this bound can be used to extract an inner-approximation of the reachable set from the outer-approximation using the Minkowski difference. Finally, we propose a novel verification algorithm that automatically refines the accuracy of the outer-approximation and inner-approximation until specifications given by time-varying safe and unsafe sets can be verified or falsified. The numerical evaluation demonstrates that our verification algorithm successfully verifies or falsifies benchmarks from different domains without requiring manual tuning.

Figures (6)

• Figure 1: Overview of theoretical contributions in Secs. \ref{['sec:tuning']}-\ref{['sec:verification']}.
• Figure 2: Visualization of the three steps required to compute the homogeneous solution of the first time interval, adapted from Althoff2010a.
• Figure 3: Reachable set computation using the correct particular time-interval solution $\widehat{\mathcal{P}}^\mathcal{U}{}(\tau_k)$ (left) and an outer-approximation $\widehat{\mathcal{P}}^\mathcal{U}{}(t_{k+1}) \supseteq \widehat{\mathcal{P}}^\mathcal{U}{}(\tau_k)$ (right).
• Figure 4: The errors $\varepsilon^{\text{a}}_{k}$ and $\varepsilon^{\text{r}}_{k}$ until $t_k$ and the bounds $\overline{\varepsilon}^{\text{a}}(t)$ and $\overline{\varepsilon}^{\text{r}}(t)$ yield the individual error bounds $\overline{\varepsilon}^{\text{n},\tau}_{k}, \overline{\varepsilon}^{\text{a},\tau}_{k}, \overline{\varepsilon}^{\text{r},\tau}_{k}$ for the current step $k$.
• Figure 5: Inner- and outer-approximations of the final reachable set $\mathcal{R}(t_{\text{end}}{})$ for the electric circuit using different error bounds $\varepsilon_\text{max}{}$, with the exact reachable set is shown in black.

Theorems & Definitions (38)

• Definition 1: Zonotope
• Definition 2: Constrained zonotope
• Definition 3: Polytope
• Definition 4: Zonotope order reduction
• Definition 5: Hausdorff distance
• Definition 6: Reachable set
• Proposition 1: Affine dynamics error
• proof
• Proposition 2: Time-point error in particular solution
• proof