In this paper we use the timed modal logic Lv 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 (Lvcont) of the logic Lv with a new modality. More precisely we define a fragment of Lv, namely Lv det, such that any control objective of Lvdet can be translated into a Lvcont 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 Lvcont strictly increases the expressive power of Lv while model-checking of Lvcont remains EXPTIME-complete.
|Number of pages||14|
|Journal||Lecture Notes in Computer Science|
|Publication status||Published - 2005|