In this work, the reachable set estimation and safety verification problems
for a class of piecewise linear systems equipped with neural network
controllers are addressed. The neural network is considered to consist of
Rectified Linear Unit (ReLU) activation functions. A layer-by-layer approach is
developed for the output reachable set computation of ReLU neural networks. The
computation is formulated in the form of a set of manipulations for a union of
polytopes. Based on the output reachable set for neural network controllers,
the output reachable set for a piecewise linear feedback control system can be
estimated iteratively for a given finite-time interval. With the estimated
output reachable set, the safety verification for piecewise linear systems with
neural network controllers can be performed by checking the existence of
intersections of unsafe regions and output reach set. A numerical example is
presented to illustrate the effectiveness of our approach.

本文提出了使用神经网络控制器的分段线性系统的可达集估算和安全性验证问题，并开发了一种逐层方法来计算修正线性单位激活函数神经网络的输出可达集。基于神经网络控制器输出可达集，可以迭代地为给定的有限时间间隔估算分段线性反馈控制系统的输出可达集，并通过检查不安全区域和输出到达集的交集的存在来执行带有神经网络控制器的分段线性系统的安全性验证。