×

Modal logics for timed control. (English) Zbl 1134.68399

Abadi, Martín (ed.) et al., CONCUR 2005 – concurrency theory. 16th international conference, CONCUR 2005, San Francisco, CA, USA, August 23–26, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28309-9/pbk). Lecture Notes in Computer Science 3653, 81-94 (2005).
Summary: 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_\nu^{\text{cont}}\)) of the logic \(L_\nu\) with a new modality.
More precisely we define a fragment of \(L_\nu\), namely \(L_\nu^{\text{det}}\), such that any control objective of \(L_\nu^{\text{det}}\) can be translated into a \(L_\nu^{\text{cont}}\) 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_\nu^{\text{cont}}\) strictly increases the expressive power of \(L_\nu\) while model-checking of \(L_\nu^{\text{cont}}\) remains EXPTIME-complete.
For the entire collection see [Zbl 1084.68002].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B45 Modal logic (including the logic of norms)
93C65 Discrete event control/observation systems
PDFBibTeX XMLCite
Full Text: DOI