Comparing Parameterizations and Objective Functions for Maximizing the Volume of Zonotopic Invariant Sets

TL;DR

This paper investigates how different parameterizations and objective functions affect the computation of maximum volume zonotope invariant sets in safety verification, comparing true volume and heuristic approaches.

Contribution

It introduces two well-behaved zonotope parameterizations and analyzes their log-concavity, providing insights into efficient optimization for invariant set computation.

Findings

Heuristics are significantly faster than true volume optimization.

The quality of heuristics declines with increasing problem dimension.

Log-concavity of volume in parameters aids optimization.

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.