Skip to Main content Skip to Navigation
Journal articles

Timed Modal Logics for Real-Time Systems - Specification, Verification and Control.

Abstract : In this paper, a timed modal logic Lc is presented for the specification and verification of real-time systems. Several important results for Lc are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for Lc model checking. Finally we consider several control problems for which Lc can be used to check controllability.
Document type :
Journal articles
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/inria-00493638
Contributor : Franck Cassez Connect in order to contact the contributor
Submitted on : Monday, June 21, 2010 - 6:00:08 AM
Last modification on : Tuesday, March 30, 2021 - 12:12:08 PM
Long-term archiving on: : Wednesday, September 22, 2010 - 5:53:01 PM

File

jlli-2010.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00493638, version 1

Collections

Citation

Patricia Bouyer, Franck Cassez, François Laroussinie. Timed Modal Logics for Real-Time Systems - Specification, Verification and Control.. Journal of Logic, Language and Computation, Springer, 2010. ⟨inria-00493638⟩

Share

Metrics

Record views

58

Files downloads

124