TY - GEN
T1 - Sparse Intersection Checking for Sparse Polynomial Zonotopes
AU - Huang, Yushen
AU - Luo, Ertai
AU - Sun, Yifan
AU - Bak, Stanley
N1 - Publisher Copyright: © 2025 Copyright held by the owner/author(s).
PY - 2025/5/21
Y1 - 2025/5/21
N2 - Polynomial zonotopes are a non-convex set representation that have many applications, such as reachability analysis of hybrid systems, control in robotics, and verification of nonlinear systems. Such analysis methods often require intersection checking. The usual algorithm for intersection checking is to, first, overapproximate the polynomial zonotope by a zonotope and then, if the overapproximation is too large, split the set and recursively and repeat. Although the overapproximation error in this algorithm converges to the original polynomial zonotope, there are still two problems. First, the overapproximation error is not monotonically decreasing after each split. Second, more critically, the split polynomial zonotopes do not preserve the sparsity structure as the original polynomial zonotope, eliminating any memory and other efficiency benefits made possible by the sparse structure. In this paper, we propose a variation of polynomial zonotopes called denormalized polynomial zonotopes, where each factor variable does not need to be in the range [-1, 1]. We prove this slight modification eliminates the two above issues, while still guaranteeing that overapproximation error will converge to the exact polynomial zonotope. We demonstrate the efficiency improvements through numerical experiments, where in certain cases denormalized polynomial zonotope intersection checking is over 400x faster and uses 550x less memory.
AB - Polynomial zonotopes are a non-convex set representation that have many applications, such as reachability analysis of hybrid systems, control in robotics, and verification of nonlinear systems. Such analysis methods often require intersection checking. The usual algorithm for intersection checking is to, first, overapproximate the polynomial zonotope by a zonotope and then, if the overapproximation is too large, split the set and recursively and repeat. Although the overapproximation error in this algorithm converges to the original polynomial zonotope, there are still two problems. First, the overapproximation error is not monotonically decreasing after each split. Second, more critically, the split polynomial zonotopes do not preserve the sparsity structure as the original polynomial zonotope, eliminating any memory and other efficiency benefits made possible by the sparse structure. In this paper, we propose a variation of polynomial zonotopes called denormalized polynomial zonotopes, where each factor variable does not need to be in the range [-1, 1]. We prove this slight modification eliminates the two above issues, while still guaranteeing that overapproximation error will converge to the exact polynomial zonotope. We demonstrate the efficiency improvements through numerical experiments, where in certain cases denormalized polynomial zonotope intersection checking is over 400x faster and uses 550x less memory.
KW - Formal Verification
KW - Polynomial Zonotopes
KW - Reachability Analysis
UR - https://www.scopus.com/pages/publications/105007549500
U2 - 10.1145/3716863.3718029
DO - 10.1145/3716863.3718029
M3 - Conference contribution
T3 - HSCC 2025 - Proceedings of the 28th International Conference on Hybrid Systems: Computation and Control, part of CPS-IoT Week
BT - HSCC 2025 - Proceedings of the 28th International Conference on Hybrid Systems
PB - Association for Computing Machinery, Inc
T2 - 28th International Conference on Hybrid Systems: Computation and Control, HSCC 2025, held as part of the 18th Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2025
Y2 - 7 May 2025 through 9 May 2025
ER -