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.

• Type: Conference
• Year: 2005
• Where: CONCUR
• Authors: Patricia Bouyer, Franck Cassez, François Laroussinie
• Keywords: CONCUR 2005, Control Objective, Logic Lν, Timed Modal Logic