Comparing Parameterizations and Objective Functions for Maximizing the Volume of Zonotopic Invariant Sets
Chenliang Zhou, Heejin Ahn, Ian M. Mitchell
TL;DR
The paper addresses computing maximum-volume invariant zonotopes for discrete-time affine systems, with dynamics $x(t+1) = A x(t) + w$ under a box constraint. It proves that the volume of zonotope parameterizations (UTPD and SFG) is log-concave in the free parameters and uses this property in convex optimization to maximize invariant volume, comparing a true-volume objective with two fast heuristics across dimensions and orders. The results show that the heuristics are significantly faster but their quality declines as dimensionality grows, while the UTPD parameterization with true volume maintains higher quality at higher dimensions at a greater cost. These findings guide the design of scalable invariant-set computations for safety verification and motivate further exploration across dimensions, generator choices, invariant-set types, and additional algorithms.
Abstract
In formal safety verification, many proposed algorithms use parametric set representations and convert the computation of the relevant sets into an optimization problem; consequently, the choice of parameterization and objective function have a significant impact on the efficiency and accuracy of the resulting computation. In particular, recent papers have explored the use of zonotope set representations for various types of invariant sets. In this paper we collect two zonotope parameterizations that are numerically well-behaved and demonstrate that the volume of the corresponding zonotopes is log-concave in the parameters. We then experimentally explore the use of these two parameterizations in an algorithm for computing the maximum volume zonotope invariant under affine dynamics within a specified box constraint over a finite horizon. The true volume of the zonotopes is used as an objective function, along with two alternative heuristics that are faster to compute. We conclude that the heuristics are much faster in practice, although the relative quality of their results declines as the dimension of the problem increases; however, our conclusions are only preliminary due to so-far limited availability of compute resources.