# Modal Logics for Timed Control

Abstract : In this paper we use the timed modal logic $L_\nu$ 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^c$) of the logic Lnu with a new modality. More precisely we define a fragment of $L_\nu$, namely $L_\nu^d$, such that any control objective of $L_\nu^d$ can be translated into a $L^c$ 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^c$ strictly increases the expressive power of $L_\nu$ while model-checking of Lc remains EXPTIME-complete.
Type de document :
Communication dans un congrès
16th nt. onf. on oncurrency heory ('05), Aug 2005, San Francisco, United States. pp.81--94, 2005

Littérature citée [10 références]

https://hal.inria.fr/inria-00368581
Contributeur : Franck Cassez <>
Soumis le : mardi 17 mars 2009 - 05:08:58
Dernière modification le : mercredi 16 mai 2018 - 11:48:03
Document(s) archivé(s) le : mardi 8 juin 2010 - 23:32:28

### Fichiers

modal-control-concur05.pdf
Fichiers produits par l'(les) auteur(s)

### Identifiants

• HAL Id : inria-00368581, version 1

### Citation

Patricia Bouyer, Franck Cassez, François Laroussinie. Modal Logics for Timed Control. 16th nt. onf. on oncurrency heory ('05), Aug 2005, San Francisco, United States. pp.81--94, 2005. 〈inria-00368581〉

### Métriques

Consultations de la notice

## 148

Téléchargements de fichiers