Sciweavers

CONCUR
2005
Springer

Modal Logics for Timed Control

14 years 5 months ago
Modal Logics for Timed Control
In this paper we use the timed modal logic Lν 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 (Lcont ν ) of the logic Lν with a new modality. More precisely we define a fragment of Lν , namely Ldet ν , such that any control objective of Ldet ν can be translated into a Lcont ν 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 Lcont ν strictly increases the expressive power of Lν while model-checking of Lcont ν remains EXPTIMEcomplete.
Patricia Bouyer, Franck Cassez, François La
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CONCUR
Authors Patricia Bouyer, Franck Cassez, François Laroussinie
Comments (0)