Semidefinite Outer Approximation of the Backward Reachable Set of Discrete-time Autonomous Polynomial Systems

TL;DR

This paper introduces a novel semidefinite programming approach to approximate the backward reachable set of discrete-time polynomial systems, enabling safety verification and control synthesis.

Contribution

It formulates the problem as an infinite-dimensional LP on measures and develops a hierarchy of SDP relaxations for practical computation.

Findings

Successfully approximates backward reachable sets for three dynamical systems.

Provides a method to approximate preimages of semi-algebraic sets under polynomial maps.

Demonstrates convergence of the hierarchy of SDP relaxations.

Abstract

We approximate the backward reachable set of discrete-time autonomous polynomial systems using the recently developed occupation measure approach. We formulate the problem as an infinite-dimensional linear programming (LP) problem on measures and its dual on continuous functions. Then we approximate the LP by a hierarchy of finite-dimensional semidefinite programming (SDP) programs on moments of measures and their duals on sums-of-squares polynomials. Finally we solve the SDP's and obtain a sequence of outer approximations of the backward reachable set. We demonstrate our approach on three dynamical systems. As a special case, we also show how to approximate the preimage of a compact semi-algebraic set under a polynomial map.