Decidable and semi-decidable controller synthesis for classes of discrete time hybrid systems

In this paper, we study classes of discrete time hybrid systems for which the classical algorithm for computing the maximal controlled invariant set and the least restrictive controller is computable and guaranteed to terminate in a finite number of iterations. We show how the algorithm can be encoded using quantifier elimination, which leads to a semi-decidability result for definable hybrid systems. For discrete time linear systems with linear constraints that are either controllable or nilpotent and have bounded disturbances, we show that the controlled invariance algorithm terminates in a number of iterations which is at most the dimension of the state space. Both in the hybrid and in the linear case, our results are much more general than the corresponding ones for continuous time systems. Finally we show that for linear systems with ellipsoidal constraints, an approximated solution can be obtained using robust convex programming. We provide an example showing that our algorithm gives better estimations than other ellipsoidal methods and is more efficient than the exact method for linear constraints