Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems

In this paper we propose a computational method based on semi-definite programming for synthesizing infinite-time reach-avoid sets in discrete-time polynomial systems. An infinite-time reach-avoid set is a set of initial states making the system eventually, i.e., within finite time enter the target set while remaining inside another specified (safe) set during each time step preceding the target hit. The reach-avoid set is first characterized equivalently as a strictly positive sub-level of a bounded value function, which in turn is shown to be a solution to a system of derived equations. The derived equations are further relaxed into a system of inequalities, which is encoded into semi-definite constraints based on the sum-of-squares decomposition for multivariate polynomials, such that the problem of synthesizing inner-approximations of the reach-avoid set can be addressed via solving a semi-definite programming problem. Two examples demonstrate the proposed approach.