Modal logics for timed control

Abstract

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 Lvdet, 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. © Springer-Verlag Berlin Heidelberg 2005.