We consider a hybrid system controlled by a sampled-data controller whose action is periodically time-driven, that is, the control inputs can change only at the particular time instants. Then, we introduce transition systems as semantics of the controlled hybrid systems and consider a control specification given by a predicate. First, we derive a necessary and sufficient condition for the predicate to be control-invariant. Next, we show that there always exists the supremal control-invariant subpredicate for any predicate. Finally, we propose a procedure to compute it and obtain a sampled-data event controller which satisfies it.

Silva and Krogh formulate a sampled-data hybrid automaton to deal with time-driven events and discuss its verification. In this paper, we consider a state feedback control problem of the automaton. First, we introduce two transition systems as semantics of the automaton. Next, using these transition systems, we derive necessary and sufficient conditions for a predicate to be control-invariant. Finally, we show that there always exists the supremal control-invariant subpredicate for any predicate.