Efficient Backward Reachability Using the Minkowski Difference of Constrained Zonotopes

TL;DR

This paper introduces a scalable algorithm for backward reachability analysis of uncertain systems using constrained zonotopes and an efficient polynomial-time under-approximation of the Minkowski difference, enabling better control synthesis.

Contribution

It develops a novel polynomial-time method to under-approximate the Minkowski difference of constrained zonotopes, improving backward reachability analysis for uncertain systems.

Findings

The algorithm efficiently computes backward reachable sets for uncertain systems.

The Minkowski difference under-approximation is exact under certain conditions.

Examples demonstrate the effectiveness of the proposed methods.

Abstract

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.