Modal Logics for Timed Control - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2005

Modal Logics for Timed Control

Résumé

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.
Fichier principal
Vignette du fichier
modal-control-concur05.pdf (342.32 Ko) Télécharger le fichier
slides-concur-05.pdf (1.03 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre
Loading...

Dates et versions

inria-00368581 , version 1 (17-03-2009)

Identifiants

  • HAL Id : inria-00368581 , version 1

Citer

Patricia Bouyer, Franck Cassez, François Laroussinie. Modal Logics for Timed Control. 16th {I}nt. {C}onf. on {C}oncurrency {T}heory ({CONCUR}'05), Aug 2005, San Francisco, United States. pp.81--94. ⟨inria-00368581⟩
127 Consultations
223 Téléchargements

Partager

Gmail Facebook X LinkedIn More