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
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


Files produced by the author(s)


  • HAL Id : inria-00493638, version 1



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⟩



Record views


Files downloads