An integrated approach to the symbolic control design of nonlinear systems with infinite states specifications