Invariant, Viability and Discriminating Kernel Under-Approximation via Zonotope Scaling

TL;DR

This work tackles scalable safety verification for discrete-time affine systems by constructing under-approximations of invariant, viable, and discriminating kernels using zonotopes scaled in center-generator form. Through convex optimization, the authors derive linear programs that compute these set families under both worst-case disturbances and best-case controls, with extensions to include time-varying control authority modeled as a scaled disturbance. The approach is demonstrated on rotation, double integrator, and a six-dimensional nonlinear quadrotor model, yielding larger, less conservative discriminating and viable sets than traditional ellipsoidal representations and showcasing practical computation times. The results suggest that zonotope-based under-approximations offer a scalable, practical framework for run-time safety analysis and filtering in high-dimensional systems, while highlighting ongoing challenges in moving from discrete to continuous-time dynamics and further improving scalability.

Abstract

Scalable safety verification of continuous state dynamic systems has been demonstrated through both reachability and viability analyses using parametric set representations; however, these two analyses are not interchangable in practice for such parametric representations. In this paper we consider viability analysis for discrete time affine dynamic systems with adversarial inputs. Given a set of state and input constraints, and treating the inputs in best-case and/or worst-case fashion, we construct invariant, viable and discriminating sets, which must therefore under-approximate the invariant, viable and discriminating kernels respectively. The sets are constructed by scaling zonotopes represented in center-generator form. The scale factors are found through efficient convex optimizations. The results are demonstrated on two toy examples and a six dimensional nonlinear longitudinal model of a quadrotor.

Figures (8)

• Figure 1: Computed invariant set $\mathcal{I}$ (red thick line) for the rotation example with varying numbers of generators in $\mathcal{I}$. Also shown are the constraint set $\mathcal{X}$ (blue thick line) and $\mathsf{R}\left({t},{\mathcal{I}}\right)$ (thin green lines) for $t = 1, \ldots T$. Top left: Two generators (the coordinate axes). Top right: Four generators (coordinate axes plus diagonals). Bottom left: Nine generators (equally spaced around top half circle). Bottom right: Sixteen random generators (only seven have scaling $\gamma_i > 0.01$).
• Figure 2: Computed invariant set for the rotation example with disturbance input using eight equally spaced generators for $\mathcal{I}$.
• Figure 3: Computed viable set $\mathcal{I}$ (red thick line) for the double integrator example with (left) and without (right) $\mathcal{F}$. Eight generators equally spaced in the north-west quadrant are used (only five have scaling $\gamma_i > 0.01$). Also shown are the constraint set $\mathcal{X}$ (blue thick line), $\mathsf{R}\left({\mathcal{I}},{t}\right)$ (thin green lines) for $t = 1, \ldots T$, and a collection of sample trajectories (star shows the initial conditions for each).
• Figure 4: Sample viable trajectory (shown as the thick black trajectory in figure \ref{['f:viable-example']}) with (left) and without (right) $\mathcal{F}$. Control at each time is chosen as close to $+1$ as possible subject to (\ref{['e:viable-input-control-disturb']}) on the left and (\ref{['e:viable-input-no-disturb']}) on the right. The dotted curve in the control subplot shows the scaling $\psi_1(t)$ (which is always zero on the right). Any difference between the actual control $u_1(t)$ and scaling $\psi_1(t)$ arises from $\Phi(t)$.
• Figure 5: Projection of the set of viable inputs at $t = 20$ with (left) and without (right) $\mathcal{F}$.

Theorems & Definitions (26)

• lemma 1
• proof
• proposition 1
• proof
• proposition 2
• proof
• proposition 3
• proof
• Remark 1
• Remark 2