Modal logics for timed control

In this paper we use the timed modal logic L_v to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (L_v^cont) of the logic L_v with a new modality. More precisely we define a fragment of L_v, namely L_v ^det, such that any control objective of L_v^det can be translated into a L_v^cont formula that holds for the plant if and only if there is a controller that can enforce the control objective. We also show that the new modality of L_v^cont strictly increases the expressive power of L_v while model-checking of L_v^cont remains EXPTIME-complete.