Abstract. An algorithm for computing the maximal controlled invariant set and the least restrictive controller for discrete time systems is proposed. We show how the algorithm can be encoded using quantier elimination, which leads to a semi-decidability result for de nable systems. For discrete time linear systems with all sets speci ed by linear inequalities, a more e cient implementation is proposed using linear programming and Fourier elimination. If in addition the system is in controllable canonical form, the input is scalar and unbounded, the disturbance is scalar and bounded and the initial set is a rectangle, then the problem is decidable.