## Abstract

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.

Original language | English |
---|---|

Pages (from-to) | 81-94 |

Number of pages | 14 |

Journal | Lecture Notes in Computer Science |

Volume | 3653 |

Publication status | Published - 2005 |

Externally published | Yes |