Modal logics for timed control

Patricia Bouyer, Franck Cassez, François Laroussinie

Research output: Contribution to journalConference paperpeer-review

4 Citations (Scopus)

Abstract

In this paper we use the timed modal logic Lv 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 (Lvcont) of the logic Lv with a new modality. More precisely we define a fragment of Lv, namely Lv det, such that any control objective of Lvdet can be translated into a Lvcont 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 Lvcont strictly increases the expressive power of Lv while model-checking of Lvcont remains EXPTIME-complete.

Original languageEnglish
Pages (from-to)81-94
Number of pages14
JournalLecture Notes in Computer Science
Volume3653
Publication statusPublished - 2005
Externally publishedYes

Fingerprint Dive into the research topics of 'Modal logics for timed control'. Together they form a unique fingerprint.

Cite this