# Linear Encodings for Polytope Containment Problems

## TL;DR

This paper introduces linear programming-based sufficient conditions for polytope containment problems, especially for affine transformations of H-polytopes, enabling efficient verification in control and verification applications.

## Contribution

It provides a linear programming approach for AH-polytope in AH-polytope containment, including special cases like zonotopes and Minkowski sums, with applications in control verification.

## Key findings

- Linear conditions for AH-polytope containment are derived.
- Efficient encodings enable convex optimization integration.
- Applications include controller verification and polytope approximation.

## Abstract

The polytope containment problem is deciding whether a polytope is a contained within another polytope. This problem is rooted in computational convexity, and arises in applications such as verification and control of dynamical systems. The complexity heavily depends on how the polytopes are represented. Describing polytopes by their hyperplanes (H-polytopes) is a popular representation. In many applications we use affine transformations of H-polytopes, which we refer to as AH-polytopes. Zonotopes, orthogonal projections of H-polytopes, and convex hulls/Minkowski sums of multiple H-polytopes can be efficiently represented as AH-polytopes. While there exists efficient necessary and sufficient conditions for AH-polytope in H-polytope containment, the case of AH-polytope in AH-polytope is known to be NP-complete. In this paper, we provide a sufficient condition for this problem that is cast as a linear program with size that grows linearly with the number of hyperplanes of each polytope. Special cases on zonotopes, Minkowski sums, convex hulls, and disjunctions of H-polytopes are studied. These efficient encodings enable us to designate certain components of polytopes as decision variables, and incorporate them into a convex optimization problem. We present examples on the zonotope containment problem, polytopic Hausdorff distances, zonotope order reduction, inner approximations of orthogonal projections, and demonstrate the usefulness of our results on formal controller verification and synthesis for hybrid systems.