Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This paper is concerned with developing scalable algorithms that under-approximate the backward reachable sets, for discrete-time uncertain linear and nonlinear systems. Our algorithm sequentially linearizes the dynamics, and uses constrained zonotopes for set representation and computation. The main technical ingredient of our algorithm is an efficient way to under-approximate the Minkowski difference between a constrained zonotopic minuend and a zonotopic subtrahend, which consists of all possible values of the uncertainties and the linearization error. This Minkowski difference needs to be represented as a constrained zonotope to enable subsequent computation, but, as we show, it is impossible to find a polynomial-sized representation for it in polynomial time. Our algorithm finds a polynomial-sized under-approximation in polynomial time. We further analyze the conservatism of this under-approximation technique, and show that it is exact under some conditions. Based on the developed Minkowski difference technique, we detail two backward reachable set computation algorithms to control the linearization error and incorporate nonconvex state constraints. Several examples illustrate the effectiveness of our algorithms.

翻译：后向可达性分析对于综合控制器以确保封闭环状系统正确性至关重要。 本文关注开发离散时间不确定线性和非线性系统在后向可达数据集之间距离过低的可伸缩算法。 我们的算法依次线性地将动态线性化, 并使用受限制的zonoopes 用于设定表达和计算。 我们的算法的主要技术成分是将受限制的zonotopt minutuend 和 zonotototop 子拉根之间的差差差小于Minkowski 的有效方法, 其中包括不确定性和线性错误的所有可能值。 Minkowski 差异需要作为受限制的zonotoope 表示, 以便随后进行计算。 但是, 正如我们所显示的那样, 在多向时间, 我们的算法中找不到一个多面体积大小的配给度过低的配给性差。 我们进一步分析了这一配给不足技术的调和线性差, 并显示它是在某种可控性进度方法下实现的精确的。