Inner-approximate Reachability Computation via Zonotopic Boundary Analysis

TL;DR

This work proposes a boundary-based inner-approximation framework for nonlinear ODEs, representing states as zonotopes and computing tight inner-approximations by excluding boundary-reached states. It introduces three core innovations: (i) a non-overlapping zonotope boundary extraction algorithm using a cross-product construction, (ii) a zonotopal tiling algorithm with boundary and tiling matrices to refine boundaries into non-overlapping tiles, and (iii) an adaptive contraction strategy that flexibly shrinks outer-approximations to produce less conservative inner-approximations. A time-inverted LP-based verification step ensures the computed inner-approximation is sound, and a prototype tool, BdryReach, demonstrates superior efficiency and precision compared to state-of-the-art methods, including in high dimensions, long horizons, and large initial sets. These advances enable scalable, accurate inner-approximation computation suitable for formal verification, planning, and safety analysis of nonlinear dynamical systems. The combination of boundary extraction, tiling-based refinement, and adaptive contraction yields substantial performance gains, making inner-approximation methods more practical for complex, real-world systems.

Abstract

Inner-approximate reachability analysis involves calculating subsets of reachable sets, known as inner-approximations. This analysis is crucial in the fields of dynamic systems analysis and control theory as it provides a reliable estimation of the set of states that a system can reach from given initial states at a specific time instant. In this paper, we study the inner-approximate reachability analysis problem based on the set-boundary reachability method for systems modelled by ordinary differential equations, in which the computed inner-approximations are represented with zonotopes. The set-boundary reachability method computes an inner-approximation by excluding states reached from the initial set's boundary. The effectiveness of this method is highly dependent on the efficient extraction of the exact boundary of the initial set. To address this, we propose methods leveraging boundary and tiling matrices that can efficiently extract and refine the exact boundary of the initial set represented by zonotopes. Additionally, we enhance the exclusion strategy by contracting the outer-approximations in a flexible way, which allows for the computation of less conservative inner-approximations. To evaluate the proposed method, we compare it with state-of-the-art methods against a series of benchmarks. The numerical results demonstrate that our method is not only efficient but also accurate in computing inner-approximations.

Figures (5)

• Figure 1: Illustration of inner-approximation computation framework
• Figure 2: Illustration of boundary extraction algorithm
• Figure 3: Illustration of one-step tiling
• Figure 4: Illustration of boundary refinement
• Figure 5: Illustration in the proof of Theorem \ref{['thm: partition of a Zonotope']}.

Theorems & Definitions (17)

• definition thmcounterdefinition: Reachable Set
• definition thmcounterdefinition
• definition thmcounterdefinition: Zonotope
• definition thmcounterdefinition: Cross Product
• remark thmcounterremark
• theorem thmcountertheorem: Soundness of boundary extraction algorithm
• definition thmcounterdefinition: Boundary Matrix
• definition thmcounterdefinition: Tiling Matrix
• remark thmcounterremark
• remark thmcounterremark