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.