  Hybrid zonotopes generalize constrained zonotopes by introducing additional
binary variables and possess some unique properties that make them convenient
to represent nonconvex sets. This paper presents novel hybrid zonotope-based
methods for the reachability analysis and safety verification of neural
feedback systems. Algorithms are proposed to compute the input-output
relationship of each layer of a feedforward neural network, as well as the
exact reachable sets of neural feedback systems. In addition, a sufficient and
necessary condition is formulated as a mixed-integer linear program to certify
whether the trajectories of a neural feedback system can avoid unsafe regions.
The proposed approach is shown to yield a formulation that provides the
tightest convex relaxation for the reachable sets of the neural feedback
system. Complexity reduction techniques for the reachable sets are developed to
balance the computation efficiency and approximation accuracy. Two numerical
examples demonstrate the superior performance of the proposed approach compared
to other existing methods.

Optimization and Control