Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis

Niklas Kochdumper, Matthias Althoff

TL;DR

Sparse polynomial zonotopes (SPZs) provide a non-convex, compact set representation that generalizes zonotopes, polytopes, and Taylor models for reachability analysis of nonlinear hybrid systems. The paper formalizes SPZs, develops a broad set of exact and over-approximate operations, and introduces an efficient reachability algorithm that mitigates wrapping and dependency-induced over-approximation via dependency tracking and restructuring. Conversions from common representations, enclosure strategies, and auxiliary operations are provided to enable integration with existing tools. Numerical benchmarks across nonlinear and hybrid systems show SPZs achieve tighter reachable sets with substantial speedups, enabling analysis without extensive set splitting. Overall, SPZs deliver polynomial-time set-ops, improved accuracy, and scalability for formal verification of nonlinear dynamical systems.

Abstract

We introduce sparse polynomial zonotopes, a new set representation for formal verification of hybrid systems. Sparse polynomial zonotopes can represent non-convex sets and are generalizations of zonotopes, polytopes, and Taylor models. Operations like Minkowski sum, quadratic mapping, and reduction of the representation size can be computed with polynomial complexity w.r.t. the dimension of the system. In particular, for reachability analysis of nonlinear systems, the wrapping effect is substantially reduced using sparse polynomial zonotopes, as demonstrated by numerical examples. In addition, we can significantly reduce the computation time compared to zonotopes when dealing with nonlinear dynamics.

Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis

TL;DR

Sparse polynomial zonotopes (SPZs) provide a non-convex, compact set representation that generalizes zonotopes, polytopes, and Taylor models for reachability analysis of nonlinear hybrid systems. The paper formalizes SPZs, develops a broad set of exact and over-approximate operations, and introduces an efficient reachability algorithm that mitigates wrapping and dependency-induced over-approximation via dependency tracking and restructuring. Conversions from common representations, enclosure strategies, and auxiliary operations are provided to enable integration with existing tools. Numerical benchmarks across nonlinear and hybrid systems show SPZs achieve tighter reachable sets with substantial speedups, enabling analysis without extensive set splitting. Overall, SPZs deliver polynomial-time set-ops, improved accuracy, and scalability for formal verification of nonlinear dynamical systems.

Abstract

We introduce sparse polynomial zonotopes, a new set representation for formal verification of hybrid systems. Sparse polynomial zonotopes can represent non-convex sets and are generalizations of zonotopes, polytopes, and Taylor models. Operations like Minkowski sum, quadratic mapping, and reduction of the representation size can be computed with polynomial complexity w.r.t. the dimension of the system. In particular, for reachability analysis of nonlinear systems, the wrapping effect is substantially reduced using sparse polynomial zonotopes, as demonstrated by numerical examples. In addition, we can significantly reduce the computation time compared to zonotopes when dealing with nonlinear dynamics.

Paper Structure

This paper contains 36 sections, 18 theorems, 68 equations, 9 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. State of the Art
  3. Overview
  4. Notation
  5. Sparse Polynomial Zonotopes
  6. Preliminary Operations
  7. Merging the Set of Identifiers
  8. Transformation to a Compressed Representation
  9. Conversion from other Set Representations
  10. Zonotope and Interval
  11. Polytope
  12. Taylor Model
  13. Enclosure by other Set Representations
  14. Zonotope
  15. Polytope
  16. ...and 21 more sections

Key Result

Proposition 1

(Merge ID) Given two SPZs, $\mathcal{PZ}_1 = \langle G_1,\newline G_{I,1}, E_1, id_1 \rangle_{PZ}$ and $\mathcal{PZ}_2 = \langle G_2, \newline G_{I,2},$$E_2, id_2 \rangle_{PZ}$, mergeID returns two adjusted SPZs with identical identifier vectors that are equivalent to $\mathcal{PZ}_1$ and $\mathcal{ where $a = |\mathcal{H}|+p_1$.

Figures (9)

  • Figure 1: Visualization of the relations between the different set representations, where A $\rightarrow$ B denotes that B is a generalization of A.
  • Figure 2: Construction of the SPZ in Example \ref{['ex:PolyZonotope']} from the single generator vectors.
  • Figure 3: Enclosure of the SPZ in \ref{['eq:polyZonotopeEnclose']} with a zonotope (left), a polytope (middle) and an interval (right).
  • Figure 4: Exact quadratic map and over-approximation computed with Prop. \ref{['prop:quadMapSpecial']} for the SPZ in Example \ref{['ex:quadMap']}.
  • Figure 5: Exact convex hull and over-approximation computed with Prop. \ref{['prop:convHullSpecial']} for the SPZ s in Example \ref{['ex:convHull']}.
  • ...and 4 more figures

Theorems & Definitions (48)

  • Definition 1
  • Example 1
  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • Definition 2
  • Proposition 3
  • proof
  • Definition 3
  • ...and 38 more