Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Franck Cassez Connect in order to contact the contributor
Submitted on : Tuesday, March 17, 2009 - 5:08:58 AM
Last modification on : Wednesday, April 27, 2022 - 4:40:04 AM
Long-term archiving on: : Tuesday, June 8, 2010 - 11:32:28 PM


  • HAL Id : inria-00368581, version 1


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. ⟨inria-00368581⟩



Record views


Files downloads